/*   SYNOPSIS: Propositional Logic Gentzen System                          */
/*   +-----------------------------------------------------------------+   */
/*   | Propositional Logic Gentzen System, - Mohsin Ahmed, 23/Jan/1989 |   */
/*   |                                       884654 CS&E   IIT-Bombay  |   */
/*   | GPL(C) Mohsin Ahmed, http://www.cs.albany.edu/~mosh             |   */
/*   +-----------------------------------------------------------------+   */
/* Step1:  Try to falsify F by Calling v( [], [Formula], [], [] ).         */
/* Step2:  Reduce v([],[F],[],[]) to v([],[],List-of-p(i),List-of-p(i)),   */
/*         giving a tree, if every node is a axiom then Formula is valid   */
/*         else any non-axiom node gives a counter model.                  */
/*         Axiom leaves fail, counter-model leaves succeed.                */
/* Step3:  Check if v([],[],L3,L4) is a axiom then fail, else succeed      */
/*               with the counter model: L3 = true, L4 = false.            */
/* ----------------------------------------------------------------------- */
/* p(I) and atomic terms are propositions symbols.                         */
/* v( Verify-formulae-list,    Falisfy-formulae-list,                      */
/*    Verify-proposition-list, Falsify-proposition-list ).                 */
/* ----------------------------------------------------------------------- */

?- op( 70, xfy , -> ).                /*   Implication, right assoc        */
?- op( 60, xfx , #  ).                /*   Disjunction                     */
?- op( 50, xfx , &  ).                /*   Conjunction                     */
?- op( 40,  fx , ~  ).                /*   Negation                        */

/* ----------  Read Eval Loop  ------------------------------------------- */

validate       :-  repeat,
                   write('-) '), read(F),
                   validate(F),
                   F = false.

validate( F )  :-  v( [], [F], [], [] ), !.  /* - One solution is enough - */
validate( F )  :-  write('Valid'), nl.

/* ----------  Negation  ------------------------------------------------- */

v( [~A|L1], L2,   L3, L4 ) :-  v( L1, [A|L2], L3, L4 ).
v( L1, [~A|L2],   L3, L4 ) :-  v( [A|L1], L2, L3, L4 ).

/* ----------  Conjunction  ---------------------------------------------- */

v( [A&B|L1], L2, L3, L4 )    :-  v( [A,B|L1], L2, L3, L4 ).
v( L1, [A&B|L2], L3, L4 )    :-  v( L1, [A|L2], L3, L4 ).
v( L1, [A&B|L2], L3, L4 )    :-  v( L1, [B|L2], L3, L4 ).

/* ----------  Disjunction  ---------------------------------------------- */

v( L1, [A#B|L2], L3, L4 )    :-  v( L1, [A,B|L2], L3, L4 ).
v( [A#B|L1], L2, L3, L4 )    :-  v( [A|L1], L2, L3, L4 ).
v( [A#B|L1], L2, L3, L4 )    :-  v( [B|L1], L2, L3, L4 ).

/* ----------  Implication  ---------------------------------------------- */

v( L1, [A->B|L2], L3, L4 )   :-  v( [A|L1], [B|L2], L3, L4 ).
v( [A->B|L1], L2, L3, L4 )   :-  v( [B|L1], L2, L3, L4 ).
v( [A->B|L1], L2, L3, L4 )   :-  v( L1, [A|L2], L3, L4 ).

/* ----------  Proposition, p(i)  ---------------------------------------- */

v( [p(I)|L1], L2, L3, L4 )   :-  member( p(I), L3 ), !, v( L1, L2, L3, L4 ).
v( [p(I)|L1], L2, L3, L4 )   :-  v( L1, L2, [p(I)|L3], L4 ).
v( L1, [p(I)|L2], L3, L4 )   :-  member( p(I), L4 ), !, v( L1, L2, L3, L4 ).
v( L1, [p(I)|L2], L3, L4 )   :-  v( L1, L2, L3, [p(I)|L4] ).

/* ----------  Proposition, atomic  -------------------------------------- */

v( [A|L1], L2, L3, L4 )    :-  atomic(A), member(A,L4), !,
                               write('  Axiom: '),
                               write( L1 ), write( [A|L3] ),
                               write(' |- '),
                               write( L2 ), write( L4 ), nl,
                               !, fail.
v( [A|L1], L2, L3, L4 )    :-  atomic(A), member(A,L3), !, v( L1, L2, L3, L4 ).
v( [A|L1], L2, L3, L4 )    :-  atomic(A), v( L1, L2, [A|L3], L4 ).

v( L1, [A|L2], L3, L4 )    :-  atomic(A), member(A,L3), !,
                               write('  Axiom: '),
                               write( L1 ), write( L3 ),
                               write(' |- '),
                               write( L2 ), write( [A|L4] ), nl,
                               !, fail.
v( L1, [A|L2], L3, L4 )    :-  atomic(A), member(A,L4), !, v( L1, L2, L3, L4 ).
v( L1, [A|L2], L3, L4 )    :-  atomic(A), v( L1, L2, L3, [A|L4] ).

/* ----------  Fail if Axiom  -------------------------------------------- */

v( [], [], L3, L4 ) :-  axiom( L3, L4 ),
                        write('  Axiom: '),
                        write( L3 ), write(' |- '), write( L4 ), nl,
                        !, fail.

/* ----------  Succeed if Counter-Model found  --------------------------- */

v( [], [], L3, L4 ) :-  write('Falsified by : '),
                        write( L3 ), write(' = true,  '),
                        write(' |- '),
                        write( L4 ), write(' = false. '),
                        nl, !.

/* ----------  Axiom( L1, L2 ) if L1 intersection L2 is not empty  ------- */

axiom( [A|_], C )   :-  member( A, C  ), !.
axiom( [_|B], C )   :-  axiom(  B, C  ).

member( A, [A|_] )  :-  !.
member( A, [_|B] )  :-  member( A, B  ).

/* ----------------------------------------------------------------------- */