SCAN

Conventions and Notation

Logical Symbols
Precedence Declarations

Throughout this documentation we use the following conventions, see also Appendix A of Engel (1996):

Logical Symbols

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.

- (negation)
& (conjunction)
| (disjunction)
-> (implication)
<-> (equivalence)
all x y ... (universal quantification)
exists x y ... (existential quantification)

Terms and atoms are written in prefix notation, for example 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).

Precedence Declarations

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

op(700,xfy,=>)

It declares the operator => 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: binary infix operator, left associative
xfx: binary infix operator, the left and right neighbour operators must have
: lower priority (typically for equality =).
fy: prefix operator (as for example negation -p)
fx: prefix operator, the right neighbour must have lower priority (excludes -(-p)).
yf: postfix operator
xf: postfix operator, the left neighbour must have lower propority.

Our predefined operators are declared as: (Otter conventions)

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)

For more operator definitions, see the operator library operators.pl