A generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). Includes logic, documentation and free download.

A PROver with a Theory Extension INterface. Theorem prover for first-order clause logic, written in ECRC's Prolog-dialect ECLiPSe. Free download, documentation.

A linear logic prover that searches a cut-free proof for the given two-sided sequent of first-order linear logic.

An implementation of the semantic tableaux method for classical propositional and predicate logic, written in JavaScript/DOM.

Takes as input the specification of a finitely-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic.

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.

Logics Workbench.

A graphical IDE for creating, running and debugging Turing machines. Freeware for Windows 95/98/NT/2000.

New proof-writing software to teach the fundamentals of logic and proof. Enables users/students to write error-free proofs by selecting rules of inference, axioms, etc. from convenient drop-down menus. Includes tutorial and exercises.

Comprehensive Gnu-Emacs and XEmacs interface for several theorem provers including Coq, Isabelle, Lego, and Phox.