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!

Blasphemy

What is the semantics for your language? Is it "no contradiction"? "is provable"? When you say p(0), are you asking it of the system, or telling it to the system? Is everything non-specified assumed to be false (like in Prolog's closed world) or can it take on any value? – Baksheesh

The semantics I am using is Clark´s Completion. The logical meaning of the queries is: "is provable", so ?- p(0) is equivalent to asking whether p(0) can be proved from the theory. – Blasphemy

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!

Diatomic

Thanks! But I don't think I am wrong, in what exactly do you think I am wrong? I have actually decided to switch to ASP a week ago, it's great! – Blasphemy

I was referring to the expectation that p(1) and p(0) are consequences of your theory. That is true only under "brave" semantics as opposed to the "skeptical" natural semantics of Prolog. – Diatomic

Thanks, I think I understand it now. p(0) and p(1) are not consequences of my theory, because they are not true in all models (skeptical). Instead, they are only true in some models (brave). – Blasphemy

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

Baksheesh

I understand what you are saying, but why does it hold? – Blasphemy

I meant it as a query, in an hypothetical evaluator/predicate is_true that would implement your semantics. It would reply either e.g. Yes or No. I think others answered your question here more specifically; try asking them too (put a comment under an answer so the answer's author will receive it). :) – Baksheesh

Answer 3

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.

Aubade

Answer 4

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)

Waldack

the only sense I could make of it is if we interpret the responses given by OP as "does not contradict", or "is consistent". So, claiming A is consistent with knowledge K that (A v B) ^ ~(A ^ B), and so is claiming B, but not claiming both A ^ B. But Prolog's semantics is "is entailed" or, "is provable", not "is consistent". – Baksheesh

Entailment and consistency are related. T |- A is equivalent to T, ~A is inconsistent. But you are right, in a non-normal setting, we could have T |- A and T |- B but not T |- A&B. See new edit. – Waldack