Rewriting-Based Provers

• 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.
  • Contact: Claude Marché <Claude.Marche @ lri.fr>
  • CiME home page
• daTac - a theorem prover for first-order logic with equality and AC operators, implementing the ordering and basic strategies.
  • Contact: Laurent Vigneron <vigneron @ loria.fr>
  • daTac home page
• E Prover (Equational Theorem Prover) - a high performance purely equational theorem prover for clausal logic.
  • Contact: Stephan Schulz, schulz @ informatik.tu-muenchen.de
  • E Prover home page
• EQP - an automated prover for first-order equational logic. EQP has AC unification, and it does well on many problems about lattice-like structures.
  • Contact: William McCune <mccune @ mcs.anl.gov>
  • EQP home page
• 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 automatically.
  • Contact: Stephen J. Garland <garland @ lcs.mit.edu>
  • LP home page
• ReDuX - a work-bench for programming and experimenting with term rewriting systems.
  • Contact: Reinhard Bündgen <buendgen @ informatik.uni-tuebingen.de>
  • ReDuX home page
• SATURATE - a saturation-based theorem prover for first-order logic with transitive relations.
  • Contact: Harald Ganzinger <hg @ mpi-sb.mpg.de>, Robert Nieuwenhuis <roberto @ lsi.upc.es>
  • SATURATE home page
• SETHEO (SEquential THEOrem prover) - a high performance theorem prover for full first order logic.
  • Contact: Gernot Stenz, setheo @ informatik.tu-muenchen.de
  • SETHEO home page
• SPIKE - a theorem prover for first-order logic and inductive reasoning.
  • Contact: Michaël Rusinowitch <rusi @ loria.fr>
  • SPIKE home page
• 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.
  • Contact: Randall Holmes <holmes @ math.boisestate.edu>
  • Watson home page