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.

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)