\documentclass[11pt,a4paper]{article}
\begin{document}

\section{ Mechanized Reasoning Systems}
\section{ 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.  

\par

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
or

here
for a general  mechanized reasoning page.


\par

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.

\par

Please send email to 

Michael Kohlhase {\bf  kohlhase@cs.uni-sb.de  } 
(clidk {\tt 
here})
or

Carolyn Talcott {\bf clt@sail.stanford.edu}
(click {\tt 
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.



\par





\subsection{ Available  Systems and Tools
}
\begin{itemize}

\item  ACL2
  is an automatic/interactive prover for a large subset of applicative 
Common Lisp
\begin{itemize}
\item 

   Brief Description 
\item Contact:
J Strother Moore  {\bf  moore@cli.com } 
Matt Kaufmann {\bf matt\_kaufmann@email.mot.com} 
\item 
 ACL2 web page 
\end{itemize}\par

\item 
CtCoq -- a working environment for COQ
\begin{itemize}
\item Contact: {\bf ctcoq-request@sophia.inria.fr }
\item web page 
\end{itemize}\par

\item 
CHOL -- a user-interface for HOL
\begin{itemize}
\item Contact: Laurent Théry {\bf  Laurent.Thery@inria.fr  }
\item  web page 
\end{itemize}\par


\item 
CLAM -- an automated tactical theorem prover with proof planning,
inductive  and meta-level reasoning.
\begin{itemize}
\item 

   Brief Description 
\item Contact: {\bf  dream@ai.ed.ac.uk}
\item  DReaM group home page 
\end{itemize}\par


\item Concurrency Workbench (CWB) is an automated tool for manipulation
and analysis of concurrent systems.
\begin{itemize}
\item Contact: Perdita Stevens, University of Edinburgh
 {\bf Perdita.Stevens@dcs.ed.ac.uk}
\item  CWB web page.
\end{itemize}\par

\item Coq --
a proof assistant base on the  calculus of inductive constructions. 
\begin{itemize}
\item 

   Brief Description 
\item Contact: Gerard Huet {\bf  Gerard.Huet@inria.fr}
\item Coq web page
\end{itemize}\par

\item 
ECLiPSe  -- a generic system for development of constraint solvers,
with several libraries of constraint solvers for use in applications.
\begin{itemize}
\item Contact: {\bf eclipse\_request@ecrc.de}
\item 
  Eclipse web page 
\end{itemize}\par

\item EHDM (Enhanced Hierarchical Development Methodology) --
a proof system for classical higher-order logic with powerful ground
decision procedures. 
\begin{itemize}
\item 

   Brief Description 
\item Contact:  John Rushby, Sam Owre  {\bf \{rushby,owre\}@csl.sri.com}
\end{itemize}\par

\item 
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.
\begin{itemize}
\item 
Contact: ELAN's team {\bf  elan@loria.fr }
\item 

ELAN web page 
\end{itemize}

\item Elf  --
a system based on predicative type theory that can be used to specify
and reason about logics, languages, type systems, etc.
\begin{itemize}
\item 

   Brief Description 
\item Contact:  
 Frank Pfenning
 {\bf fp@cs.cmu.edu}
\item 
  Elf web page 
\end{itemize}\par

\item EVES/NEVER
-- an untyped first-order theorem prover for the Verdi specification
system providing a balance of powerful decision procedures and user guidances.
\begin{itemize}
\item 

   Brief Description 
\item Contact:
Dan Craigen {\bf dan@ora.on.ca}
\item 

  EVES web page \item 

  ORA web page 
\end{itemize}\par

\item 
Expander is a proof and test environment for algebraic data type specifications
and functional-logic programs. 
\begin{itemize}
\item 
Contact: Peter Padawitz {\bf peter@issan.informatik.uni-dortmund.de  }
\item 

Expander web page 
\end{itemize}\par

\item GETFOL -- a proof system for sorted first order logic
 based on R. Weyhrauch's FOL.
\begin{itemize}
\item 

   Brief Description 
\item 
Contact:  Fausto Giunchiglia, {\bf getfol@frege.mrg.dist.unige.it}
\item 
 FOL web page 
\end{itemize}\par

\item ft -- an intuitionistic predicate logic theorem prover
\begin{itemize}
\item 
Contact: Torkel Franzen (torkel@sics.se)
\item 
 ft web page 
\end{itemize}\par

\item HOL -- 
 an interactive environment for machine-assisted 
 theorem-proving in higher-order logic.
\begin{itemize}
\item 

   Brief Description 
\item Contact: \begin{itemize}
  \item {\bf hol-support@cl.cam.ac.uk}
  \item John Harrison {\bf jrh@cl.cam.ac.uk}
  \item Phillip J. WIndley 
  \end{itemize}
\item 

HOL page at BYU (on-line documentation)
\item 
 
HOL page at Oxford
\item 
 
HOL page at Cambridge
\end{itemize}\par

\item 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.  
\begin{itemize}
\item 

 brief summary
\item 
Contact:
Mark Dawson
{\bf  md@doc.ic.ac.uk }

\item 

ftp site

\end{itemize}\par


\item 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.
\begin{itemize}
\item 

   Brief Description 
\item Contact:    William M. Farmer, Joshua D. Guttman, F. Javier Thayer
     {\bf  \{farmer,guttman,jt\}@mitre.org }
\item 
             IMPS web page 
\end{itemize}\par


\item INKA is a first-order theorem prover with induction
which is based on the explicit induction paradigm. 
\begin{itemize}
\item Contact:
Dieter Hutter {\bf hutter@dfki.uni-sb.de}
\item 
     INKA web page 
\end{itemize}\par


\item Isabelle --
 a generic theorem prover in which logics can be specified
and used.
\begin{itemize}
\item Contact:
Lawrence C. Paulson  {\bf Larry.Paulson@cl.cam.ac.uk}
Tobias Nipkow  {\bf Tobias.Nipkow@informatik.tu-muenchen.de }
\item 
     Isabelle web page 
\end{itemize}\par

\item Jape (Just Another Proof Editor)
is a generic interactive proof editor.
\begin{itemize}
\item Contact:
  Bernard Sufrin {\bf Bernard.Sufrin@comlab.ox.ac.uk}
  Richard Bornat (London University)
\item 

Jape web page 
\item  anonymous FTP
\end{itemize}\par

\item 
KEIM (Kernel for Enhancement of Implementation and Maintenance)
an extensitble toolbox for the development of deduction systems.
\begin{itemize}
\item Contact: {\bf keim@cs.uni-sb.de}
\item 
 
  KEIM web page 
\end{itemize}\par

\item 
 KIV is an interactive system designed for formal
reasoning about imperative programs.
\begin{itemize}
\item Contact:
Andreas Wolpers {\bf wolpers@dfki.uni-sg.de}
\item 
     KIV web page 
\end{itemize}\par

\item Kripke prover -- a theorem prover for the Relevant Logic LR.
\begin{itemize}
\item Contact:
Gustav Meglicki, {\bf gustav@arp.anu.edu.au}
\item 
ARP home page 
\end{itemize}\par

\item LAMBDA -- a toolset that supports formal verification for 
hardware/software co-design.  
\begin{itemize}
\item Contact:  Abstract Hardware Ltd, UK, {\bf lambda@ahl.co.uk} 
\end{itemize}\par

\item 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. 
\begin{itemize}
\item 

   Brief Description 
\item Contact:
John Garland {\bf garland@lcs.mit.edu},
John Guttag {\bf guttag@lcs.mit.edu}
\item 

   LP web page
\item See also
 
   Larch home page
\end{itemize}\par    

\item 
LeanTAP -- a micro prolog prover for FOL
\begin{itemize}
\item Contact:
Bernhard Beckert {\bf Beckert@ira.uka.de}

Joachim Posegga {\bf Posegga@ira.uka.de}
\item 

   LeanTAP web page 
\end{itemize}\par

\item LEGO A Proof Assistant based on type theory.
\begin{itemize}
\item 
Contact: {\bf lego@dcs.ed.ac.uk}
\item 
 LEGO web page
\end{itemize}\par

  \item 
  Logics Workbench (LWB): mastering propositional logics on the computer
  \begin{itemize}
  \item Contact: {\bf lwb@iam.unibe.ch}
  \item LWB web page
  \end{itemize}\par

\item Merill -- an  order-sorted equational reasoning system
\begin{itemize}
\item 

   Brief Description 
\item 
Contact: Brian Matthews {\bf bmm@inf.rl.ac.uk}
\item 
ftp 
\end{itemize}\par

\item 
Metamath - An extremely simple, universal language for expressing 
theorems and proofs.  Logic is not built-in but desired axioms are 
provided by user.  
\begin{itemize}
\item Contact: Norman Megill, {\bf  ndm@shore.net }
\item 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.
\end{itemize}\par

\item 
Mizar is a system for writing and checking formal mathematics,
based on  Tarski-Grothendieck set theory, and natural deduction.
\begin{itemize}
\item Contact: Piotr Rudnicki, {\bf  piotr@cs.ualberta.ca }
\item 

Mizar web page
\end{itemize}\par

\item 
 MuRal
\begin{itemize}
\item Contact:
 Brian Ritchie
 {\bf br@inf.rl.ac.uk}
\item 
MuRal web page 
\end{itemize}\par

\item  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.
\begin{itemize}
\item 

   Brief Description 
\item Contact:
Robert S. Boyer  {\bf  boyer@cli.com } 
J. Strother Moore {\bf moore@cli.com} 
\item 
 Nqthm ftp 
\item See also:
 Computational Logic Inc.
\end{itemize}\par

\item  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.
\begin{itemize}
\item 

   Brief Description 
\item Contact: {\bf nuprl@cs.cornell.edu}
\item 

NUPRL web page 
\end{itemize}\par

\item 
OBJ3 is based on order-sorted equational logic, with
computation/deduction  via rewriting modulo associative, commutative, 
  and/or identity equations.
\begin{itemize}
\item 

   Brief Description 
\item Contact:
Joseph Goguen {\bf  goguen@prg.oxford.ac.uk }
Jose Meseguer {\bf meseguer@csl.sri.com}
\item  OBJ web page 
\end{itemize}\par

\item Otter is an automated resolution prover for first-order logic.
\begin{itemize}
\item 

   Brief Description 
\item Contact:
William McCune   
{\bf  mccune@mcs.anl.gov}
\item 

Otter web page
\item 
ATP at Argonne
\end{itemize}\par

\item Oyster is an Edinburgh implementation of the 
 Nuprl  System.
\begin{itemize}
\item 

   Brief Description 
\item Contact:  {\bf dream@ai.ed.ac.uk}
\item  DReaM group home page 
\end{itemize}\par

\item Pc-Nqthm (Proof-Checker Nqthm) is an
enhancement to the  Boyer-Moore prover  
that provides further interactive capabilities and first-order quantification.
\begin{itemize}
\item 

   Brief Description 
\item Contact: Matt Kaufmann {\bf kaufmann@cli.com}
\item 
 Pc-Nqthm ftp 
\end{itemize}\par

\item Porgi -- a Proof-Or-Refutation Generator for Intuitionistic
         propositional logic.
\begin{itemize}
\item 

   Brief Description 
\item Contact: Allen Stoughton {\bf allen@cis.ksu.edu}
\item 
 Porgi web page 
\end{itemize}\par


\item ProCom is a theorem prover based on the PTTP paradigm
\begin{itemize}
\item 
Contact: Gerd Neugebauer {\bf gerd@imn.th-leipzig.de}
\item 
 
ProCom web page 
\end{itemize}\par

\item ProofPower -- a specification and proof tool based on an 
implementation of Higher Order Logic (HOL), with
support for specification and proof in Z.
\begin{itemize}
\item 
Contact: ProofPower-support@win.icl.co.uk 
\item 

   ProofPower web page 
\end{itemize}\par

\item PROTEIN  (PROver with a Theory Extension Interface)
is an automated prover for first-order clause logic.
\begin{itemize}
\item 
Contact: Peter Baumgartner {\bf peter@informatik.uni-koblenz.de }
\item 
 PROTEIN web page 
\end{itemize}\par

\item 
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).
\begin{itemize}
\item 

   Brief Description 
\item Contact:
\begin{itemize}
\item Graeme I Parkin (United Kingdom) {\bf   gip@cise.npl.co.uk }
\item Gunnar Stalmarck (Sweden) 
  {\bf Tel: +46 8 615 68 60,  FAX: +46 8 641 19 06}
\end{itemize}
\end{itemize}\par

\item PVS (Prototype Verification System) is a specification/verification
system based on higher-order logic.
\begin{itemize}
\item 

   Brief Description 
\item Contact: John Rushby, N. Shankar, Sam Owre
{\bf  \{rushby,shankar,owre\}@csl.sri.com}
\item 
 PVS home page
\end{itemize}\par

\item ReDuX is a work-bench for programming and experimenting with
term rewriting systems.
\begin{itemize}
\item Contact: Reinhard Buendgen, {\bf buendgen@informatik.uni-tuebingen.de}
\item 

ReDuX web page
\end{itemize}\par

\item RRL (Rewrite Rule Laboratory) is a tool for automatic
proof of theorems in first-order predicate calculus with equality.
\begin{itemize}
\item 

   Brief Description 
\item Contact: 
Deepak Kapur {\bf kapur@cs.albany.edu }
Hantao Zhang {\bf hzhang@cs.uiowa.edu}
\end{itemize}\par


\item SATURATE -- a saturation-based theorem prover for first-order logic
with transitive relations.
\begin{itemize}
\item Contact:
Harald Ganzinger {\bf hg@mpi-sb.mpg.de} 
Robert Nieuwenhuis {\bf roberto@lsi.upc.es}
\item 
  SATURATE home page 
\end{itemize}\par


\item 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. 
\begin{itemize}
\item 

   Brief Description 
\item Contact:
Ranwa Haddad {\bf haddad@aero.org} 
Leo Marcus {\bf marcus@aero.org}
\end{itemize}\par


\item Setheo (SEquential THEOrem prover) -- a high performance theorem prover for full first order logic
\begin{itemize}
\item 
Contact: {\bf setheo@informatik.tu-muenchen.de}
\item 
  Setheo web page 
\end{itemize}\par


\item SPIN is an automated verification tool (model checker), based on CSP.
\begin{itemize}
\item 
Contact: 
Gerard Holzmann, {\bf gerard@research.att.com}
\item 

SPIN web page 
\end{itemize}\par

\item Tableaux
is a system for developing proofs in classical first-order logic
using deductive tableaux graphical notation.
\begin{itemize}
\item 

   Brief Description 
\item Contact:
Ron Burback
{\bf  burback@neon.stanford.edu}
\end{itemize}\par


\item 
3TAP -- a  tableaux based theorem prover for many-valued first-order logics.
\begin{itemize}
\item 

   Brief Description 
\item Contact:
 Reiner Haehnle or Bernhard Beckert {\bf \{haehnle,beckert\}@ira.uka.de}
\item   3TAP web page 
\end{itemize}\par

\item Tools for TLA (Temporal Logic of Actions) based specifications.
\begin{itemize}
\item Contact: 
Heiko Krumm {\bf krumm@ls4.informatik.uni-dortmund.de }
\item 
Tools for TLA web page
\item See also
 
   TLA web page 
\end{itemize}\par

\item TPS
 is a theorem proving system for first- and higher-order logic with
both automatic and interactive modes.
\begin{itemize}
\item 

   Brief Description 
\item Contact: 

   Peter Andrews.
 {\bf Peter.Andrews@cs.cmu.edu}
\item 

 The TPS THEOREM PROVING SYSTEM
\end{itemize}\par


\item UV (UNITY Verifier) System - an interactive symbolic model checker 
for UNITY.
\begin{itemize}
\item Contact: Markus Kaltenbach {\bf markus@cs.utexas.edu}
\item 
 UV web page 
\item See also: 
UNITY web page
\end{itemize}\par

\item 
Verification Execution and Rewrite System for ACSR
(VERSA) is an automated tool for analyzing resource-bound real-time
systems using the ACSR Process Algebra. 
\begin{itemize}
\item Contact:
 {\bf  versa@saul.cis.upenn.edu }
\item 
     VERSA web page 
\end{itemize}\par

\item 
Verification Support Environment (VSE) too
to support formal software development.
\begin{itemize}
\item 
Contacts: 
Dieter Hutter {\bf  hutter@dfki.uni-sb.de } 
Werner Stephan {\bf  stephan@dfki.uni-sb.de}
\item 
web page
\end{itemize}


\end{itemize}


\subsection{ Other Existing  Systems and Tools
}
\begin{itemize}

\item CRACK a description logics evaluator



\item SPTHEO (parallel theorem prover based on SETHEO)


\item 
Teamwork  (Distributed automated theorem proving)


\item 
 
Clause-Diffusion theorem provers  
( experimentall prototypes for distributed deduction )

\end{itemize}

This page comes to you courtesy of

Michael Kohlhase and

Carolyn Talcott.
\par

Last updated 8 August 1996.

 

\end{document}