First-order logic prologue

Question

I am trying to find a way to include the following logical first-order expression in Prolog:

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

This means that it should respond as follows to requests:

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

I tried to translate a boolean 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 the Clarks termination (which states that any theory of definition can be placed in a logical program, giving if-halves), I can get:

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

Unfortunately, this resulting theory sounds only (it will not output false information), but not complete (for example: p (1) cannot be obtained). This is a consequence of Clarks's theorem.

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

Answer 1

This is subtle, but you are actually mistaken. You should not expect p (0). Completion will 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 widely studied in the literature. As you pointed out correctly, Clark's completion does not cope with these cases. Even worse, SLDNF falls into infinite recursion for

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

This is the most suitable translation into certain provisions of your theory.

I will spare you pointers to defining different semantics, but if you want a quick and practical solution, I suggest switching to programming a set of answers.

Here is a link to my favorite solver (the manual is also nice and self-sufficient): http://www.cs.uni-potsdam.de/clasp/

Enjoy it!

Answer 2

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

This means that you will need to create your own little interpreter, develop ways to present your goals and rules for it, and ask your questions in it, for example

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

Answer 3

If you introduce the entered term into the logic “target”, you can implement 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.

Answer 4

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

The question is whether the completion of the clark is completed or something else, you can add additional default values ​​for the information, so that we finally have T | - A and T | - B. But logically we will have T | - A & B.

So, I think that in a normal situation it is impossible to do what you would like to do.

Bye

PS: A non-standard setting will, for example, use a gullible consequence, not a skeptical consequence. Skeptical attitude of the consequences:

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

Permissible ratio of effects:

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

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

PSS: There are several ways to abuse the Prolog system for gullible argumentation, although the basis of Prologs is a skeptical argument. the trick is to use the identity T | ~ A = ~ (T | - ~ A).

But before you apply this to your example, you need to solve the problem of presenting a disjunction in Prolog. Some disjunction can be realized using the following identity and hypothetical reasoning :

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