ANL/MCS-TM-263
OTTER 3.3 Reference Manual
by
William McCune
Mathematics and Computer Science Division
Technical Memorandum No. 263
August 2003
This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Advanced Scientific Computing Research, Office of Science, U.S. Department of Energy, under Contract W-31-109-ENG-38.
Argonne National Laboratory, with facilities in the states of Illinois and Idaho, is owned by the United States Government and operated by The University of Chicago under the provisions of a contract with the Department of Energy.
This report was prepared as an account of work sponsored by an agency of the United States Government. Neither the United States Government nor any agency thereof, nor The University of Chicago, nor any of their employees or officers, makes any warranty, express or implied, or assumes any legal liability or responsibility for the accuracy, completeness, or usefulness of any information, apparatus, product, or process disclosed, or represents that its use would not infringe privately-owned rights. Reference herein to any specific commercial product, process, or service by trade name, trademark, manufacturer, or otherwise, does not necessarily constitute or imply its endorsement, recommendation, or favoring by the United States Government or any agency thereof. The views and opinions of document authors expressed herein do not necessarily state or reflect those of the United States Government or any agency thereof, Argonne National Laboratory, or The University of Chicago.
Otter 3.3 Reference ManualWilliam McCune |
Abstract: Otter 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 features are conversion from first-order formulas to clauses, forward and back subsumption, factoring, weighting, answer literals, term ordering, forward and back demodulation, evaluable functions and predicates, Knuth-Bendix completion, and the hints strategy. Otter is coded in ANSI C, is free, and is portable to many different kinds of computer.
Otter (Organized Techniques for Theorem-proving and Effective Research) is a resolution-style theorem prover, similar in scope and purpose to the aura [24] and lma/itp [15] theorem provers, which are also associated with Argonne. Otter applies to statements written in first-order logic with equality. The primary design considerations have been performance, portability, and extensibility. The programming language ANSI C is used.
Otter features the inference rules binary resolution, hyperresolution, UR-resolution, and binary paramodulation. These inference rules take a small set of clauses and infer a clause; if the inferred clause is new, interesting, and useful, it is stored and may become available for subsequent inferences. Other features of Otter are the following.
Although Otter has an autonomous mode, most work with Otter involves interaction with the user. After encoding a problem into first-order logic or into clauses, the user usually chooses inference rules, sets options to control the processing of inferred clauses, and decides which input formulas or clauses are to be in the initial set of support and which (if any) equalities are to be demodulators. If Otter fails to find a proof, the user may wish to try again with different initial conditions. In the autonomous mode, the user inputs a set of clauses and/or formulas, and Otter does a simple syntactic analysis and decides inference rules and strategies. The autonomous mode is frequently useful for the first attempt at a proof.
Some of the first applications that come to mind when one hears “automated theorem proving” are number theory, calculus, and plane geometry, because these are some of the first areas in which math students try to prove theorems. Unfortunately, Otter cannot do much in these areas: interesting number theory problems usually require induction, interesting calculus and analysis problems usually require higher-order functions, and the first-order axiomatizations of geometry are not practical. (Nonetheless, Art Quaife has proved many interesting theorems in number theory and geometry using Otter [22, 21].) For practical theorem proving in inductive theories, see the work of Boyer, Moore, and Kaufmann [2, 10].
Otter is also not targeted toward synthesizing or verifying formal hardware or software systems. See [6, 5] for work in those areas.
Summaries of other theorem-proving systems can be found in proceedings of the recent Conferences on Automated Deduction (CADE) and in coverage of the CADE ATP System Competition (CASC).
There have been several previous releases of Otter, starting with version 0.9, which was distributed at the 9th International Conference on Automated Deduction (CADE-9) in May 1988. Many new features have been added since then, many bugs have been fixed, and (of course) many bugs have been introduced.
This manual does not contain an introduction to first-order logic or to automated deduction. We assume that the reader knows the basic terminology including term (variable, constant, complex term), atom, literal, clause, propositional variable, function symbol, predicate symbol, Skolem constant, Skolem function, formula, conjunctive normal form (CNF), resolution, hyperresolution, and paramodulation. See [3, 14, 32] for an introductions and overviews of automated theorem proving, see [23, 1] for collections of important papers, see [30] for a list of general problems in the field, and see [33, 8, 18] for introductions and applications that focus on the use of Otter.
Once Otter gets going with its real work—making inferences and searching for proofs—it operates on clauses and on clauses only. If the user inputs nonclausal first-order formulas, Otter immediately translates them to clauses, by a straightforward procedure involving negation normal form conversion, Skolemization, quantifier operations, and conjunctive normal form conversion.
As with its predecessors aura and lma/itp, Otter’s basic inference mechanism is the given-clause algorithm, which can be viewed as a simple implementation of the set of support strategy [31]. Otter maintains four lists of clauses:
sos (set of support) are not available to make
inferences; they are waiting to participate in the search.
The main loop for inferring and processing clauses and
searching for a refutation operates mainly on the lists usable
and sos:
While (sos is not empty and no refutation has been found)
1. Let given_clause be the ``best'' clause in sos;
2. Move given_clause from sos to usable;
3. Infer and process new clauses using the inference
rules in effect; each new clause must have the
given_clause as one of its parents and members
of usable as its other parents; new clauses
that pass the retention tests are appended to sos;
End of while loop.
The set of support strategy requires the user to partition the
input clauses into two sets: those with support and those without.
For each inference, at least one of the parents must have support.
Retained inferences receive support. In other words, no inferences
are made in which all parents are nonsupported input clauses. At
input time, Otter’s list sos is the set of supported clauses,
and usable is the nonsupported clauses. (Once the main loop
has started, usable no longer corresponds to nonsupported
clauses, because sos clauses have moved there.) Otter’s
main loop implements the set of support strategy, because no
inferences are made in which all of the parents are from the initial
usable list.
The following paragraph tries to answer the frequently asked question “At a certain point, Otter has all of the clauses available to make the inference I want, and one of the potential parents is selected as the given clause—why doesn’t the program make the inference?”
Otter’s main loop eliminates an important kind of redundancy.
Suppose one can infer clause C from clauses A and B, and suppose
both A and B are in list sos. If A is selected as the
given clause, it will be moved to usable and inferences
will be made; but A will not mate with B to infer C,
because B is still in sos. We must wait until B has also
been selected as given clause. Otherwise, we would infer C
twice. (The redundancy would be much worse with inference rules such as
hyperresolution and UR-resolution with which a clause can have
many parents.) In general,
all parents that participate in an inference must either have been in
the initial usable list or have been selected as given clauses.
(This is not true when demodulators are considered as parents.)
The procedure for processing a newly inferred clause new_cl follows;
steps marked with * are optional.
1. Renumber variables.
* 2. Output new_cl.
3. Demodulate new_cl (including $ evaluation).
* 4. Orient equalities.
* 5. Apply unit deletion.
6. Merge identical literals (leftmost copy is kept).
* 7. Apply factor-simplification.
* 8. Discard new_cl and exit if too many literals or variables.
9. Discard new_cl and exit if new_cl is a tautology.
* 10. Discard new_cl and exit if new_cl is too `heavy'.
* 11. Sort literals.
* 12. Discard new_cl and exit if new_cl is subsumed by any clause
in usable, sos, or passive (forward subsumption).
13. Integrate new_cl and append it to sos.
* 14. Output kept clause.
15. If new_cl has 0 literals, a refutation has been found.
16. If new_cl has 1 literal, then search usable, sos, and
passive for unit conflict (refutation) with new_cl.
* 17. Print the proof if a refutation has been found.
* 18. Try to make new_cl into a demodulator.
-------------
* 19. Back demodulate if Step 18 made new_cl into a demodulator.
* 20. Discard each clause in usable or sos that is subsumed by
new_cl (back subsumption).
* 21. Factor new_cl and process factors.
Steps 19–21 are delayed until steps 1–18 have been applied to all clauses inferred from the active given clause.
Although Otter has a primitive interactive feature (Sec. 15), it is essentially a noninteractive program. On unix-like systems it reads from the standard input and writes to the standard output:
otter < input-file > output-file
No command-line options are accepted; all options are given in the input file.
Otter recognizes two basic types of statement: clauses and formulas. Clauses are simple disjunctions whose variables are implicitly universally quantified. Otter’s searches for proofs operate on clauses. Formulas are first-order statements without free variables—all variables are explicitly quantified. When formulas are input, Otter immediately translates them to clauses.
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.
Three kinds of character string, collectively referred to as names, can be used for variables, constants, function symbols, and predicate symbols:
$, and _.
*+-/\^<>=`~:?@&!;# (and sometimes |).
" 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. 4.6.) For completeness, we list here 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.
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
variable if it starts with u, v, w, x,
y, or z. If the flag prolog_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.) In a formula, a simple term is a variable if
and only if it is bound by a quantifier.
Names that start with $
are reserved for special purposes,
including evaluable functions and predicates (Sec. 9),
answer literals and terms (Sec. 11), and some internal
system names. The name = and any name that starts with
eq, EQ, or Eq, when used as a binary predicate
symbol, is recognized as an equality predicate by the demodulation
and paramodulation processes. And some names, when they occur
in clauses or formulas, are recognized as logic 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
disjunction and as Prolog-style list punctuation, and although the
symbol - is built in as logical negation, it can be
used for both unary and binary minus as well.
Recall that, when interpreted, terms are evaluated as objects in some domain, and atoms are evaluated as truth values. Constants and variables 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 variable) 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 application 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.
Some binary symbols can be written in
infix form; the most important is =. In addition, a negated
equality, -(a=b) can be abbreviated a!=b.
Prolog-style list notation can be used to write terms that usually represent lists. Table 1 gives some example terms in list notation and the corresponding pure prefix form.
Of course, lists can contain complex terms, including other lists.
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 disjunction are - and |,
respectively.
Although clauses can be written in pure prefix form, with - as a
unary symbol and | as a binary symbol, 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. 4.6).
Table 2 lists the built-in logic symbols for constructing formulas.
Although the practice is rarely done, formulas can be written in pure
prefix form. Quantification is the only tricky part: there is a
special variable-arity symbol, $Quantified, for quantified
formulas. For example, ∀ x y ∃ z (P(x,y,z) | Q(x,z)) is
represented by
$Quantified(all,x,y,exists,z,|(P(x,y,z),Q(x,z))).
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. 4.6. Here are some examples.
| Standard Usage | Otter syntax (abbreviated) | |
| ∀ x P(x) | all x P(x) | |
| ∀ x y ∃ z (P(x,y,z) ∨ Q(x,z)) | all x y exists z (P(x,y,z) | Q(x,z)) | |
| ∀ 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, the following three strings represent the same formula.
p | -q & r -> -s | t.
(p | (-(q) & r)) -> (-(s) | t).
->(|(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. 4.6
for the rules.
Many Prolog systems 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 ordinary Prolog mechanism and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.
Table 3: Predeclared Symbols
op(800, xfy, # ).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 symbol with higher
precedence is more dominant (closer to the root of the term), and
one with lower precedence binds more tightly. For example, the
symbols
->,
|,
&, 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
symbol, and x and y, which represent the expressions to
which the symbol applies, specify how terms are associated.
Given an expression involving symbols of the same precedence,
the types of the symbol determines, in part, the association. See
Table 4.
The following are examples of associativity:
+ has type xfy, then a+b+c+d is understood as
a+(b+(c+d)).
-> has type xfx, then a->b->c is not well formed.
- has type fy, then - - -p is understood as
-(-(-(p))). (The spaces are necessary; otherwise, --- will
be parsed as single name.)
- has type fx, then - - -p is not well formed.
Caution: The associativity specifications in the
infix symbol declarations say nothing about the logical associativity
of the operation, for example, whether (a+b)+c is the same object as
as a+(b+c). The specifications 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.
(This paragraph can be skipped by most users.)
The precedence of symbols 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 symbol. For example, a&b has
the precedence of &, and a&bordinary Prolog mechanism
and Otter’s.
a,b,c cannot be a term, as in a,b,c -> d,e,f.
all and exists as
special cases, because they don’t seem to fit neatly into the
standard Prolog mechanism.
Symbols to be treated in this special way are given a type and a precedence. Either Otter predeclares the symbol’s properties, or the user gives Otter a command of one of the following forms.
op(precedence, type, symbol).
op(precedence, type, list-of-symbols).
The precedence is an integer i, 0<i<1000, and type
is one of the following: xfx, xfy, yfx (infix),
fx, fy (prefix), xf, yf (postfix).
See Table 3 for the commands corresponding to the
predeclared symbols.