prolog first order logic

Question

I'm trying to find a way to put the following first order logic expression into Prolog:

(p(0) or p(1)) and not (p(0) and p(1)) 

This means that it should respond in the following way to queries:

?- p(0)
Yes.
?- p(1)
Yes.
?- p(0),p(1).
No. 

I tried to translate the logical expression:

(p(0) or p(1)) and not (p(0) and p(1)) <=>
(not p(0) -> p(1)) and (p(0) -> not p(1)) <=>
p(0) <-> not p(1) 

Using Clarks completion (that states that every definitional theory can be put in a logical program by giving the if-halves), I can obtain:

p(0) :- not p(1). 

Unfortunately, this resulting theory is only sound (it will not derive false information), but not complete (for example: p(1) cannot be derived). This is a consequence of Clarks theorem.

Does anybody know if there is a better solution? Thanks!

Answer 1

This is subtle, but you are actually wrong. You shouldn't expect p(0) to be entailed. Entailment would require that p(0) is true in all models of the theory. But this theory has two models {p(1)} and {p(0)}.

This is extensively studied in literature. As you correctly pointed out Clark's completion fails to handle these cases. What's worse, SLDNF falls into infinite recursion for

p(0) :- not p(1). 
p(1) :- not p(0).

Which is the most appropriate translation to definite clauses of your theory.

I'll spare you pointers on the definition of different semantics but if you want a quick and practical solution I suggest switching to Answer Set Programming.

Here's the link to my favourite solver (the guide is also nice and self-contained): http://www.cs.uni-potsdam.de/clasp/

Enjoy!

Answer 2

In Prolog, if both p(0) and p(1) succeed, then p(0),p(1) can not fail.

That means you would have to build your own little interpreter, devise ways to represent your goals and rules for it, and ask in it your questions, like

?- is_true( (p(0),p(1)) ).