:- set_prolog_flag(toplevel_print_options, [quoted(true), portray(true), attributes(portray), max_depth(999), priority(699)]).

% Propositional Sequent Calculus Prover constructed in Prolog
% author: Robert Keller

/* Example output from test([not(or(a, b))], [and(not(a), not(b))]).
 *
 * Proof of sequent or(not(a),not(b)) |- not(and(a,b)):
 * 1: a, b |- a  -- Axiom
 * 2: not(a), a, b |-   -- not L, line 1
 * 3: a, b |- b  -- Axiom
 * 4: not(b), a, b |-   -- not L, line 3
 * 5: a, b, or(not(a),not(b)) |-   -- or L, lines 2 and 4
 * 6: and(a,b), or(not(a),not(b)) |-   -- and L, line 5
 * 7: or(not(a),not(b)) |- not(and(a,b))  -- not R, line 6
 */

% If L |- R, where L and R are lists of formula,
% prove(L, R, Proof) will produce a sequent calculus proof tree.
% Using test(L, R) will display the proof in line-numbered fashion.
% If the sequent is not provable, the prove predicate will fail.

prove(L, R, axiom(L, R)) :- member(F, L), member(F, R).

prove(L, R, notLeft(L, R, Proof)) :-
            select(not(A), L, Rest),
            prove(Rest, [A | R], Proof).

prove(L, R, notRight(L, R, Proof)) :-
            select(not(A), R, Rest),
            prove([A | L], Rest, Proof).

prove(L, R, andLeft(L, R, Proof)) :-
	    select(and(A, B), L, Rest), 
            prove([A, B | Rest], R, Proof).

prove(L, R, orRight(L, R, Proof)) :-
            select(or(A, B), R, Rest),
            prove(L, [A, B | Rest], Proof).

prove(L, R, impliesRight(L, R, Proof)) :-
            select(implies(A, B), R, Rest),
            prove([A | L], [B | Rest], Proof).

prove(L, R, andRight(L, R, ProofL, ProofR)) :-
	    select(and(A, B), R, Rest), 
            prove(L, [A | Rest], ProofL), 
            prove(L, [B | Rest], ProofR).

prove(L, R, orLeft(L, R, ProofL, ProofR)) :- 
	    select(or(A, B), L, Rest), 
            prove([A | Rest], R, ProofL), 
            prove([B | Rest], R, ProofR).

prove(L, R, impliesLeft(L, R, ProofL, ProofR)) :- 
	    select(implies(A, B), L, Rest), 
            prove(Rest, [A | R], ProofL), 
            prove([B | Rest], R, ProofR).

test(Left, Right) :-
    prove(Left, Right, Proof) ->
        (
        nl,
        nl,
        write('Proof of sequent '),
        showSequent(Left, Right),
        write(':'),
        nl,
        showProof(Proof)        
        )
    ;   (
        nl,
        nl,
        write('No proof found for sequent '),
        write(Left),
        turnstile,
        write(Right),
        write('.'),
        nl
        ).

showSequent(L, R) :-
    showList(L),
    turnstile,
    showList(R).

showList([]).
showList([A]) :-
    write(A).
showList([A | X]) :-
    X \= [],
    write(A),
    write(', '),
    showList(X).

showNumber(Number) :-
    write(Number),
    write(': ').


showProof(Proof) :-
    showProof(1, Proof, _).

showProof(Number, axiom(L, R), Number) :-
    showNumber(Number),
    showSequent(L, R),    
    write('  -- Axiom'),
    nl.

showProof(Number, notLeft(L, R, Proof), Next) :-
    showProof(Number, Proof, Last),
    Next is Last+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- not L, line '),
    write(Last),
    nl.

showProof(Number, notRight(L, R, Proof), Next) :-
    showProof(Number, Proof, Last),
    Next is Last+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- not R, line '),
    write(Last),
    nl.

showProof(Number, andLeft(L, R, Proof), Next) :-
    showProof(Number, Proof, Last),
    Next is Last+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- and L, line '),
    write(Last),
    nl.

showProof(Number, andRight(L, R, ProofL, ProofR), Next) :-
    showProof(Number, ProofL, LastL),
    NextR is LastL+1,
    showProof(NextR, ProofR, LastR),
    Next is LastR+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- and R, lines '),
    write(LastL),
    write(' and '),
    write(LastR),
    nl.

showProof(Number, orRight(L, R, Proof), Next) :-
    showProof(Number, Proof, Last),
    Next is Last+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- or R, line '),
    write(Last),
    nl.

showProof(Number, orLeft(L, R, ProofL, ProofR), Next) :-
    showProof(Number, ProofL, LastL),
    NextR is LastL+1,
    showProof(NextR, ProofR, LastR),
    Next is LastR+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- or L, lines '),
    write(LastL),
    write(' and '),
    write(LastR),
    nl.

showProof(Number, impliesRight(L, R, Proof), Next) :-
    showProof(Number, Proof, Last),
    Next is Last+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- implies R, line '),
    write(Last),
    nl.

showProof(Number, impliesLeft(L, R, ProofL, ProofR), Next) :-
    showProof(Number, ProofL, LastL),
    NextR is LastL+1,
    showProof(NextR, ProofR, LastR),
    Next is LastR+1,
    showNumber(Next),
    showSequent(L, R),
    write('  -- implies L, lines '),
    write(LastL),
    write(' and '),
    write(LastR),
    nl.

turnstile :-
    write(' |- ').

test(1) :- test([and(a, and(b, c))], [and(and(a, b), c)]).

test(2) :- test([or(a, or(b, c))], [or(or(a, b), c)]).

test(3) :- test([or(a, and(b, c))], [and(or(a, b), or(a, c))]).

test(4) :- test([and(a, or(b, c))], [or(and(a, b), and(a, c))]).

test(5) :- test([implies(a, b), implies(b, c)], [implies(a, c)]).

test(5) :- test([implies(a, b), implies(b, c), implies(c, d)], [implies(a, d)]).

test(6) :- test([a], [not(not(a))]).

test(7) :- test([not(not(a))], [a]).

test(8) :- test([implies(a, b)], [implies(not(b), not(a))]).

test(9) :- test([implies(not(b), not(a))], [implies(a, b)]).

test(10) :- test([implies(a, c), implies(b, c)], [implies(or(a, b), c)]).

test(11) :- test([implies(a, b), implies(a, c)], [implies(a, and(b, c))]).

test(12) :- test([and(not(a), not(b))], [not(or(a, b))]).

test(13) :- test([not(or(a, b))], [and(not(a), not(b))]).

test(12) :- test([or(not(a), not(b))], [not(and(a, b))]).

test(13) :- test([not(and(a, b))], [or(not(a), not(b))]).

test(14) :- test([], [or(a, not(a))]).

test(15) :- test([], [or(implies(a, b), implies(b, a))]).

test(16) :- test([], [implies(implies(implies(a, b), a), a)]).

test(bad1) :- test([implies(a, b)], [implies(b, a)]).

test :- test(_), fail.
test.