
(negation)
&
(conjunction)

(disjunction)
>
(implication)
<>
(equivalence)
all x y ...
(universal quantification)
exists x y ...
(existential quantification)
f(x,y)
.
For the logical symbols we use infix notation with priorities as far as it makes sense.
The priorities are <>, >, , &, . That means
a & b  c > d <> e
is read as (((a & b)  c) > d) <> e
For all operators, right associativity is assumed, i.e.
a > b > c
is read as a > (b > c)
.
=>
to be an infix written right associative
binary (the xfy
) operator of priority 700
.
That means formula a => b=> c
are to be read as a => (b => c)
Furthermore the number 700 places the operator at a certain place in the operator hierarchy.
As a rule of thumb, if in an infix expression a op1 b op2 c
the
operator op1
has higher priority than op2
then it comes
higher in the formula tree, i.e. the parentheses are a op1 (b op2 c)
.
Besides xfy
there are a few more declarations allowed:
yfx
xfx
fy
fx
yf
xf
op(800, xfy, >).
op(850, xfy, <>).
op(790, xfy, ).
op(780, xfy, &).
op(500, xfx, ).
op(700, xfx, =).
op(700, xfx, !=).
(not equal)
op(750, xfx, =).
(satisfiability relation)