Database of Existing Mechanized Reasoning Systems
This page represents the current state
of an ongoing effort to collect information about existing
automated reasoning systems.
One objective is to provide concise
useful information for people who have need for such a system and don't want
to `roll their own'. Another objective is to provide a single place
where information about existing systems can be accessed,
thus providing an overview of the state of the art.
This page is split into three parts:
Reasoning Tools Executable via the Web,
Entries in the available systems part are restricted to reasoning systems
and tools that are implemented and available to outside users.
Systems falling outside that category are listed in the others part.
for a general mechanized reasoning page.
We attempt to provide for each entry:
a one sentence description;
a link to a brief overview;
a link to a home page for the entry;
and possibly other relevant information or links.
In addition to individual there is a list of automated reasoning related
mailing lists, and a list of related pages.
Please send email to
Michael Kohlhase firstname.lastname@example.org
Carolyn Talcott email@example.com
if you know of implementations missing from this database,
would like modify the information about your system,
or if you have suggestions for making the database more useful.
is an automatic/interactive prover for a large subset of applicative
Af2 is a type system based on second order intuitionistic logic.
CtCoq -- a working environment for COQ
CHOL -- a user-interface for HOL
Contact: Laurent Théry Laurent.Thery@inria.fr
CLAM -- an automated tactical theorem prover with proof planning,
inductive and meta-level reasoning.
Concurrency Workbench (CWB) is an automated tool for manipulation
and analysis of concurrent systems.
Contact: Perdita Stevens, University of Edinburgh
CWB web page.
The Concurrency Workbench of North Carolina (CWB-NC)
supports the automatic verification of finite-state
a proof assistant base on the calculus of inductive constructions.
Deep Thought (DT) is an automated free variable analytic
tableau prover for first order finitely many-valued logic
Contact: S. Gerberding
DT web page
E is a theorem prover for clausal logic with equality. It is based on
superpostion and rewriting.
Contact: Stephan Schulz firstname.lastname@example.org
ECLiPSe -- a generic system for development of constraint solvers,
with several libraries of constraint solvers for use in applications.
EHDM (Enhanced Hierarchical Development Methodology) --
a proof system for classical higher-order logic with powerful ground
ELAN is an environment to prototype the
combination of different computational systems that provide a basis for
constraint solving, theorem proving and logic programming paradigms.
a system based on predicative type theory that can be used to specify
and reason about logics, languages, type systems, etc.
-- an untyped first-order theorem prover for the Verdi specification
system providing a balance of powerful decision procedures and user guidances.
Expander is a proof and test environment for algebraic data type specifications
and functional-logic programs.
Gandalf is a theorem prover for classical first order logic.
GETFOL -- a proof system for sorted first order logic
based on R. Weyhrauch's FOL.
ft -- an intuitionistic predicate logic theorem prover
an interactive environment for machine-assisted
theorem-proving in higher-order logic.
HOL Light -- a small clean HOL implementation
Contact: John Harrison email@example.com
The Imperial College Logic Environment (ICLE)
is designed to assist in the development of
Gentzen-style presentations of logics. Besides this it can be used to
develop type inference systems and other proof theoretic presentations
of logics. Derivations can be easily constructed.
ILF is a shell that facilitates the work with a variety of theorem provers.
Contact: The ILF group
The ILF System
-- is an interactive proof system based on a nonconstructive
version of simple type theory with partial functions and subtypes,
with a theory interpetation mechanism.
INKA is a first-order theorem prover with induction
which is based on the explicit induction paradigm.
a generic theorem prover in which logics can be specified
Lawrence C. Paulson Larry.Paulson@cl.cam.ac.uk
Tobias Nipkow Tobias.Nipkow@informatik.tu-muenchen.de
Isabelle web page
Jape (Just Another Proof Editor)
is a generic interactive proof editor.
KEIM (Kernel for Enhancement of Implementation and Maintenance)
an extensitble toolbox for the development of deduction systems.
KIV is an interactive system designed for formal
reasoning about imperative programs.
Andreas Wolpers firstname.lastname@example.org
KIV web page
Kripke prover -- a theorem prover for the Relevant Logic LR.
LAMBDA -- a toolset that supports formal verification for
Contact: Abstract Hardware Ltd, UK, email@example.com
LA (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
LeanTAP -- a micro prolog prover for FOL
Bernhard Beckert Beckert@ira.uka.de
Joachim Posegga Posegga@ira.uka.de
LeanTAP web page
LEGO A Proof Assistant based on type theory.
Logics Workbench (LWB): mastering propositional logics on the computer
LPTP is an interactive theorem prover for the formal verification of
pure Prolog programs.
MARK2 - an equational theorem prover
Merill -- an order-sorted equational reasoning system
Metamath - An extremely simple, universal language for expressing
theorems and proofs. Logic is not built-in but desired axioms are
provided by user.
Contact: Norman Megill, firstname.lastname@example.org
A proof-verifier, MetaMath book and sample database
covering ZF set theory are available via anonymous fto
to ftp.shore.net in the directory members/ndm.
Mizar is a system for writing and checking formal mathematics,
based on Tarski-Grothendieck set theory, and natural deduction.
is an implementation of decision procedures for weak second-order
logics of successors.
is a prover for quantifier free logic for recursive functions
over the integers and other finitely generated structures, combining
rewriting, heuristics for induction, and other techniques.
is a proof system for an intuitionistic type theory
based on Martin Lof type theory, with proof by refinement
and extraction of programs from proofs.
OBJ3 is based on order-sorted equational logic, with
computation/deduction via rewriting modulo associative, commutative,
and/or identity equations.
OSHL is a first-order based on a novel first order theorem proving strategy
-- ordered semantic hyper linking.
David Plaisted email@example.com
Yunshan Zhu firstname.lastname@example.org
OSHL web page
Otter is an automated resolution prover for first-order logic.
OSCAR is a fully implemented architecture for rational agents,
based upon a general purpose defeasible reasoner.
Oyster is an Edinburgh implementation of the
Pc-Nqthm (Proof-Checker Nqthm) is an
enhancement to the Boyer-Moore prover
that provides further interactive capabilities and first-order quantification.
Porgi -- a Proof-Or-Refutation Generator for Intuitionistic
ProCom is a theorem prover based on the PTTP paradigm
ProofPower -- a specification and proof tool based on an
implementation of Higher Order Logic (HOL), with
support for specification and proof in Z.
PROTEIN (PROver with a Theory Extension Interface)
is an automated prover for first-order clause logic.
Prover (NP-Tools) -- an automated prover for propositional logic
that produces a counter model
if no proof is found, and allows models of systems to be built using
propositional logic (diagrams or text).
Graeme I Parkin (United Kingdom) email@example.com
Gunnar Stalmarck (Sweden)
Tel: +46 8 615 68 60, FAX: +46 8 641 19 06
PVS (Prototype Verification System) is a specification/verification
system based on higher-order logic.
ReDuX is a work-bench for programming and experimenting with
term rewriting systems.
Contact: Reinhard Buendgen, firstname.lastname@example.org
ReDuX web page
RRL (Rewrite Rule Laboratory) is a tool for automatic
proof of theorems in first-order predicate calculus with equality.
Deepak Kapur email@example.com
Hantao Zhang firstname.lastname@example.org
SATURATE -- a saturation-based theorem prover for first-order logic
with transitive relations.
Harald Ganzinger email@example.com
Robert Nieuwenhuis firstname.lastname@example.org
SATURATE home page
SDVS (State Delta Verification System)
is based on a version of temporal logic structured in order to
of computations and proofs by symbolic execution.
Setheo (SEquential THEOrem prover) -- a high performance theorem prover for full first order logic
SPASS and FLOTTER are prototypes of a first-order theorem prover and a
Contact: Christoph Weidenbach email@example.com
SPIN is an automated verification tool (model checker), based on CSP.
Gerard Holzmann, firstname.lastname@example.org
SPIN web page
is a system for developing proofs in classical first-order logic
using deductive tableaux graphical notation.
3TAP -- a tableaux based theorem prover for many-valued first-order logics.
TempEst is a toolset for the formal verification of safety
properties of programs written in the Esterel programming language.
The Theorema project aims at extending current computer algebra systems by
facilities for supporting mathematical proving.
Tools for TLA (Temporal Logic of Actions) based specifications.
is a theorem proving system for first- and higher-order logic with
both automatic and interactive modes.
UV (UNITY Verifier) System - an interactive symbolic model checker
Verification Execution and Rewrite System for ACSR
(VERSA) is an automated tool for analyzing resource-bound real-time
systems using the ACSR Process Algebra.
Verification Support Environment (VSE) too
to support formal software development.
Dieter Hutter email@example.com
Werner Stephan firstname.lastname@example.org
Yarrow is a proof-assistant for Pure Type Systems (PTSs)
WinKE is an interactive theorem proving assistant based on the KE calculus,
developed to support teaching logic and reasoning to undergraduates.
This page comes to you courtesy of
Michael Kohlhase and
Last updated 1 June 1999.
Last updated June 18, 1999.