Conventions and Notation
Throughout this documentation we use the following conventions, see also
Appendix A of
We tried to use a consistent notation for logical formulae.
Since the basis of our implementation is the theorem prover Otter,
we stick at the Otter notation in the documentation as well as for the
input syntax for the various interfaces to SCAN.
Terms and atoms are written in prefix notation, for example
all x y ... (universal quantification)
exists x y ... (existential quantification)
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).
In the correspondence theory application of SCAN, the user can define new
operators which are not known to the system.
Since priority declarations for the operators make formulae much more readable,
we provide the Prolog type priority declarations. A typical such declaration is
It declares the operator
=> to be an infix written right associative
xfy) operator of priority
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
op1 has higher priority than
op2 then it comes
higher in the formula tree, i.e. the parentheses are
a op1 (b op2 c).
xfy there are a few more declarations allowed:
Our predefined operators are declared as: (Otter conventions)
- binary infix operator, left associative
- binary infix operator, the left and right neighbour operators must have
- lower priority (typically for equality =).
- prefix operator (as for example negation -p)
- prefix operator, the right neighbour must have lower priority (excludes -(-p)).
- postfix operator
- postfix operator, the left neighbour must have lower propority.
For more operator definitions, see the operator library
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)
Basic Form |
Correspondences Form |
Circumscription Form |
Computing Correspondences |
Computing Circumscription |
The System |
Last modified: 05 Aug 13