Sequent calculus in prolog

Question

I'm really new programming in Prolog. I have to program the rules of sequent calculus in Prolog, which I think, I did right. The code should return true if the formula is valid and false if it's not. Here is my code:

code as a picture

And this returns true if the formula is valid.

But if I run the code with a not valid formula it never ends and I really don't know how I can fix it.

The query -? sc([ ],[ (neg ((neg p)or neg (neg p)))]). should return false, because that formula is not valid.

I would appreciate any help with this.

Please don't post your code as an image. Post it as text so that we can work with it. Most users will not attempt to answer a question without code as text. — Enigmativity
Please show what query you ran and what result you expected. — lurker
Please edit your question and put the actual text of your code there. Select it all and click the {} button to format it properly. Do you know that [ (neg ((neg p)or neg (neg p)))] is a list of one element? — lurker

Mostowski Collapse Mostowski Collapse · Accepted Answer · 2019-03-02T19:43:00

There is an error in the disjunction rule. Further the permutation rule is a structural rule:

G, A, B, D |- C
---------------
G, B, A, D |- C

And you should code it, so that it doesn't loop. But now this can exactly happen. There is a simple trick, maybe you wanted to implement it, only swap in non-atoms to the fronts.

Here is a cleaned up version:

:- use_module(library(basic/lists)).

sc([neg(A)|L],R) :- !, sc(L,[A|R]).
sc(L,[neg(A)|R]) :- !, sc([A|L],R).
sc(L,[or(A,B)|R]) :- !, sc(L,[A,B|R]).
sc([or(A,B)|L],R) :- !, sc([A|L],R), sc([B|L],R).
sc([A|L],R) :- atom(A), select(B,L,H), compound(B), !, sc([B,A|H],R).
sc(L,[A|R]) :- atom(A), select(B,R,H), compound(B), !, sc(L,[B,A|H]).
sc(L,R) :- member(A,L), member(A,R), !.

And here are some runs:

Jekejeke Prolog 3, Runtime Library 1.3.5
(c) 1985-2019, XLOG Technologies GmbH, Switzerland

?- sc([],[neg(or(neg(p),neg(neg(p))))]).
No
?- sc([],[or(neg(p),neg(neg(p)))]).
Yes

Remarks: I have moved the identity rule to the end, so it will only hit atoms. I have placed cuts, which is justified by some inversion lemmas for classical logic. Might not work for other logics or when non-ground problems are posed.

Sequent calculus in prolog

2 Answers