-
(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)