

Science Math Logic and Foundations Software Science Math Logic and Foundations Software sites Software.LogicandFoundations.Math.sciencenter.work 

Science Math Logic and Foundations Software Science Math Logic and Foundations Software sites Software.LogicandFoundations.Math.sciencesites.work 

ACL2 Version 2. 7 A programming language in which you can model computer systems and a tool to help prove properties of those models. Available under GPL and runs on various platforms. Includes related download links. www.cs.utexas.edu/users/moore/acl2/ 

Bertrand Bertrand solves sets of firstorder predicate logic statements for satisfiability (consistency) , validity , and equivalence. It also checks single statements for "logical truth" (tautology) and "logical falsity" (selfcontradiction). Subjectidentity is www.uwosh.edu/faculty_staff/herzberg/Bertrand.html 

Church Program understands the different types of lambda expressions , can extract lists of variables (both free and bound) and subterms , and can simplify complicated expressions. Uses Python. www.alcyone.com/software/church/ 

DC Proof Online New proofwriting software to teach the fundamentals of logic and proof. Enables users/students to write errorfree proofs by selecting rules of inference , axioms , etc. from convenient dropdown menus. Includes tutorial and exercises. www.dcproof.com/ 

Gateway to Logic A collection of webbased logic programs offering a number of logical functions: interactively or automatically build proofs , check theorems , and operate on propositional logic formulae. logik.phl.univie.ac.at/~chris/formularuk.html 

Isabelle A generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). Includes logic , documentation and free download. www.cl.cam.ac.uk/Research/HVG/Isabelle/ 

j'Imp Theorem Prover An automatic theorem prover based on set of support and ordered resolution for firstorder logic. j'Imp is part of the Orbital library. This library is a Java class providing objectoriented representations and algorithms for logic , mathematics , and art www.functologic.com/logic/jImp.html 

llprover A linear logic prover that searches a cutfree proof for the given twosided sequent of firstorder linear logic. bach.scitec.kobeu.ac.jp/llprover/ 

LOOM A language and environment for constructing intelligent applications. It is a research project in the Artificial Intelligence research group at the University of Southern California's Information Sciences Institute. The goal of the project is to develop www.isi.edu/isd/LOOM/LOOMHOME.html 

LWB Logics Workbench. www.lwb.unibe.ch/ 

MUltlog Takes as input the specification of a finitelyvalued firstorder logic and produces a sequent calculus , a natural deduction system , and clause formation rules for this logic. www.logic.at/multlog/ 

MUltseq A generic sequent prover for propositional finitelyvalued logics. www.logic.at/multseq/ 

Proof General Comprehensive GnuEmacs and XEmacs interface for several theorem provers including Coq , Isabelle , Lego , and Phox. proofgeneral.inf.ed.ac.uk/ 

ProofPower A suite of tools supporting specification and proof in Higher Order Logic (HOL) and in Z notation. www.lemmaone.com/ProofPower/index/ 

PVS The PVS Specification and Verification System. Available for Sparc machines with Solaris 2 and Intel x86 Machines with Linux compatible with Redhat 5 or later. Required is Emacs (version 19 or later) , recommended LaTeX and Tcl/Tk. Download by FTP. pvs.csl.sri.com/ 
