% -----------------------------------------------------------------
% leanseq.pl - A sequent calculus prover implemented in Prolog
% -----------------------------------------------------------------
:- use_module(library(lists)).
:- use_module(library(statistics)).
% operator definitions (TPTP syntax)
:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % conditional
:- op(1120, xfy, <=>).  % biconditional
:- op( 500, fy, !).     % universal quantifier:  ![X]:
:- op( 500, fy, ?).     % existential quantifier:  ?[X]:
:- op( 500,xfy, :).
% -----------------------------------------------------------------
provable(F,P):-
        time(prove([]>[F],P)).
% -----------------------------------------------------------------
%% 1. Initial rule: if G and D are strings [i.e. lists] of atomic formulae,
%% then G > D  is a theorem if some atomic formula occurs on both sides of the arrow:                 
prove(G>D, ax(G>D, A)):-
        member(A,G), member(B,D), A==B,!.
% In the ten rules listed below, G and D, are always
% strings (possibly empty) of atomic formulae.
% FIRST, NON-BRANCHING RULES 
%% 2. Conditional on the  right 
prove(G>D, rcond(G>D,P)):-
        select((A=>B),D,D1),!,
        prove([A|G]>[B|D1],P).
%% 3. Disjunction on the right 
prove(G>D, ror(G>D, P)):-
        select((A|B),D,D1),!,
        prove(G>[A,B|D1],P).
%% 4. Negation on the right: If A,G >
prove(G>D, rneg(G>D,P)):-
        select(~A,D,D1),!,
        prove([A|G]>D1,P).
%% 5. Negation on the left 
prove(G>D, lneg(G>D,P)):-
        select(~A,G,G1),!,
        prove(G1>[A|D],P).
%% 6. Conjunction on the left
prove(G>D, land(G>D,P)):-
        select((A&B),G,G1),!,
        prove([A,B|G1]>D,P).
% SECOND, BRANCHING RULES 
%% 7. Biconditional on the right
prove(G>D, rbicond(G>D,P1,P2)):-
        select((A<=>B),D,D1),!,
        prove([A|G]>[B|D1],P1),
        prove([B|G]>[A|D1], P2).
%% 8. Biconditional on the left
prove(G>D, lbicond(G>D, P1,P2)):-
        select((A<=>B),G,G1),!,
        prove([A,B|G1]>D,P1),
        prove(G1>[A,B|D],P2).
%% 9. Conditional on the left
prove(G>D, lcond(G>D,P1,P2)):-
        select((A=>B),G,G1),!,
        prove(G1>[A|D],P1),
        prove([B|G1]>D,P2).
%% 10. Conjunction on the right
prove(G>D, rand(G>D,P1,P2)):-
        select((A&B) ,D,D1),!,
        prove(G>[A|D1],P1),
        prove(G>[B|D1],P2).
%% 11. Disjunction on the left
prove(G>D, lor(G>D, P1,P2)):-
        select((A|B),G,G1),!,
        prove([A|G1]>D, P1),
        prove([B|G1]>D, P2).
% Third - One and only one refutation rule.
% NB: this rule in Prolog must be the last one in the order of clauses. 
%% 12 - Failure-rule
prove(G>D, asq(G<D, asq)):-
        \+ (member(A,G), member(A,D)),
        write("Unprovable formula ! ").

