[Albrecht Heeffer]
Home Logic Math Publications Shogi Sites About Me
         
Gentzen-style sequent calculus prover

Gentzen-style sequent calculus prover for propositional logic and paraconsistent logic CLUN

based on Andrzej Wisniewski's Socratic proofs

for proving:
{((p ≡ q) ∨ ¬r), ¬s, (s ∨ s) ≡ (q ⊃ s)} |- q ∧ (p ∨ s), use
[(p<=>q) v -r,-s, (s v s)<=>(q=>s)], q&(p v -r)
Premisses:Conclusion:

Press send for the proof of this example, or edit the input fields for a different problem

For proving a theorem ((p∧~p)∨(q∧~q))∨(((r⊃(p∨q)∧(~p∧~q))⊃~r) : (example in CLuN):

Press send for the proof of this example, or edit the input fields for a different problem
Some guidelines:
'-' is classic negation ¬
'~' is paraconsistent negation
Always use a space before a '-' and '~'
For '¬¬p', use brackets: -(-p)
use a space before and after disjunction ∨
The proof is shown using Gentzen-style sequents with a number indicating the level on which they appear
See: Andrzej Wisniewski (2004) "Socratic proofs", Journal of Philosophical Logic  
         

The core program in Prolog:

% pr(P,G): Prove G from premisse set P
pr(X, -(-G))   :- pr(X,G), !.
pr(X,F => G)   :- append(X,[F],X1), pr(X1,G),!.
pr(X,F v G)    :- append(X,[-(F)],X1), pr(X1,G), !.
pr(X,F & G)    :- pr(X,F), !, pr(X,G), !.
pr(X,-(F & G)) :- append(X,[F],X1), pr(X1,-(G)), !.
pr(X,-(F v G)) :- pr(X,-(F)), !, pr(X, -(G)), !.
pr(X,-(F=> G)) :- pr(X,F), !, pr(X, -(G)), !.
pr(X,F<=>G)    :- pr(X,F=>G), !, pr(X,G=>F), !.
pr(X,-(F<=>G)) :- append(X,[F=>G],X1), pr(X1,-(G=>F)), !.

% Terminating conditions
pr(X,F) :- memberchk(F,X), !.
pr(X,_) :- member(F,X),  member(-F,X), !.
pr(X,_) :- member(-F,X), member(F,X), !.

pr(X,Y) :- pick(-(-F),X,X1,X2),    append(X1,[F|X2],Z), pr(Z,Y), !.
pr(X,Y) :- pick(F & G,X,X1,X2),    append(X1,[F|[G|X2]],Z), pr(Z,Y),!.
pr(X,Y) :- pick(-(F v G),X,X1,X2), append(X1,[-(F)|[-(G)|X2]],Z), pr(Z,Y),!.
pr(X,Y) :- pick(F<=>G,X,X1,X2),    append(X1,[F=>G|[G=>F|X2]],Z), pr(Z,Y),!.
pr(X,Y) :- pick(-(F<=>G),X,X1,X2), append(X1,[-(F=>G)|[-(G=>F)|X2]],Z), pr(Z,Y),!.
pr(X,Y) :- pick(-(F=> G),X,X1,X2), append(X1,[F|[-(G)|X2]],Z), pr(Z,Y),!.
pr(X,Y) :- pick(-(F & G),X,X1,X2), append(X1,[-F|X2],Z1), 
	   append(X1,[-G|X2],Z2),  pr(Z1,Y), !, pr(Z2,Y), !.
pr(X,Y) :- pick(F v G,X,X1,X2),    append(X1,[F|X2],Z1), 
	   append(X1,[G|X2],Z2),   pr(Z1,Y), !, pr(Z2,Y), !.
pr(X,Y) :- pick(F =>G,X,X1,X2),    append(X1,[-(F)|X2],Z1), 
	   append(X1,[G|X2],Z2),   pr(Z1,Y), !, pr(Z2,Y), !.

% pick(+E,+L,-H,-T)
% removes element E from list L and returns the head before
% the element and the tail after the element
pick(H,[H|T],[],T) :- !.
pick(H,[E|T],[E|L1],L2) :- pick(H,T,L1,L2), !.
© 2004 Albrecht Heeffer