- CiME - a tool for checking termination
and confluence of rewrite systems modulo equational theories, and for
completion of such systems. Includes the Normalized completion
algorithm and the dependency pairs criterion for termination. Also
provides unification algorithms modulo Associativity and Commutativity,
Abelian Groups and Boolean Rings.
- daTac - a theorem prover for first-order logic
with equality and AC operators, implementing the ordering and basic
- E Prover (Equational Theorem Prover) - a high
performance purely equational theorem prover for clausal logic.
- EQP - an automated prover for first-order
equational logic. EQP has AC unification, and it does well on many
problems about lattice-like structures.
- LP (the Larch Prover) - a first order prover
designed for a middle ground between proof checkers that require
detailed guidance and theorem provers that work completely
- ReDuX - a work-bench for programming and
experimenting with term rewriting systems.
- SATURATE - a saturation-based theorem prover for
first-order logic with transitive relations.
- SETHEO (SEquential THEOrem prover) - a high
performance theorem prover for full first order logic.
- SPIKE - a theorem prover for first-order logic
and inductive reasoning.
- Watson - an interactive equational theorem
prover, where theorems are rewrite rules, with a programming language
(programs are systems of recursively chained rewrite rules, proved and
stored in the same way as theorems), and with dedicated features for
reasoning about expressions defined by cases and supporting a
higher-order logic with the strength of type theory.