Menu
Because of the problems of negation-as-failure, negation in Prolog is represented in modern Prolog interpreters using the symbol \+ , which is supposed to be a mnemonic for not provable with the \ standing for not and the + for provable.
A single underscore ( _ ) denotes an anonymous variable and means "any term". Unlike other variables, the underscore does not represent the same value everywhere it occurs within a predicate definition. A compound term is composed of an atom called a "functor" and a number of "arguments", which are again terms.
Not Relation in Prolog So it means that when a statement is true, then not(statement) will be false, otherwise if the statement is false, then not(statement) will be true. not(P) :- P, !, fail ; true. So if P is true, then cut and fail, this will return false, otherwise it will be true.
=:= expression is meaning of exactly equal. such as in JavaScript you can use === to also see if the type of the variables are same. Basically it's same logic but =:= is used in functional languages as Prolog, Erlang.
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??).
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With