Double Negation

[Bruce Colletti]

In the code below, I want to recognize x as belonging to [x, r, s, t] and must do so via double negation (this is part of a larger project).  not(not(x)) isn't recognized as x and I don't know what to do.  Ideally, I'd like to recognize ~~x, ~~~~x, etc. as x but don't know how. 

Any ideas?  Thanks.

Bruce

member(X, [X | _])  :-  !.

member(X, [_ | L])  :-  member(X,L).

main  :-  member(not(not(x)), [x, r, s, t]).

[Jan Wielemaker]

You cannot negate *terms* (=data). not(Term) is just a new term that
happens not to be part of the list. You can only negate *relations*
(=goals). So, you get

main :- not(not((member(x, [x,r,s,t]))).

Now, not/1 is old school because not/1 is not the logical _not_, but
rather `negation by failure' which is expressed by the \+ operator
(mnemonics: \ is negation in Prolog and + refers here to provable), so
you get

main :- \+ \+ member(x, [x,r,s,t]).

The next questions is what is the use of using `\+ \+ Goal`. I'll leave
that for you to chew on first :-)

Cheers --- Jan

[Bruce Colletti]

Thanks for the reply, Jan. 

What I seek is a way to recognize ~~x, ~~~~x, ~~~~~~x, etc. as the term x.  Mathematica can do so and I'm hoping SWI-Prolog can too.  It's just that I've never encountered this before in Prolog programming  and can't find anything to resolve the matter (or more likely, don't recognize what I may have already seen).

Bruce

[Kilian Evang]

On 05/03/2015 05:00 PM, Bruce Colletti wrote:
> What I seek is a way to recognize ~~x, ~~~~x, ~~~~~~x, etc. as the
> term x.

Ah, so you want to normalize logical expressions which are represented
as Prolog terms. To my best knowledge, SWIPL does not come with anything
to help with that particular task, here's a way to implement it
(provided your terms are always ground):

remove_double_negation(not(not(X)), Y) :-
!,
remove_double_negation(X, Y).
remove_double_negation(X, X).

Note that this only removes double negation from the very outside of the
term. If you need more normalization, consider implementing a full
conversion to conjunctive normal form.

Note also that when Prolog programmers read "double negation", they
usually think of double negation by failure, which Jan mentioned. It is
a useful technique in Prolog programming, but a very different thing.