Tools

The following automated reasoning tools are available for download.

ACL2: a computational logic
http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html

AF2: a type system based on second order intuitionistic logic http://www.logique.jussieu.fr/www.raffalli/af2.html

Alloy Analyzer: software design tool
http://alloy.mit.edu/

BCSat: satisfiability checker for Boolean circuits
http://www.tcs.hut.fi/~tjunttil/bcsat/index.html

BerkMin: satisfiability solver
http://eigold.tripod.com/BerkMin.html

Chaff: satisfiability solver
http://www.ee.princeton.edu/~chaff/software.php

CHOL: a user-interface for HOL
http://www.inria.fr/croap/chol/chol.html

CLAM: a proof planner
http://dream.dai.ed.ac.uk/software/clam/index.html

CtCoq: a proof assistant
http://www.inria.fr/croap/ctcoq/ctcoq-eng.html

CWEB: concurrency workbenck for reasoning about concurrent systems http://www.dcs.ed.ac.uk/packages/cwb/

Coq: a proof assistant
http://zenon.inria.fr:8003/Equipes/COQ-eng.html

DCTP: disconnection calculus theorem prover
http://www4.informatik.tu-muenchen.de/~letz/dctp.html

Deep Thought: tableau prover
http://kirmes.inferenzsysteme.informatik.th-darmstadt.de/~stefan/dt.html

E: equality theorem prover
http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html

ELAN: rewrite engine
http://www.loria.fr/equipes/protheo/SOFTWARES/ELAN/

ELF: proof system
http://www.cs.cmu.edu/~fp/elf.html

EQP: equational theorem prover
http://www-unix.mcs.anl.gov/AR/eqp/

E-SETHEO: equality theorem prover
http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-setheo.html

EVES: theorem prover
http://www.ora.on.ca/eves.html

FDPLL: first order DPLL theorem prover
http://www.uni-koblenz.de/~peter/FDPLL/ft: theorem prover http://www.sics.se/ps/ft.html

Gandalf: theorem prover
http://www.cs.chalmers.se/~tammet/gandalf/

GRASP: satisfiability solver
http://sat.inesc-id.pt/~jpms/grasp/

GSAT: satisfiability solver
http://www.cs.washington.edu/homes/kautz/walksat/

HOL: Higher Order Logic
http://www.cl.cam.ac.uk/Research/HVG/HOL/

HOL Light: small clean HOL
http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html

IMPS: Interactive Mathematical Proof System
http://imps.mcmaster.ca/

INKA: inductive theorem prover
http://www.dfki.de/vse/systems/inka/

Isabelle: a generic theorem proving environment
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/

Jape: proof editor tool
http://users.comlab.ox.ac.uk/bernard.sufrin/jape.html

kcnf: satisfiability solver
http://www.laria.u-picardie.fr/~dequen/sat/

KIV: interactive prover
http://i11www.ira.uka.de/~kiv/KIV-KA.html#WHAT

Lambda CLAM: a higher order proof planner
http://dream.dai.ed.ac.uk/software/lambda-clam/

Larch: theorem prover
http://nms.lcs.mit.edu/Larch/

LDPP: satisfiability prover
http://www.ai.sri.com/~stickel/ldpp.html

LeanTAP: lean tableau theorem prover
http://i12www.ira.uka.de/leantap/

Limmat: satisfiability solver
http://www.inf.ethz.ch/personal/biere/projects/limmat/

MACE: model finder
http://www-unix.mcs.anl.gov/AR/mace/

MathWeb: web tool
http://www.mathweb.org/mathweb/

MBase: a mathematical knowledge base
http://www.mathweb.org/mbase/

METEOR: model elimination prover
http://www.cs.duke.edu/~ola/meteor.html

Mizar: mathematical proof system
http://web.cs.ualberta.ca:80/~piotr/Mizar/

Nqthm: the Boyer-Moore prover
http://www.cs.utexas.edu/users/boyer/ftp/nqthm/

NTAB: satisfiability solver
http://www.cirl.uoregon.edu/crawford/

Nuprl: a proof & program refinment logic
http://www.cs.cornell.edu/Info/Projects/NuPrl/

NuSMV: new symbolic model checker
http://sra.itc.it/tool.epl?name=NuSMV

OBJ3: equatioanl rewrite engine
http://www.kindsoftware.com/products/opensource/OBJ3/

OKsolver: satisfiability solver
http://cs-svr1.swan.ac.uk/~csoliver/OKsolver.html

Omega system: theorem prover
http://www.ags.uni-sb.de/~omega/

OSHL: theorem prover
http://www.cs.unc.edu/~zhu/prover.html

Otter: theorem prover
http://www-unix.mcs.anl.gov/AR/otter/

Porgi: intuitionistic theorem prover
http://www.cis.ksu.edu/~allen/porgi.html

PTTP: prolog technology theorem prover
http://www.ai.sri.com/~stickel/pttp.html

PVS: Prototype Verification System
http://pvs.csl.sri.com/

RRL: rewrite rule engine
http://www.cs.uiowa.edu/~hzhang/induc.html

SATO: satisfiability solver
http://www.cs.uiowa.edu/~hzhang/sato.html

SATURATE: theorem prover
http://www.mpi-sb.mpg.de/SATURATE/

satz: satisfiability solver
http://www.laria.u-picardie.fr/~Ecli/EnglishPage.html

Satzoo: satisfiability solver
http://www.cs.chalmers.se/~een/Satzoo/

SCOTT: theorem prover
http://arp.anu.edu.au/~jks/scott.html

SEM: finite model generation program
http://www.cs.uiowa.edu/~hzhang/sem.html

SEMPROP: decision procedure for quantified Boolean formulae
http://www4.informatik.tu-muenchen.de/~letz/semprop/

SETHEO: theorem prover
http://www4.informatik.tu-muenchen.de/~letz/setheo/

SNARK: SRI's New Automated Reasoning Kit (theorem prover) http://www.ai.sri.com/~stickel/snark.html

SPASS: theorem prover
http://spass.mpi-sb.mpg.de/

SpecWare: formal software development system
http://www.specware.org/

SPIN: model checker
http://spinroot.com/spin/whatispin.html

STAR: software tools for automated reasoning
http://www.mrg.dist.unige.it/star/

STeP: Stanford Temporal Prover
http://www-step.stanford.edu/

3TAP: theorem prover
http://i12www.ira.uka.de/~threetap/

Theorema: theorem prover and computer algebra system
http://www.theorema.org/

TPS: higher order theorem prover
http://gtps.math.cmu.edu/andrews.html

Twelf: logical framework and prover
http://www-2.cs.cmu.edu/~twelf/

UnitWalk: satisfiability solver
http://logic.pdmi.ras.ru/~arist/UnitWalk/

Vampire: theorem prover
http://www.prover.info/

Verifun: theorem prover for functional programs
http://www.inferenzsysteme.informatik.tu-darmstadt.de/verifun/

Walksat: satisfiability solver
http://www.cs.washington.edu/homes/kautz/walksat/

  Sponsored by: