- From: Sandro Hawke <sandro@w3.org>
- Date: Fri, 6 Sep 2002 12:40:51 -0400
- To: www-archive@w3.org
EXCERPT FROM: http://www-unix.mcs.anl.gov/AR/otter/
Otter 3.0 Reference Manual and Guide
William W. McCune
Otter (Organized Techniques for Theorem-proving and Effective
Research) is a resolution-style theorem-proving program for
first-order logic with equality. Otter includes the inference
rules binary resolution, hyperresolution, UR-resolution, and
binary paramodulation. Some of its other abilities and fea-
tures are conversion from first-order formulas to clauses,
forward and back subsumption, factoring, weighting, answer
literals, term ordering, forward and back demodulation, evalu-
able functions and predicates, and Knuth-Bendix completion.
Otter is coded in C, is free, and is portable to many differ-
ent kinds of computer.
January 1994
(Revision A, August 1995)
This work was supported by the Office of Scientific Computing, U.S.
Department of Energy, under Contract W-31-109-Eng-38.
CHAPTER 4, "SYNTAX"
4. Syntax
Otter recognizes two basic types of statement: clauses and formulas.
Clauses are simple disjunctions whose variables are implicitly univer-
sally quantified. Otter's searches for proofs operate on clauses.
Formulas are first-order statements without free variables---all vari-
ables are explicitly quantified. When formulas are input, Otter imme-
diately translates them to clauses.
Function symbols and predicate symbols are sometimes referred to as
functors when the distinction is not important.
4.1. Comments
Comments can be placed in the input file by using the symbol %. All
characters from the first % on a line to the end of the line are
ignored. Comments can occur within terms. Comments are not echoed to
the output file.
4.2. Names for Variables, Constants, Functions, and Predicates
Three kinds of character string, collectively referred to as names,
can be used for variables, constants, function symbols, and predicate
symbols:
+ An ordinary name is a string of alphanumerics, $, and _.
+ A special name is a string of characters in the set
*+-/<>=`~:?@&!;# (and sometimes |).
+ A quoted name is any string enclosed in two quotation marks of
the same type, either " or '. We have no trick for including a
quotation mark of the same type in a quoted name.
(The reason for separating ordinary and special names has to do with
infix, prefix, and postfix operators; see Sec. [ops].) Although out
of place here, for completeness we list the meanings of the remaining
printable characters.
. (period) --- terminates input expressions.
% --- starts a comment (which ends with the end of the line).
,()[] (and sometimes |) --- are punctuation and grouping symbols.
Variables.
Determining whether a simple term is a constant or a variable depends
on the context of the term. If it occurs in a clause, the symbol
determines the type: the default rule is that a simple term is a vari-
able if it starts with u, v, w, x, y, or z. If the flag pro-
log_style_variables is set, a simple term is a variable if and only if
it starts with an upper-case letter or with _. (Therefore, variables
in clauses must be ordinary names.) A simple term in a formula is a
variable if and only if it is bound by a quantifier.
Reserved and Built-in Names.
Names that start with $ are reserved for special purposes, including
evaluable functions and predicates (Sec. [eval]), answer literals and
terms (Sec. [answer]), and some internal system names. The name = and
any name that starts with eq, EQ, or Eq, when used as a binary predi-
cate symbol, is recognized as an equality predicate by the demodula-
tion and paramodulation processes. And some names, when they occur in
clauses or formulas, are recognized as logic symbols.
Overloaded Symbols.
The user can use a name for more than one purpose, for example as a
constant and as a 5-ary predicate symbol. When the flag check_arity
is set (the default), the user is warned about such uses. Some built-
in names are also overloaded; for example, | is used both for disjunc-
tion and as Prolog-style list punctuation, and although - is built in
as logical negation, it is generally used for both unary and binary
minus as well.
4.3. Terms and Atoms
Recall that, when interpreted, terms are evaluated as objects in some
domain, and atoms are evaluated as truth values. Constants and vari-
ables are terms. An n-ary function symbol applied to n terms is also
a term. An n-ary predicate symbol applied to n terms is an atom. A
nullary predicate symbol (also referred to as a propositional vari-
able) is also an atom.
The pure way of writing complex terms and atoms is with standard
application: the function or predicate symbol, opening parenthesis,
arguments separated by commas, then closing parenthesis, for example,
f(a,b,c) and =(f(x,e),x). If all subterms of a term are written with
standard application, the term is in pure prefix form. Whitespace
(spaces, tabs, newlines, and comments) can appear in standard applica-
tion terms anywhere except between a function or predicate symbol and
its opening parenthesis. If the flag display_terms is set, Otter will
output terms in pure prefix form.
Infix Equality. infix form; the most important is =. In addition, a
negated equality, -(a=b) can be abbreviated a!=b.
List Notation. to write terms that represent lists. Table 1 gives
some example terms in list notation and the corresponding pure prefix
form.
Table 1: List Notation
[] $nil
[x|y] $cons(x,y)
[x,y] $cons(x,cons(y,nil))
[a,b,c,d] $cons(a,cons(b,cons(c,cons(d,nil))))
[a,b,c|x] $cons(a,cons(b,cons(c,x)))
Of course, lists can contain complex terms, including other lists.
4.4. Literals and Clauses
A literal is either an atom or the negation of an atom. A clause is a
disjunction of literals. The built-in symbols for negation and dis-
junction are - and |, respectively. Although clauses can be written
in pure prefix form, with - as a unary symbol and | as a binary sym-
bol, they are rarely written that way. Instead, they are almost
always written in infix form, without parentheses. For example, the
following is a clause in both forms.
Pure prefix: |(-(a),|(=(b1,b2),-(=(c1,c2))))
Infix (abbreviated): -a | b1=b2 | c1!=c2
Otter accepts both forms. (Clauses are parsed by the general term-
parsing mechanism presented in Sec. [ops]).
4.5. Formulas
Table 2. lists the built-in logic symbols for constructing formulas.
Table 2: Logic Symbols
negation -
disjunction |
conjunction &
implication ->
equivalence <->
existential quantification exists
universal quantification all
Formulas in Pure Prefix Form.
Although the practice is rarely done, formulas can be written in pure
prefix form. Quantification is the only tricky part: there is a spe-
cial variable-arity functor, $Quantified, for quantified formulas.
For example, all x y exists z (P(x,y,z) | Q(x,z)) is represented by
$Quantified(all,x,y,exists,z,|(P(x,y,z),Q(x,z))).
If the flag display_terms is set, the formulas (and everything else)
will be displayed in pure prefix form.
Abbreviated Formulas.
Formulas are usually abbreviated in a natural way. The associativity
and precedence rules for abbreviating formulas and the mechanism for
parsing formulas are presented in Sec. [ops]. Here are some examples.
standard usage Otter syntax (abbreviated)
all x P(x) all x P(x)
all x y exists z (P(x,y,z) v Q(x,z))
all x y exists z (P(x,y,z) | Q(x,z))
all x (P(x) & Q(x) & R(x) -> S(x))
all x (P(x) & Q(x) & R(x) -> S(x))
Note that if a formula has a string of identical quantifiers, all but
the first can be dropped. For example, all x all y all z p(x,y,z) can
be shortened to all x y z p(x,y,z). In expressions involving the
associative operations & and |, extra parentheses can be dropped.
Moreover, a default precedence on the logic symbols allows us to drop
more parentheses: <-> has the same precedence as ->, and the rest in
decreasing order are ->, |, &, -. Greater precedence means closer to
the root of the term (i.e., larger scope). For example, p | -q & r ->
-s | t represents (p | (-(q) & r)) -> (-(s) | t), or in pure prefix
form, ->(|(p,&(-(q),r)),|(-(s),t)).
When in doubt about how a particular string will be parsed, one can
simply add additional parentheses and/or test the string by having
Otter read it and then display it in pure prefix form. The following
input file can be used to test the preceding example.
assign(stats_level, 0).
set(display_terms).
formula_list(usable).
p| -q&r-> -s|t. % This formula has minimum whitespace.
end_of_list.
In general, whitespace is required around all and exists and to the
left of -; otherwise, whitespace around the logic symbols can be
removed. See Sec. [ops] for the rules.
4.6. Infix, Prefix, and Postfix Expressions
Many Prolog systems (for example Quintus and Sicstus) have a feature
that allows users to declare that particular function or predicate
symbols are infix, prefix, or postfix and to specify a precedence and
associativity so that parentheses can sometimes be dropped. Otter has
a similar feature. In fact, the clause and formula parsing routines
use the feature. Users who use only the predeclared logic operators
for clauses and formulas and the predeclared infix equality = can skip
the rest of this section.
Prolog users who are familiar with the declaration mechanism should
note the following differences between the Quintus/Sicstus mechanism
and Otter's.
+ The predeclared operators are different. See Table 3.
+ Otter does not treat comma as an operator; in particular, a,b,c
cannot be a term, as in a,b,c -> d,e,f.
+ Otter treats the quantifiers all and exists as special cases,
because they don't seem to fit neatly into the standard Prolog
mechanism.
+ Otter requires whitespace in some cases where the Prologs do not.
Functors to be treated in this special way are given a type and a
precedence. Either Otter predeclares the functor's properties, or the
user gives Otter a command of one of the forms
op( precedence , type , functor ).
op( precedence , type , list-of-functors ).
The precedence is an integer i, 0<i<1000, and type is one of the fol-
lowing: xfx, xfy, yfx (infix), fx, fy (prefix), xf, yf (postfix). See
Table 3 for the commands corresponding to the predeclared functors.
Table 3: Predeclared Functors
op(800, xfx, ->). op(700, xfx, @<).
op(800, xfx, <->). op(700, xfx, @>).
op(790, xfy, |). op(700, xfx, @<=).
op(780, xfy, ). op(700, xfx, @>=).
op(700, xfx, =). op(500, xfy, +).
op(700, xfx, !=). op(500, xfx, -).
op(700, xfx, <). op(500, fx, +).
op(700, xfx, >). op(500, fx, -).
op(700, xfx, <=).
op(700, xfx, >=). op(400, xfy, *).
op(700, xfx, ==). op(400, xfx, /).
op(700, xfx, =/=). op(300, xfx, mod).
Given an expression that looks like it might be associated in a number
of ways, the relative precedence of the operators determines, in part,
how it is associated. A functor with higher precedence is more domi-
nant (closer to the root of the term), and one with lower precedence
binds more tightly. For example, the functors ->, |, &, and - have
decreasing precedence; therefore the expression p & - q | r -> s is
understood as ((p & (-q)) | r) -> s.
In each of the types, f represents the functor, and x and y, which
represent the expressions to which the functor applies, specify how
terms are associated. Given an expression involving functors of the
same precedence, the types of the functors determines, in part, the
association. See Table 4.
Table 4: Functor Types
xfx infix (binary) don't associate
xfy infix (binary) associate right
yfx infix (binary) associate left
fx prefix (unary) don't associate
fy prefix (unary) associate
xf postfix (unary) don't associate
yx postfix (unary) associate
The following are examples of associativity:
+ If + has type xfy, then a+b+c+d is understood as a+(b+(c+d)).
+ If -> has type xfx, then a->b->c is not well formed.
+ If - has type fy, then - - -p is understood as -(-(-(p))). (The
spaces are necessary; otherwise, --- will be parsed as single
name.)
+ If - has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the infix functor decla-
rations say nothing about the logical associativity of the operation,
e.g., whether (a+b)+c is the same object as as a+(b+c). The specifi-
cations are only about parsing ambiguous expressions. In most cases,
when an operator is xfy or yfx, it is also logically associative, but
the logical associativity is handled separately; it is built-in in the
case of the logic symbols | and & in Otter clauses and formulas, and
it must be axiomatized in other cases.
Details of the Functor Declarations. (This paragraph can be skipped
by most users.) The precedence of functors extends to the precedence
of expressions in the following way. The precedence of an atomic,
parenthesized, or standard application expression is 0. Respective
examples are p, (x+y), and p(a+b,c,d). The precedence of a (well-
formed) nonparenthesized nonatomic expression is the same as the
precedence of the root functor. For example, a&b has the precedence
of &, and a&b|c has the precedence of the greater functor. In the
type specifications, x represents an expression of lower precedence
than the functor, and y represents an expression with precedence less
than or equal to the functor. Consider a+b+c, where + has type xfy;
if association is to the left, then the second occurrence of + does
not fit the type, because a+b, which corresponds to x, does not have a
lower precedence than +; if association is to the right, then all is
well. If we extend the example, under the declarations op(700, xfx,
=) and op(500, xfy, +), the expression a+b+c=d+e must be understood as
(a+ (b+c))= (d+e).
4.7. Whitespace in Expressions
The reason for separating ordinary names from special names (Sec.
[names]) is so that some whitespace (spaces, tabs, newline, and com-
ments) can be removed. We can write a+b+c (instead of having to write
a + b + c), because "a+b+c" cannot be a name, that is, it must be
parsed into five names.
Caution. There is a deficiency in Otter's parser having to do with
whitespace between a name and opening parenthesis. The rule to use
is: Insert some white space if and only if it is not a standard
application. For example, the two pieces of white space in (a+
(b+c))= (d+e) are required, and no white space is allowed after f or g
in f(x,g(x)).
4.8. Bugs, etc., in Input and Output of Expressions
+ The symbol | is either Prolog-style list punctuation or part of a
special name. With the built-in declaration of | as infix, the
term [a|b] is ambiguous, with possible interpretations
t_1=$cons(a,b) and t_2=$cons(|(a,b),$nil). Otter recognizes
[a|b] as t_1. The term t_2 can be written [(a|b)]. The bug is
that t_2 will be output without the parentheses. This is the
only case I know in which Otter cannot correctly read a term it
has written.
+ A term consisting of a unary + or - applied to a nonnegative
integer is always translated to a constant.
+ Parsing large terms without parentheses, say a1+a2+a3+...+a1000,
can be very slow if the operator is left associative (yfx). If
you intend to parse such terms, make the operator right associa-
tive (xyf).
+ Quoted strings cannot contain a quotation mark of the same type.
+ The flag check_arity sometimes issues warnings when it should
not.
+ Braces () can be used to group input expressions, but Otter
always uses ordinary parentheses on output.
4.9. Examples of Operator Declarations
Group Theory. Suppose we like to see group theory expressions in the
form (ab^-1c^-1-1)^-1, in which right association is assumed.
We can approximate this for Otter with (a*b^ *c^ ^)^.
(We have to make the group operator explicit; -1 is not a legal
Otter name; the whitespace shown is required.) The declarations
op(400, xfy, *) and op(350, yf, ^) suffice. Other examples of expres-
sions (with minimum whitespace) using these declarations are
(x*y)*z=x*y*z and (y*x)^ =x^ *y^.
Otter Options. Options are normally input as in the following examples.
set(prolog_style_variables).
clear(print_kept).
assign(max_given, 300).
If, however, we make the declarations (the precedences are irrelevant)
op(100, fx, set).
op(100, fx, clear).
op(100, xfx, assign).
then we may write
set prolog_style_variables.
clear print_kept.
max_given assign 300.
================================================================
---- With Permission ----
To: Sandro Hawke <sandro@w3.org>
Subject: Re: Is the otter manual on the web? Can I put it there?
Date: Thu, 05 Sep 2002 11:03:40 -0500
From: William McCune <mccune@mcs.anl.gov>
Message-Id: <200209051603.g85G3fn11253@theorem.mcs.anl.gov>
You're most welcome to put any parts of the Otter manual on the web.
Bill
---- Why? ----
Because I want to refer people to this syntax in web documents.
- sandro
Received on Friday, 6 September 2002 12:43:14 UTC