EQP 0.9 USERS' GUIDE
William McCune
Mathematics and Computer Science Division
Argonne National Laboratory
October 1997 (updated April 1999)
1. INTRODUCTION
This document is a quick and dirty (and incomplete) guide to the use
of EQP, a theorem prover for equational logic. EQP's important
properties are:
+ It has associative-commutative (AC) unification and matching.
+ It has "basic paramodulation" and several other strategies.
+ It seems to work well on many theorems about lattice-like structures.
+ It proved the Robbins conjecture [5].
In many ways EQP is similar to Otter, including input format,
functionality, and use. I hope that Otter users will find EQP easy to
learn.
EQP is not really meant for wide and general use, but it may be just
the thing you need to solve your lattice problem. I expect that
within a few years, Otter and EQP will be replaced (and subsumed) by a
new program. See the EQP experiments paper [2] for an overview of
EQP, including descriptions of the various strategies available in
EQP. See the Otter manual [1] for for general information and details
on EQP clause syntax. See the EQP web page [3] for further
information on EQP.
2. COMPILING AND RUNNING EQP
To compile EQP on a UNIX system, run "make eqp". For me, EQP (version
0.9c) compiles out-of-the-box on Linux 2.0.27 (gcc 2.7.2.1), FreeBSD
2.1.0 (gcc 2.6.3), AIX 4.2 (gcc 2.7.2.1), SunOS 4.1.4 (gcc 2.7.2),
SunOS 5.5.1 (gcc 2.7.2.1). I don't know if EQP has been compiled on
Microsoft or Macintosh operating systems. To run EQP, put all
of the input into a file, say problem.in, and run
eqp09c < problem.in > problem.out
3. EQP INPUT
Comments start with the first "%" on a line and continue to the
end of the line.
3.1. Clauses
EQP input clauses (which must be positive or negative equations with
infix symbol "=" or "!=") have the same syntax as Otter 3.0.4 clauses,
and I will not give the details here. See the Otter manual [1],
available from the Otter Web page [4]. Or, see the example input
files that accompany the source code. Here are a few things to note
about clause syntax.
+ One can declare function symbols to be infix, with assumed
associativity and precedence (in a similar way to to many Prolog
systems).
+ Be careful about white space between a function symbol and an
opening parenthesis. The rule is: if there is no white space, it is a
function applied to arguments, e.g, "f(x,y)"; if there is whitespace,
the opening parenthesis is the start of a new term, e.g., "x* (y*z)".
The expression "x*(y*z)" is not a well formed term. In other places,
white space is usually optional. I recommend including space around
infix function symbols, e.g., "x * (y * z)".
3.2. The Rest of the Input File
EQP's input is divided into two sections: commands, then lists of
clauses. The commands section is terminated with "end_of_commands."
3.2.1. Commands
set(). % Set a flag
clear(). % Clear a flag
assign(, ). % Assign a value to a parameter
assoc_comm(). % Declare a symbol to be AC
commutative(). % Declare a symbol to be commutative
The preceding two commands apply to binary function symbols.
lex(). % Order symbols
lrpo_multiset_status(). % Give symbols multiset status
The preceding two commands are used with the LRPO term ordering
(which is activated with "set(lrpo)"). DO NOT USE LRPO WITH
AC OR COMMUTATIVE SYMBOLS. Symbols in the list must have the
correct number of arguments.
op(, , ).
The op() command is used to declare the symbol syntactic associativity
and precedence of a symbol. This is for parsing and printing only.
It is independent of the the assoc_comm() command.
interpretation(, ).
The preceding command is for use with semantic paramodulation.
See interp.c.
3.2.2. Lists of Clauses
Four list names are recognized: usable, sos, demodulators and passive.
The use of the lists is the same as in Otter. A list of clauses looks
like this:
list().
end_of_list.
3.3. An Example Input File
The following input file does not make much sense, but it
is syntactically correct and uses all of the commands.
%%%%%%%%%%%%% Start of input file
set(para_pairs).
clear(print_given).
assign(pick_given_ratio, 4).
op(400, xfy, *).
op(500, xfx, #).
assoc_comm(*).
commutative(#).
lex([a, b, c, d, e, g, h, f(_,_), _*_, _#_]).
lrpo_multiset_status([f(_,_)]).
end_of_commands.
list(usable).
a * b * c = d.
e # (e # g) = h.
end_of_list.
list(sos).
c = d.
end_of_list.
list(demodulators).
r = s.
end_of_list.
list(passive).
x # y != y # x.
end_of_list.
%%%%%%%%%%%%% End of input file
4. FLAGS AND PARAMETERS
4.1. Flags
display_terms - default clear. If set, all output terms are printed
in prefix form with full parenthesization (did I just create that word?!).
check_arity - default set. If set, symbol overloading with multiple
arities is not allowed.
prolog_style_variables - default clear. If set, variables start with
upper case. If clear, variables start with a member of [uvwxyz].
print_gen - default clear. If set, all generated clauses are printed
to the output file.
demod_history - default set. If set, demodulation steps are included
in the justification of a clause.
print_given - default set. If set, given clauses printed to the
output file.
print_pairs - default clear. If set, given pairs are printed to the
output file.
lrpo - default clear. If set, LRPO (lexicographic recursive path ordering
is used to orient equations. DO NOT USE THIS IF YOUR INPUT CONTAINS
AC of commutative symbols.
para_pairs - default clear. If set, use the pair algorithm; that is,
at each iteration of the main loop, select a PAIR of equations for
application of paramodulation.
If clear, use the given clause algorithm (as in Otter).
print_forward_subsumed - default clear. If set, print a message
when forward subsumption occurs.
print_back_demod - default set. If set, print a message when
back demodulation occurs.
print_lists_at_end - default clear. If set, print all lists
at the end of the search.
no_demodulation - default clear. If set, do not add clauses to
list(demodulators). However, if the user inputs clauses on
list(demodulators), those clauses will always be used for demodulation.
index_bt_demod - default set. This flag is relevant only if
assoc_comm or commutative symbols have been declared; that is,
only if backtrack unification/matching is in use. If set, demodulators
are indexed. (If there are no assoc_comm or commutative symbols,
demodulators are always indexed.
index_ac_args - default set. This flag is relevant only
if assoc_comm symbols have been declared. If set, a small amount
of indexing is done on arguments of AC symbols. The indexing is
done on number of arguments and number of nonvariable arguments.
If clear, AC symbols are indexed as constants; that is, subterms
are ignored.
index_paramod - default set. IF ANY SYMBOLS ARE DECLARED assoc_comm
OR commutative, THIS FLAG WILL BE AUTOMATICALLY CLEARED, because
FPA/Path indexing does not handle those properties.
If set, use FPA/Path indexing for
paramodulation. If clear, do not index for paramodulation.
index_bd - default set. IF ANY SYMBOLS ARE DECLARED assoc_comm OR
commutative, THIS FLAG WILL BE AUTOMATICALLY CLEARED, because FPA/Path
indexing does not handle those properties. If set, use FPA/Path
indexing for back demodulation. If clear, do not index for back
demodulation.
index_bs - default set. IF ANY SYMBOLS ARE DECLARED assoc_comm OR
commutative, THIS FLAG WILL BE AUTOMATICALLY CLEARED, because FPA/Path
indexing does not handle those properties. If set, use FPA/Path
indexing for back subsumption. If clear, do not index for back
subsumption.
index_fs - default set. IF ANY SYMBOLS ARE DECLARED assoc_comm OR
commutative, THIS FLAG WILL BE AUTOMATICALLY CLEARED, because binding
discrimination tree indexing does not handle those properties. If set,
index for forward subsumption. If clear, do not index for forward
subsumption.
index_conflict - default set. IF ANY SYMBOLS ARE DECLARED assoc_comm OR
commutative, THIS FLAG WILL BE AUTOMATICALLY CLEARED, because FPA/Path
indexing does not handle those properties. If set, use FPA/Path
indexing for unit conflict. If clear, do not index for unit
conflict.
print_kept - default set. If set, inferred clauses that pass the
retention tests are printed to the output file.
print_new_demod - default set. If set, newly adjoined demodulators
are printed to the output file.
delay_back_demod - default clear. If set, back demodulate with a
newly adjoined demodulator when (if) it is selected as a given clause
rather than immediately when it is adjoined. WARNING: This flag
has not been well tested and might not even be fully implemented.
delay_new_demod - default clear. Not currently in use.
demod_given - default clear. Not currently in use.
back_demod_sos - default set. Not currently in use.
ordered_paramod - default clear. This is relevant only if the
flags index_paramod (e.g., there are no assoc_comm or commutative
symbols) and lrpo are set. If set, paramodulation will not replace
a term with an LRPO-larger term.
ac_extend - default set. If set, extensions of AC-rooted equations are
used for AC paramodulation. If clear, no extensions are used.
functional_subsume - default clear. If set, apply functional subsumption,
that is subsumption modulo functional substitution axioms. For example,
a=b subsumes f(a)=f(b).
basic_paramod - default clear. If set, apply the "basic" refinement
of paramodulation.
prime_paramod - default clear. If set, do not generate a paramodulant
if any term in the substitution is reducible with the current
set of demodulators.
fpa_delete - default clear. If set, delete terms from the FPA/Path
index when the containing clauses are disabled. One might think
that we should always do so, but it can be a very expensive operation
(because of naive implementation), and it does not hurt to leave
them there. Recall that when a clause is no longer useful (back
demodulated or back subsumed) it is disabled, but not actually
deleted.
4.2. PARAMETERS
max_mem - range [-1 .. INT_MAX], default 8000. This is the limit,
in kilobytes, on dynamically allocated memory. A value of -1 means
that there is no limit.
max_weight - range [-INT_MAX .. INT_MAX], default INT_MAX.
This is the weight limit for kept clauses. The weight is symbol count
(the total number of constant, variable, function, and predicate symbols).
There are weight lists as in Otter.
max_given - range [0 .. INT_MAX], default INT_MAX.
The search will stop after this many given clauses of given pairs.
weight_function - range [0 .. INT_MAX], default 0. This is for
orienting equality literals. There are currently two choices: 0 means
to use symbol count (see Section 5), and 1 is a special-purpose
polynomial ordering for ring problems (see the source code).
It should not be difficult to add your own function by writing
a little C code.
max_proofs - range [1 .. INT_MAX], default 1.
The search will stop after this many proofs have been found.
report_given - range [1 .. INT_MAX], default INT_MAX.
Statistics are sent to the output file at intervals of this
many seconds.
ac_superset_limit - range [-1 .. INT_MAX], default -1.
This controls the "heuristic" super restriction on AC unifiers.
-1 means no restriction, 0 means super-0, etc. See [2] for
details.
max_seconds - range [0 .. INT_MAX], default INT_MAX.
The search will stop after this many seconds.
pick_given_ratio - range [-1 .. INT_MAX], default -1. This is the
shortest-first to breadth-first selection ratio. It applies to both
the given clause algorithm (para_pairs clear) and the pair algorithm
(para_pairs set). See [2] for details.
fpa_depth - range [0 .. INT_MAX], default 8. This is the indexing
depth for FPA/Path indexing. 0 means to index on the root symbol only.
pair_index_size - range [1 .. 100], default 50.
This is the size of the pair index. You probably won't need to change it
(I never have).
max_variables - range [0 .. INT_MAX], default INT_MAX.
This is a limit on the number of (distinct) variables for
kept clauses. That is, if the value is 2, then derived clauses
with more than 2 variables will be deleted.
5. TERM ORDERING
Term ordering is very important for many equational problems. In
particular it is used to orient equations and to decide if equations
should be rewrite rules (demodulators). When no symbols are declared
to be assoc_comm (AC) or commutative (C), I recommend using the LRPO
ordering (via set(lrpo)). (LRPO is okay with associativity and/or
commutativity as axioms.)
EQP's term ordering with symbols declared to be AC or C is quite weak.
If symbols are declared to be AC or C, do not use LRPO. (There are
LRPO orderings that work with AC and C symbols, but none are
implemented in EQP.)
The default term ordering (and the one I have used for almost all of
my AC work so far) is simple: t1 > t2 if t1 has more symbols than t2
and no variable has more occurrences in t2 than in t1. This is
clearly a simplification ordering, because each application of a
demodulator t1=t2, with t1 > t2, reduces the number of symbols.
However, this ordering is not very powerful and it will probably not
be useful if you are looking for a complete set of reductions. (My
view is that for theorem proving, it is not particularly important to
try to make all equations into rewrite rules.) Also, this order
cannot be used to expand terms with definitions.
In order to prove some of the benchmark ring theory problems, I coded
Stickel's polynomial ordering (see Stickel's 1984 CADE paper).
which is activated with assign(weight_function, 1). One can
easily add new polynomial orderings (or other kinds of orderings)
by adding new C code to EQP.
References
1. W. McCune, Otter 3.0 Reference Manual and Guide. Tech. Report
ANL-94/6, Argonne National Laboratory, 1994. (Also available from
http://www.mcs.anl.gov/AR/otter/.)
2. W. McCune, 33 Basic Test Problems: A Practical Evaluation of Some
Paramodulation Strategies. Chapter 5 in "Automated Reasoning and its
Applications: Essays in Honor of Larry Wos", ed. R. Veroff, MIT Press
(1997).
3. W. McCune, EQP Web page, http://www.mcs.anl.gov/AR/eqp/.
4. W. McCune, Otter Web page, http://www.mcs.anl.gov/AR/otter/.
5. W. McCune, Solution of the Robbins Problem. To appear in Journal of
Automated Reasoning, 1997.