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.
http://pvs.csl.sri.com/
By Jon Barwise and John Etchemendy.
http://www-csli.stanford.edu/hp/Logic-software.html
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 and field advanced tools for knowledge representation and reasoning in Artificial Intelligence.
http://www.isi.edu/isd/LOOM/LOOM-HOME.html
Web resource provided by research group. Includes access to software developed by the team, coverering such projects as FINDER (Finite Domain Enumerator), MaGIC (Matrix Generator for Implication Connectives) and Kripke (A theorem prover for the relevant logic LR).
http://cslab.anu.edu.au/ar/
Logics Workbench.
http://www.lwb.unibe.ch/
Comprehensive Gnu-Emacs and XEmacs interface for several theorem provers including Coq, Isabelle, Lego, and Phox.
http://proofgeneral.inf.ed.ac.uk
Application that draws truth-tables for propositional logic formulae. Available for free download and web use.
http://www.mintlogic.com/ludwig/
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.
http://www.cs.utexas.edu/users/moore/acl2/