CODEWITHSUNDEEP
prologunification
Milo Wielondek
Milo Wielondek

Reputation: 4352

Unification of expanded terms, double negation

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.

Upvotes: 1

Views: 162

Answers (1)

CapelliC
CapelliC

Reputation: 60014

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.

Upvotes: 1

Related Questions