# Equational Prover

EQP is an automated theorem proving program for first-order
equational logic. Its strengths are good implementations
of associative-commutative unification and matching,
a variety of strategies for equational reasoning, and
fast search. It seems to perform well on many problems
about lattice-like structures.
EQP is not as stable and polished as our main production theorem
prover
Otter. But it has obtained several interesting results, and we
have decided to make it available (including the source code) to
everyone, with no restrictions (and of course no warranty).
EQP's documentation is not good, but if you already know Otter,
you might not have great difficulty in learning to use EQP.

### Download

The whole package, including the source code,
users' guide, and example input files:
For a quick preview, see the
README file,
the
users' guide,
and the
ChangeLog file.

## Related Pages