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:
pred_list[predicates].
set(unskolemize).
set(negate).
;.
set(binary_c_res).
set(c_factor).
set(print_lists_at_end).
set(process_input).
set(unit_deletion).
clear(print_kept).
assign(max_seconds,n).
set(prolog_style_variables).
set(display_terms).
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' 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.
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.
scan < input_file >! output file
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)).
all(x,all(y,all(z,p(x,y) & p(y,z) -> q(x,z)))).
all x y z (p(x,y) & p(y,z) -> q(x,z))
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, )]
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
So far, there are two different higher-level interfaces,
Both are realized in the same Prolog file.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))').
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
prolog is started (if such a system is installed).
trans and executes the commands:
[scan,operators].
scan_input_file('/tmp/scan_corr.in').
set(max_seconds,2).
assign(max_seconds,2).
(some Prolog systems have a built in predicate assign!)
clear(print_kept).
operator(binary(->,->),800).
operator(box(b,r)).
operator(diamond(d,r)).
scan([p],'b(p) -> b(b(p))').
/tmp/scan_corr.in, which looks like
pred_list[p]. set(unskolemize). set(negate). ;. set(print_lists_at_end). set(binary_c_res). set(c_factor). set(unit_deletion). set(process_input). clear(print_kept). assign(max_seconds, 2). formula_list(usable). end_of_list. formula_list(sos). (- (all world ((all wv1 (r(world, wv1) -> p(wv1) ) ) -> (all wv2 (r(world, wv2) -> (all wv3 (r(wv2, wv3) -> p(wv3) ) ) ) ) ) ) ). end_of_list.
scan is started, reads this file and writes a protocol
to the file trans.out
The last two lines of this file would be
(all x0 all x1 all x2 (-r(x0,x1) | -r(x1,x2) | r(x0,x2))) % Clause set unskolemized.
r.
#!/bin/sh eclipse < $1 ; scan < /tmp/scan.in > $2
define(type,name,body1,...)
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
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
or
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:
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
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(-,<->,&,'|')]).
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
- 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
truth_condition(name).
all' is instantiated by default.)
trc(condition).
define(truth_condition,name,condition).
truth_condition(name).
operator(name). and operator(name,precedence_number).
ops(operator,semantics).
define(operator,name,semantics). operator(name).
opr(operator,rewrite_rule).
define(operator,name,rewrite_rule). operator(name).
(no precedence declarations in both cases.)
qualification(name).
qual(qualific).
define(qualification,name,qualific). qualification(name).
assumption(name).
ass(assump).
define(assumption,name,assump). assumption(name).
op(number,assoc,operator).
scan_input_file(file).
set(flag).
clear(flag).
set(parameter,value).
negate_first(negation_sign).
scan(predicates,formula).
scan(predicates,premisses,conclusion).
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).
set(flag).
clear(flag).
set(parameter,value).
circ(Formula,P).
circ(Formula,P,Z).
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.