SCAN

The System



SCAN/Otter: The Program

Our SCAN implementation is a modified version of the Otter theorem prover developed by Bill McCune at Argonne National Laboratory. Although we hope that you can use our interface without understanding Otter, for a more detailed understanding of the system, it is quite helpful to read the Otter manual and get used to the Otter program.

The main modifications in Otter itself are the integration of the constrained resolution rule, the purity deletion operation and the particular resolution strategy SCAN requires. The unskolemization routine which has been implemented by Thorsten Engel is an extra module.

SCAN/Otter simply reads an input file containing the full specification of the problem and it generates an output file with the protocol of the run and the final result.

The input file consists of three main parts:

The SCAN control parameters

pred_list[predicates].
predicates is a comma separated list of the predicates to be eliminated.
set(unskolemize).
the result is to be unskolemized (if not, just omit this command).
set(negate).
the unskolemized result is to be negated (if not, just omit this command).
The SCAN control parameter block has to be finished with the line:
;.

Otter control parameters

The main Otter control parameters are
set(binary_c_res).
activates the special constrained resolution rule
set(c_factor).
activates the special constrained factorization rule
set(print_lists_at_end).
causes the final set of clauses to be printed
set(process_input).
causes C-factorization to be applied to the input clauses as well. SCAN is definitely incomplete without this.
Useful optional parameters are
set(unit_deletion).
activates the simplification (p & (-p | q)) <-> q (very useful)
clear(print_kept).
suppresses output of the resolvents.
assign(max_seconds,n).
n is an integer > 0, aborts the processing after n seconds (not always reliable).
set(prolog_style_variables).
If this flag is set, a name with no arguments in a clause is a variables if and only if it starts with an upper case letter from A trough Z, or with _.
set(display_terms).
If this flag is set all clauses and terms are printed in pure prefix form (useful for debugging purposes).
Some of the other standard Otter parameters might be useful in particular cases, but we do not guarantee that they do not influence SCAN negatively.

Formulae

Otter maintains different lists of formulae. SCAN uses two of these lists. The 'sos' list is the list of active formulae which are processed by SCAN. The 'usable' list is an additional list of formulae which are used for simplifying the resolvents. Here you can make use of a background theory in your domain. Using the 'usable' list means logically:
'usable formulae' -> (input(SCAN) <-> output(SCAN))
That means SCAN computes formulae which are only equivalent to the second-order input formula modulo the background theory. A typical example is the reflexivity clause all x (x = x). as part of the usable list. This causes all resolvents with literals s = s to be subsumed. The 'usable' list should of course NOT contain formulae with the predicates to be eliminated.

The two different lists are specified in one of the following four ways:

list(usable).   formula_list(usable).     
...             ...                       
end_of_list.    end_of_list.              

list(sos).      formula_list(sos).
...             ...
end_of_list.    end_of_list.
The list(...). form requires the formulae to be presented in clause syntax, whereas the formula_list(...). form accepts full first-order predicate logic syntax. Each formula has to be terminated with a period. It is possible to have a part of the sos list (and the usable list as well) in clause syntax and another part in formula syntax.

For more details on the clause and formula syntax see SCAN: Syntax for formulae.

An example for a typical input file is

pred_list[p].
set(unskolemize).
set(negate).
;.

set(binary_c_res).
set(c_factor).
assign(max_seconds, 100).
set(print_lists_at_end).
set(unit_deletion).
clear(print_kept).
set(process_input).

formula_list(sos).
(exists a all w ((r(a,w) -> p(w)) & -p(a))).
end_of_list.
In a Unix environment, SCAN can be activated with the Unix command
scan < input_file >! output file
provided, SCAN is properly installed.

The Prolog Interface

A quantifier elimination task usually comes as a subproblem of another problem. Therefore we provide interfaces to SCAN which turn particular problems into quantifier elimination problems and prepare the input file for SCAN. These interfaces are written in Prolog. To be compatible with as many Prologs as possible, we used the Clocksin Mellish fragment. The program works at least with Quintus Prolog, SICStus Prolog, SWI Prolog and Eclipse.

Using Prolog for writing such an interface has advantages and disadvantages. The advantages are that algorithms for manipulating logical formulae are very easy to write in Prolog, and quite easy to understand and to modify. However, the formulae to be manipulated have to be fed into the Prolog system. And this means they have to be parsed by the Prolog parser, which in turn means that their syntactic structure must follow the Prolog conventions. This is fine for terms and clauses, but for first-order formulae with quantifiers, the Prolog term structure differs from the quite well readable Otter syntax. As an example, the Otter parseble formula

all x y z (p(x,y) & p(y,z) -> q(x,z)).
would look in Prolog syntax
all(x,all(y,all(z,p(x,y) & p(y,z) -> q(x,z)))).
In order to have a uniform and easy to use interface, we allow all formulae to be written in the more convenient Otter syntax, but enclosed in quotes. That means the above formula is to be written as
all x y z (p(x,y) & p(y,z) -> q(x,z))
The quotes cause Prolog to parse this as a Prolog atom and then a special parser can turn it into a proper Prolog term.

Therefore the following conventions hold for feeding formulae into the Prolog interface: If the formula's structure is parseble by the standard Prolog parser, then there is no problem. Just write it as a Prolog term. If the formula is not parseble by the standard Prolog parser, but by Otter, then enclose it in quotes.

In order to understand the syntax error messages, you should know the following: The Otter syntax is not that much different from the Prolog term syntax. Therefore we tokenize the Otter formulae, reconstruct at the token level the term structure for the quantifiers and then feed this into the Prolog parser. Since Prolog does not have something like a `read from string', and we did not want to include the portable read function, because this is more code than the whole other Prolog program, we just write the modified string to a temporary file and then read it back into the system.

Syntax errors may therefore be detected in these two stages, either during the process of reconstructing the term structure, or when reading the temporary stored string back into Prolog. A typical error message in the first stage, when reconstructing the term structure for quantifiers, is

Parenthesis mismatch while parsing

all x y ((p(x) & q(y) | r) 
[all, **HERE**, x, y, (, (, p, (, x, ), &, q, (, y, ), '|', r, )]
A typical error message printed by Eclipse's parser when parsing the formula 'p(a) & (q(b) | r(c)' with unbalanced parenthesis is
file /tmp/scan-lazy-parse, line 1: syntax error: unexpected full stop
| lazy_parse(p(a)&(q(b)'|' r(c)). 
|                                ^ here
These kind of error messages may be different for other Prolog systems.

So far, there are two different higher-level interfaces,

Both are realized in the same Prolog file.

The Correspondence Theory Interface

See also SCAN: Computing Correspondences.

The purpose of this interface is to translate a Hilbert axiom of some nonclassical logic into second-order predicate logic and then to prepare an input file for SCAN which allows it to eliminate the predicate variables.

Besides the main Prolog program file with the translation functions, there may be arbitrary many library files containing various specifications, in particular the specifications of the nonclassical operators. One general library file is provided in our SCAN package, namely operators.pl.

The user who wants to use the Prolog interface directly, i.e. without WWW, can either start some Prolog system, load the corresponding files and then give some Prolog commands, or he/she can prepare an input file with these commands, start the Prolog with a Unix redirection that causes the Prolog to read this file, execute the commands and then halt. The result would be a SCAN input file, ready to be fed into SCAN.

If the Prolog translation file is scan.pl and the library file is operators.pl then a typical input file would look like

[scan,operators].
scan_input_file('/tmp/scan_corr.in').
set(max_seconds,2).
clear(print_kept).

operator(binary(->,->),800).           
operator(box(b,r)).
operator(diamond(d,r)).

scan([p],'b(p) -> b(b(p))').
This file specifies the task to compute for the modal Hilbert axiom []p -> [][]p the corresponding frame property, which is the transitivity of the accessibility relation. Suppose the name of this file is trans. Suppose further, the name of the SCAN program itself is scan. Then the Unix command
prolog < trans ; scan < /tmp/scan_corr.in > trans.out
causes the following sequence of actions: A Unix shell script for executing this sequence of commands is:
#!/bin/sh
eclipse < $1 ; scan < /tmp/scan.in > $2
In the following section we describe in detail how to define operators and all other parameters that influence the translation into predicate logic. After this we describe in more detail the different input parameters for the Prolog interface.

The Operators Library

The operators library contains all definitions which influence the translation of formulae of some nonclassical logic into predicate logic. The General Definition Mechanism. The translation of formulae of a user-defined logic is determined by various parameters. These parameters are provided by a general definition mechanism. For this purpose there is a predicate
define(type,name,body1,...)
The first argument specifies the type of the parameter. The second argument is a name of the parameter. In general this is a Prolog term f(a1,...an) where the ai are some Prolog atoms used in the body of the definition. These ai can be exchanged by the actual values when the definition is instantiated.

If the body contains logical formulae, in particular those with quantifiers, it is possible to use the more convenient Otter syntax instead of the Prolog term syntax convention. To this end the formula must be enclosed in quotes, for example 'all x p(x)'.

The `define' construct provides schematic definitions. In order to activate these definitions, they have to be instantiated with special Prolog predicates, as for example the `operator' predicate we have seen in the example above.

Truth Conditions. Truth conditions specify when a formula of a nonclassical logic is to be considered as a theorem. A typical specification is

define(truth_condition,
all,
'all w (w |= Phi)'.
It specifies that a formula must be valid in all worlds. A truth condition can be an arbitrary formula with literals Term |= X in them. The X, which may be an arbitrary symbol stands for the formula. As in all define .. predicates, the name of the truth condition may be a Prolog GROUND term, whose constants serve as formal parameters replaced by the actual parameters when it is instantiated.

Operator Definitions. Operator definitions have either the form

define(operator,
Name,
Semantics).
or
define(operator,
Name,
Rewrite_rule).
The prolog atom `operator' as a fixed keyword determines this as an operator definition. Name is a Prolog GROUND term f(a1,...,an) where the ai are atoms which can occur in the third argument.

Examples:

define(operator
box(b,r),
'w |= b(Phi) <-> (all v (r(w,v) -> v |= Phi))',
op(500,fy,[b]).
define(operator,
back('<=',->),
'(P <= Q) -> (Q -> P)'
op(800,yfx,'<=').
The first version defines an operator via its semantics (in this case a standard modal [] operator) and the second version defines it via a rewrite rule.

The Semantics argument must always be an equivalence Left <-> Right whose left hand side is of the form w |= Pattern and whose right hand side is an arbitrary formula containing instances of v |= Formula (here is the recursion). If Prolog syntax conventions are not used, the formula must be quoted.

Conventions: The formula variables must be Prolog variables (with capital letters)

The Rewrite_rule argument is a formula Left -> Right and gives a definition of the operator in terms of a rewrite rule.

Conventions: The formula variables must be Prolog variables.

The precedence declarations in the third argument define the precedence for the operator. It is used for parsing the second argument, the semantics declaration and the rewrite rule respectively. It is also used as default value when the operator is instantiated, but at this point the precedence number can be overwritten.

Rewrite Systems. We provide a general rewrite mechanism for the user-defined logic. It is primarily intended for computing a negation normal form, but it may also be used to do other transformations.

A rewrite system is defined in several stages. The lowest level is the definition rewrite rules. Typical definitions could be

define(rr_rule,implication(-,->,&,'|'),
[ '(P -> Q) -> (-P | Q)',
'-(P -> Q) -> (P & -Q)']). or
define(rr_rule,box(b,d),
'-b(P) -> d(-P)').
The first argument of the `define' predicate must be the atom `rr_rule'. The second argument is the rule name, which can be an atom or a GROUND term. The parameters are formal parameters, which can be instantiated with the actual parameters later on. The last argument consists of a single rewrite rule or a list of rewrite rules. Each rewrite rule must be an implication left -> right, and both sides can be in Otter syntax, but the formula variables must be Prolog variables (i.e. starting with a capital letter). The second level is the definition of a rewrite rule system, for example
define(rr_system,pl0_nnf(-,&,'|',->,<->),
[cancel(-),
neg_in(-,&,'|'),neg_in(-,'|',&),
implication(-,->,&,'|'),
equivalence(-,<->,&,'|')]).
The first argument of `define' is the atom `rr_sytem'. The second argument is the name of the rewrite system with its parameters. The third argument is a list of rewrite rule or other rewrite system names with the formal parameters replaced by the actual parameters.

By using other rewrite system names you can incrementally build rewrite systems on top of other systems.

Predicate Qualifications. Predicate Qualifications restrict the quantifications over predicate symbols

all p phi(p) to all p qualification(p) -> phi(p)
and
exists p phi(p) to exists p qualification(p) & phi(p).
They are defined as for example in
define(qualification,assignment_restriction(p,r),
'all w (p(w) -> all v (r(w,v) -> p(v)))').
The first argument of `define' is the atom `qualifications', the second argument is the name of the qualification, together with the formal parameters, and the third argument is an arbitrary formula, if necessary enclosed in quotes.

Assumptions. The assumption facility provides a means to pass certain formulae to the SCAN algorithm. Typically these are properties of the accessibility relation etc. which might help simplify the SCAN generated formula set. Assumptions are not part of the `scanned' formulae, and they are not negated. Assumptions are defined in the same way as predicate qualifications. An example is

define(assumption,transitivity(r),
'all x y z (r(x,y) & r(y,z) -> r(x,z)').

Commands for the Correspondence Theory Interface

The following Prolog predicates can be used in the input file for the Prolog interface:
truth_condition(name).
instantiates a truth condition. (The truth condition `all' is instantiated by default.)
trc(condition).
abbreviates the sequence define(truth_condition,name,condition). truth_condition(name).
operator(name). and operator(name,precedence_number).
instantiates an operator with default precedence or the given precedence.
ops(operator,semantics).
abbreviates the sequence define(operator,name,semantics). operator(name).
opr(operator,rewrite_rule).
abbreviates the sequence define(operator,name,rewrite_rule). operator(name). (no precedence declarations in both cases.)
qualification(name).
instantiates a qualification.
qual(qualific).
abbreviates the sequence define(qualification,name,qualific). qualification(name).
assumption(name).
instantiates an assumption.
ass(assump).
abbreviates the sequence define(assumption,name,assump). assumption(name).
op(number,assoc,operator).
precedence declaration.
scan_input_file(file).
defines the input file for SCAN.
set(flag).
sets an Otter flag.
clear(flag).
clears an Otter flag.
set(parameter,value).
assigns an Otter parameter to the given value. (All essential flags and parameters are set by default.)
negate_first(negation_sign).
The negate first declaration cause the original formula to be negated before it is translated. This is usually not necessary, but might be useful.
scan(predicates,formula).
translates the formula and generates the SCAN/Otter input file.
scan(predicates,premisses,conclusion).
translates a Hilbert rule premisses -> conclusion and generates the SCAN/Otter input file. In both cases predicates can be a Prolog atom or a list of Prolog atoms. premisses is a list of formulae.

The Circumscription Interface

See also SCAN: Computing Circumscription.

Circumscription operates on predicate logic formulae. Therefore this interface is much simpler than the correspondence theory interface. The handling, however is the same. Either you start Prolog, load the program file, and interactively give the appropriate commands, or you write these commands into a file, and start prolog with redirecting STDIN to this file.

Commands for the Circumscription Interface. The following Prolog predicates can be used in the input file for the Prolog interface:

scan_input_file(file).
defines the input file for SCAN.
set(flag).
sets an Otter flag.
clear(flag).
clears an Otter flag.
set(parameter,value).
circ(Formula,P).
circ(Formula,P,Z).
compute the circumscription formula and generate the SCAN/Otter input file. Formula is a predicate logic formula in Prolog or SCAN/Otter syntax. P and Z are single predicates or lists of predicates (Prolog atoms!). P are the predicates to be minimized and Z are the predicates to be varied.
Important: The final output of SCAN is only one half of the circumscription formula. The correct result is the conjunction of the formula and the output of SCAN.

The WWW Interface

The http Interface

When you fill out a WWW form and push the Submit button, a string of parameter = value pairs is sent to the home http server. This string includes the name of a program to be activated. In our case these are Perl programs which manipulate this string of parameter = value pairs in a certain way, generate input files, either for SCAN directly or for the Prolog interface, start the corresponding programs and forward the output to the http server. The http servers sends the output back to the WWW viewer.

The html Files

Here is an overview of all html files which make up this documentation We provide three different forms:

References


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: 05 Aug 13