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)) ).

Answer 3

Logically, already in propositional logic, it does not follow (A v B) |- A and neither (A v B) |- B. The situation does also not change if you add ~(A & B).

Question is now whether clark completion or something else can add more default information, so that we finally have T |- A and T |- B. But by logic we would then have T |- A&B.

So I guess in a normal setting it is impossible to do, what you would like to do.

Bye

P.S.: A non normal setting would be for example to use a credulous consequence relation instead of a skeptical consequence relation. The skeptical consequence relation is:

T |- A iff forall M (if M |- T then M |- A)

The credulous consequence relation is:

T |~ A iff exists M (M |- T and M |- A)

It is possible to have T |~ A and T |~ B, but not T |~ A&B, your (A v B) & ~(A & B) without any default information is already such a theory.

P.S.S.: There are some ways to abuse a Prolog system for credulous reasoning, although Prologs foundation is skeptical reasoning. The trick is to use the identity T |~ A = ~(T |- ~A).

But before one can apply this to your example, one has to solve the problem of representing disjunction in Prolog. Some disjunction can be realized via the following identity and hypothetical reasoning:

(A v B -> C) == (A -> C) & (B -> C)

Answer 4

If introducing a named term is allowed in your 'target' logic, you could implement a dummy t/0:

t :- p(0), p(1), !, fail.
t :- p(0).
t :- p(1).

then if we have both

p(0).
p(1).

t/0 will fail.