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.
Click
here (USA)
or
here (Germany)
for a general mechanised reasoning page.
We attempt to provide for each entry:
a one sentence description;
a link to a brief overview;
contact information;
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 kohlhase@cs.uni-sb.de
(click
here )
or
Carolyn Talcott clt@cs.stanford.edu
(click
here )
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.
- ACL2
is an automatic/interactive prover for a large subset of applicative
Common Lisp
-
CtCoq -- a working environment for COQ
- Contact: ctcoq-request@sophia.inria.fr
- web page
-
CHOL -- a user-interface for HOL
- Contact: Laurent Th駻y Laurent.Thery@inria.fr
- web page
-
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
Perdita.Stevens@dcs.ed.ac.uk
- CWB web page.
- Coq --
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
decision procedures.
-
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.
- Elf --
a system based on predicative type theory that can be used to specify
and reason about logics, languages, type systems, etc.
- EVES/NEVER
-- 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.
- HOL --
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.
- IMPS
-- 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.
- Isabelle --
a generic theorem prover in which logics can be specified
and used.
- Contact:
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.
- Contact:
Andreas Wolpers wolpers@dfki.uni-sg.de
-
KIV web page
- Kripke prover -- a theorem prover for the Relevant Logic LR.
- LAMBDA -- a toolset that supports formal verification for
hardware/software co-design.
- Contact: Abstract Hardware Ltd, UK, lambda@ahl.co.uk
- 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
automatically.
-
LeanTAP -- a micro prolog prover for FOL
- Contact:
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, ndm@shore.net
- 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.
-
MuRal
- NQTHM
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.
- NUPRL
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
Nuprl System.
- 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).
-
Brief Description
- Contact:
- Graeme I Parkin (United Kingdom) gip@cise.npl.co.uk
- 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, buendgen@informatik.uni-tuebingen.de
-
ReDuX web page
- RRL (Rewrite Rule Laboratory) is a tool for automatic
proof of theorems in first-order predicate calculus with equality.
-
Brief Description
- Contact:
Deepak Kapur kapur@cs.albany.edu
Hantao Zhang hzhang@cs.uiowa.edu
- 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
- SDVS (State Delta Verification System)
is based on a version of temporal logic structured in order to
facilitate specification
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.
- Tableaux
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.
- TPS
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
for UNITY.
-
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.
-
Contacts:
Dieter Hutter hutter@dfki.uni-sb.de
Werner Stephan stephan@dfki.uni-sb.de
-
web page
This page comes to you courtesy of
Michael Kohlhase and
Carolyn Talcott.
Last updated 6 May 1996.