Logical Negation in Prolog

Question

I've read quite a bit about Prolog's Negation by Failure where Prolog in order to prove that \+Goal holds tries to prove that Goal fails.

This is highly connected with CWA (close world assumption) where for example if we query \+P(a) (where P is a predicate of arity 1) and we have no clues that lead to prove P(a) Prolog assumes (due to CWA) that not P(a) holds so \+P(a) succeeds.

From what I've searched this is a way to solve classical logic weakness where if we had no clue about P(a) then we could not answer whether \+P(a) holds.

What described above was the way of introducing non-monotonic reasoning in Prolog. Moreover the interesting part is that Clark proved that Negation by Failure is compatible/similar with classical negation only for ground clauses. I understand that for example:

X=1, \+X==1.: should return false in Prolog (and in classical Logic).

\+X==1, X=1.: should return false in classical logic but it succeeds in Prolog since the time that NF is examined X is not bound, this differs from classic-Pure Logic.

\+X==1.: should not give any answer in classical logic until X is bound, but in Prolog it returns false (possibly to break weakness of classical logic) and this is not same/compatible with pure Logic.

My attempt was to simulate classic negation, thanks to @false's suggestions in comments, current implementation is:

\\+(Goal) :- when(ground(Goal), \+Goal). 

Some testing:

?- \\+(X==1).
when(ground(X), \+X==1).

?- X=1, \\+(X==1).
false.

?- \\+(X==1), X=1.
false. 

My question:

Is the above a correct interpretation of classical negation? (Are there any obvious corner cases that it misses?? also I'm concerned about Logic Purity when using when/2, is it safe to assume that the above is pure??).

Answer 1

In SWI-Prolog, it is possible to implement the rules of inference for classical logic in Constraint Handling Rules, including de Morgan's laws and the law of noncontradiction:

:- use_module(library(chr)).
:- chr_constraint is_true/1.
:- chr_constraint animal/2.
:- initialization(main).
:- set_prolog_flag('double_quotes','chars').

is_true(A),is_true(A) <=> is_true(A).
is_true(A=B) ==> A=B.
is_true(A\=B) ==> not(A=B).
is_true(not(A)),is_true(A) ==> false.
is_true(not((A;B))) ==> is_true((not(A),not(B))).
is_true(not((A,B))) ==> is_true((not(A);not(B))).
is_true((A,B)) ==> is_true(A),is_true(B).
is_true((A;B)) ==> is_true(A),(is_true(B);is_true(not(B)));is_true(B),(is_true(A);is_true(not(A))).
is_true(not(not(A))) ==> is_true(A).

Then, you can use the solver like this:

is_true(animal(X,A)),is_true(animal((Y,A))) ==> X \= Y,false;X==Y.
is_true((A->B)) ==> is_true(((A;not(A)),B));is_true(((not(A);A),not(B))).

main :- is_true(((X=cat;X=dog;X=moose),(not((animal(dog,tom);animal(moose,tom))),animal(X,tom)))),writeln(animal(X,tom)).

This program prints animal(cat,tom).

But this formula could be solved more efficiently using a different algorithm, such as DPLL.

Answer 2

Prolog cannot do classical negation. Since it does not use classical inference. Even in the presence of Clark completion, it cannot detect the following two classical laws:

Law of noncontradiction: ~(p /\ ~p)

Law of excluded middle: p \/ ~p

Here is an example, take this logic program and these queries:

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

The Clark completion of the logic program is as follows and the negation as failure query execution yields the following:

   p <-> p

   loops

   loops

Clark completion adresses the issue of predicate definitions and negative information. See also section 5.2 Rules and their Completion. On the other hand, when no predicate definitions are around, CLP(X) can sometimes do both laws, when a negation operator is defined deMorgan style. Here is a negation operator for CLP(B):

?- listing(neg/1).
neg((A;B)) :-
    neg(A),
    neg(B).
neg((A, _)) :-
    neg(A).
neg((_, A)) :-
    neg(A).
neg(neg(A)) :-
    call(A).
neg(sat(A)) :-
    sat(~A).

And here is some execution:

?- sat(P); neg(sat(P)).
P = 0 
P = 1.
?- neg((sat(P), neg(sat(P)))).
P = 0 
P = 1.

CLP(X) will also have problems when the negation affects domains, that are usually finite and that would then get infinite. So for example a constraint such as (#=)/2, ... shouldn't be a problem, since it can be replaced by a constraint (#\=)/2, ... .

But negation for CLP(FD) will usually not work when applied to constraints (in)/2. The situation can slightly be mitigated if the CLP(X) system offers reification. In this case the disjunction can be rendered a little bit more intelligent than just using Prolog backtracking disjunction.