% -----------------------------------------------------------------
% leanseq.pl - A sequent calculus prover implemented in Prolog
% -----------------------------------------------------------------

% operator definitions (TPTP syntax)

:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % implication
:- op( 500, fy, !).     % universal quantifier:  ![X]:
:- op( 500, fy, ?).     % existential quantifier:  ?[X]:
:- op( 500,xfy, :).

% -----------------------------------------------------------------
prove(F) :- prove(F,1).

prove(F,I) :- print(iteration:I), nl,
              prove([] > [F],[],I).
prove(F,I) :- I1 is I+1, prove(F,I1).
% -----------------------------------------------------------------

% axiom
prove(G > D,_,_) :- member(A,G), member(B,D),
                    unify_with_occurs_check(A,B).

% conjunction
prove(G > D,FV,I) :- select1(A&B,G,G1), !,
                     prove([A,B|G1] > D,FV,I).

prove(G > D,FV,I) :- select1(A&B,D,D1), !,
                     prove(G > [A|D1],FV,I),
                     prove(G > [B|D1],FV,I).

% disjunction
prove(G > D,FV,I) :- select1(A|B,G,G1), !,
                     prove([A|G1] > D,FV,I),
                     prove([B|G1] > D,FV,I).

prove(G > D,FV,I) :- select1(A|B,D,D1), !,
                     prove(G > [A,B|D1],FV,I).

% implication
prove(G > D,FV,I) :- select1(A=>B,G,G1), !,
                     prove(G1 > [A|D],FV,I),
                     prove([B|G1] > D,FV,I).

prove(G > D,FV,I) :- select1(A=>B,D,D1), !,
                     prove([A|G] > [B|D1],FV,I).

% negation
prove(G > D,FV,I) :- select1(~A,G,G1), !,
                     prove(G1 > [A|D],FV,I).

prove(G > D,FV,I) :- select1(~A,D,D1), !,
                     prove([A|G] > D1,FV,I).

% universal quantifier
prove(G > D,FV,I) :- member((![X]:A),G),
                     \+ length(FV,I),
                     copy_term((X:A,FV),(Y:A1,FV)),
                     prove([A1|G] > D,[Y|FV],I).

% existential quantifier
prove(G > D,FV,I) :- member((?[X]:A),D),
                     \+ length(FV,I),
                     copy_term((X:A,FV),(Y:A1,FV)),
                     prove(G > [A1|D],[Y|FV],I).

% -----------------------------------------------------------------
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).
% -----------------------------------------------------------------