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:
available systems,
Reasoning Tools Executable via the Web,
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 mechanized 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
(clidk
here)
or
Carolyn Talcottclt@sail.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.
Contact: John Rushby, Sam Owre {rushby,owre}@csl.sri.com
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.
EVES/NEVER
-- an untyped first-order theorem prover for the Verdi specification
system providing a balance of powerful decision procedures and user guidances.
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.
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.
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.
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.
Pc-Nqthm (Proof-Checker Nqthm) is an
enhancement to the Boyer-Moore prover
that provides further interactive capabilities and first-order quantification.
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).
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.
Verification Execution and Rewrite System for ACSR
(VERSA) is an automated tool for analyzing resource-bound real-time
systems using the ACSR Process Algebra.
SCAN
is a program for computing first-order equivalent formulae for
second-order formulae with quantified predicate variables.
Interfaces for computing circumscription and for computing
correspondence axioms in non-classical logics are available.
Contact:
Hans Jürgen Ohlbach
Parthenon -
a resolution theorem prover
that runs on a parallel machine and can handle non-Horn clauses -
by
Edmund Clarke (Edmund.Clarke@g.gp.cs.cmu.edu) et al.
Linseq/Linres - tableau-style/resolution-style provers
for full first-order propsitional logic -
by T. Tammet
(look for 'Proof Strategies in Linear Logic')
( tammet@cs.chalmers.se)