Unification of expanded terms, double negation

Question

I need to introduce a predicate that will let me negate atoms. So far I have neg(Premise) :- \+ Premise., which gives me following results:

?- assert(a).
true.

?- a.
true.

?- neg(a).
false.

?- neg(neg(a)).
true.

That makes sense and all is dandy, until I tried unification. For instance

[a,_] = [a,123]. returns true.

while

[a,_] = [neg(neg(a)),123]. returns false..

How can I solve this so that the neg(neg(X)) part is being evaluated or otherwise unified with X (since they both are logically equivalent)? So basically, I need X=neg(a), a=neg(X). to succeed.

Edit I found an explanation as to why not(not(<expression>)) is not equivalent to <expression> in prolog. Since <expression> succeeds, not(<expression>) fails. When a goal fails the variables it instantiated get uninstantiated. (source, slide 14).

I'm still not sure how to get around this though.

Prolog isn't executing a predicate like a function and returning a result. It instantiates uninstantiated variables where possible and checks for truth value. So neg(neg(a)) isn't doing what you might think. It's instantiating Premise with neg(a) and then evaluating \+ neg(a). ultimately determining the truth value of neg with neg(a) given as a term. Your array example attempts to unify a with neg(neg(a)) and fails because they are both fully instantiated terms that don't match. You'll need to be more clear on what you're trying to do in order to 'get around it'. — lurker
@mbratch I see. Basically what I want is: if l(a). holds, then l(neg(neg(a)). should succeed too. Does that make sense? — Milo Wielondek
Yes. You want a predicate that says, l(neg(neg(X))) :- l(X). — lurker
@mbratch and if I want that to hold for all predicates? Copy & paste and substitute l for each predicate seems like not the most efficient solution. — Milo Wielondek
Indeed, if you are looking for a general solution, that wouldn't be efficient. I'm a little curious as to what's driving the scenario to be so prevalent. Some refactoring may be necessary. — lurker

CapelliC CapelliC · Accepted Answer · 2013-11-05T19:10:22

Reification of truth value will work on your simple case:

4 ?- [user].
|: reify(P, V) :- call(P) -> V = 1 ; V = 0.
% user://1 compiled 0.03 sec, 2 clauses
true.

5 ?- reify(true, V), reify(\+ \+ true, U), V = U.
V = U, U = 1.

using your symbols:

6 ?- [user].
|: a.
|: neg(P) :- \+ P.
% user://2 compiled 0.02 sec, 3 clauses
true.

7 ?- reify(a, V), reify(neg(neg(a)), U), V = U.
V = U, U = 1.

not sure how well this will merge with your code.

Unification of expanded terms, double negation

1 Answers