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 two parts:
available systems and others.
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 mechanised 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
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.
a proof assistant base on the calculus of inductive constructions.
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.
GETFOL -- a proof system for sorted first order logic
based on R. Weyhrauch's FOL.
an interactive environment for machine-assisted
theorem-proving in higher-order logic.
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.
-- 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 framework for building proof-calculators.
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.
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 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.
Otter is an automated resolution prover for first-order logic.
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.
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
SPIN is an automated verification tool (model checker), based on CSP.
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.
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
This page comes to you courtesy of
Michael Kohlhase and
Last updated 6 May 1996.