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

Limestone

ground/2 has really no meaning. – Lampyrid

The meaning of a relation is defined by its ground interpretation. That is the set of ground terms that hold for this relation. So ground/2 must be the constant true. There is no situation where it is false. – Lampyrid

Oh I see !!, so you mean writing something like: \\+(Goal) :- when(ground(Goal), \+Goal). ??? – Limestone

That makes sense. – Lampyrid

Could this be considered as pure ?? – Limestone

Well, it is a form of non-monotonic extension. Regardless of its merit, it is extremely limited by insisting on groundness. Most of the time the answer would be a floundering goal which tells you exactly nothing. Think of the goal \\+( [] = [X|Xs]) which is not ground, thus you would never get a response, whereas dif([], [X|Xs]) just snugly succeeds. – Lampyrid

Very nice point !! thanks @Lampyrid this pretty much answers my question since it proves that this is not the right approach. Do you have any approach in mind, or logical negation may be impossible?? – Limestone

BTW, your question merits a much more detailed answer, which would start with 1972 and Prolog 0 and goes about everything that happened up to now including ASP but also the pure programming in Prolog itself. – Lampyrid

I understand your point, I think there has been so much research that searching seems endless, thanks for your replies, appreciate it !!! – Limestone

Answer 1

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.

Eatables

Prolog is not classical, but far more like this Intuitionistic Logic, where the label "true" means "provable/there is evidence for" (as opposed to the God-emitted statement "true" of classical logic), a situation embraced by Lambda Prolog. I don't understand why this isn't the first thing being said in every book on Prolog. – Indefectible

Intuitionistic logic would require "Law of noncontradiction: ~(p /\ ~p)", which is provable in intuitionistic logic. So Prolog is below intuitionistic logic, one can show that it is a fragment of so called minimal logic. – Eatables

Answer 2

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.

Avlona

I just would like to ask how the whole project of "making Prolog classical" fits with the fact that first-order logic is not decidable. – Chrysotile