Logical negation in Prolog ~ a = (a => f)

Help! Data Structure
1 
% =========================================================================
%  TPTP Operators 
% =========================================================================
:- op( 500, fy, ~).             % negation
:- op(1000, xfy, &).            % conjunction
:- op(1100, xfy, '|').          % disjunction
:- op(1110, xfy, =>).           % conditional
:- op(1120, xfy, <=>).          % biconditional
:- op( 500, fy, !).             % universal quantifier:  ![X]:
:- op( 500, fy, ?).             % existential quantifier:  ?[X]:
:- op( 500, xfy, :).            % quantifier separator

With the previous operators, it would be useful for a Prolog program to read any ~ a as (a => f) with f meaning falsum or bot. So:

term_expansion(~ ~ A, Result) :-
    !,
    expand_negations(A, A1),
    Result = ((A1 => f) => f).

term_expansion(~ A, Result) :-
    !,
    expand_negations(A, A1),
    Result = (A1 => f).

expand_negations(~ ~ A, ((A1 => f) => f)) :-
    !,
    expand_negations(A, A1).

expand_negations(~ A, (A1 => f)) :-
    !,
    expand_negations(A, A1).

expand_negations((A | B), (A1 | B1)) :-
    !,
    expand_negations(A, A1),
    expand_negations(B, B1).

expand_negations((A & B), (A1 & B1)) :-
    !,
    expand_negations(A, A1),
    expand_negations(B, B1).

expand_negations((A => B), (A1 => B1)) :-
    !,
    expand_negations(A, A1),
    expand_negations(B, B1).

expand_negations(A, A) :-
    atomic(A).

But :

 ?- term_expansion(~ ~  (~ a | a), X).
X = (((a=>f)| a=>f)=>f).

?- term_expansion(~ (~  (~ a | a)), X).
X = (((a=>f)| a=>f)=>f).

are clearly wrong .

A solution would be helpful.

Best wishes,
Jo.

2

I don’t think you need to handle double negation, indeed the code seems to work fine without that.

But mind your operator precedence levels, as if you write the term canonically, you can see it’s the right term:

?- term_expansion(~ (a | b), X), write_canonical(X), nl.
=>('|'(a,b),f)
X = (a|b=>f).

(I have not tested the code with more complex cases, anyway it looks fine at an inspection.)

1 Like
3

Hi, you are right. But it is a kind of “display bug” . I had a Prolog file to show the problem . And I consider that my perplexity was understandable, but you gave the explanation. SWI-Prolog shoud correct this to get the solution. :slight_smile:

demo_bug.pl (1,4 Ko)

4

But it is a kind of “display bug” .

IMO, it is not a bug: you did declare the conditional at a higher level than disjunction… together with the fact that plain Prolog printing is supposed not to add unneeded parentheses – nor spacing, and especially the spacing is peculiar in Prolog compared to most other languages, as the base case is that there is no spacing between tokens.

1 Like