Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
/* * Problem from: * https://swi-prolog.discourse.group/t/4693 * Unfortunately no MathJax yet. */ % ----------------------------------------------------------------- % 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 % ----------------------------------------------------------------- prove0(F, P) :- prove([] > [F], P). % ----------------------------------------------------------------- % axiom prove(G > D, ax(G > D, A)) :- member(A,G), member(A,D), !. % conjunction prove(G > D, land(G > D, P) ) :- select( (A & B) ,G,G1), !, prove([A , B | G1] > D, P). prove(G > D, rand(G > D, P1,P2)) :- select( (A & B) ,D,D1), !, prove(G > [A|D1], P1), prove(G > [B|D1], P2). % disjunction prove(G > D, lor(G > D, P1,P2)) :- select((A | B),G,G1), !, prove([A|G1] > D, P1), prove([B|G1] > D, P2). prove(G > D, ror(G > D, P)) :- select( (A | B),D,D1), !, prove(G > [A,B|D1], P ). % implication prove(G > D, limpl(G > D, P1,P2)) :- select((A => B),G,G1), !, prove(G1 > [A|D], P1), prove([B|G1] > D, P2). prove(G > D, rimpl(G > D, P)) :- select((A => B),D,D1), !, prove([A|G] > [B|D1], P). % negation prove(G > D, lneg(G > D, P)) :- select( ~A,G,G1), !, prove(G1 > [A|D], P). prove(G > D, rneg(G > D, P)) :- select(~A ,D,D1), !, prove([A|G] > D1, P). /** <examples> ?- prove0((('A' & 'B') => 'A'), Proof). */