Problem with redefining operators for propositional logic

Hi, teaching myself prolog I found an interesting article about how to rewrite Prolog operators to represent propositional logic, so that you can formulate propositions like:

P = t('A is a knight'),Q = t('B is a knight'), P <=> ~P ^ Q.

I created this notbook on swish with the complete code.

It redefines the operators two times and aliases them. But the not alias ~, the implies and the equiv alias don´t work and I get an “operator expected” error in swish and swipl. The code looks ok, but what am I missing, or misunderstanding?

% infix syntax for logical connectives   
:- op(400,xf,not).
:- op(500,xfx,and).
:- op(500,xfx,or).
:- op(600,xfx,implies).
:- op(600,xfx,equiv).

% logical operators for the connectives
:- op(400,xf,~).
:- op(500,xfx,^).
:- op(500,xfx,v).
:- op(600,xfx,=>).
:- op(600,xfx,<=>).

% aliases of the connectives
~P :- not P.
P ^ Q :- P and Q.
P v Q :- P or Q.
P => Q :- P implies Q.
P <=> Q :- P equiv Q.
1 Like

Try fy instead of xf. What I use when I code propositional logic routines:

%%% 2.1 The syntax of propositional logic                                       
%%% I use the built in parser and change/augment the Prolog operators to handle
%%% propositional logic.                                                        
:-op(0, fy, ~).
:-op(200, fy, ~).                   % Negation                                  
:-op(0, yfx, (/\)).
:-op(0, xfy, (/\)).
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which \
is yfx)                                                                         
:-op(0, yfx, (\/)).
:-op(0, xfy, (\/)).
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which \
is yfx)                                                                         
:-op(0, xfy, ==>).
:-op(600, xfy, ==>).                % Implication                               
:-op(0, xfy, <=>).
:-op(700, xfy, <=>).                % Equivalence                               

Top tip: to test your understanding of operator precedence try this query

read(X), write_canonical(X).

and give it some typical input and make sure it works as you think it should. Here’s an example from the manual of my Prolog system:

| ?- op(200, xfx, @).
% yes
| ?- op(300, xfx, &).
% yes
| ?- write_canonical(a @ b & c), nl.
1 Like