 # 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.
&(@(a,b),c)
``````
1 Like