SCAN
Conventions and Notation
Throughout this documentation we use the following conventions, see also
Appendix A of
Engel (1996):
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)
.
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
SCAN Home
Forms:
Basic Form 
Correspondences Form 
Circumscription Form 
Help
Documentation:
Theory 
Computing Correspondences 
Computing Circumscription 
The System 
Conventions 
Syntax 
Literature
Maintained by
schmidt@cs.man.ac.uk.
Last modified: 7 Nov 2000
Copyright © 19952000 by MaxPlanckInstitut
für Informatik. All rights reserved.
Imprint  Data Protection