Free Microsoft Excel add-in for processing and evaluating logic in your spreadhseet.

j'Imp is an automatic theorem prover based on set of support and ordered resolution for first-order logic. j'Imp is part of the the Orbital library. This library is a Java class providing object-oriented representations and algorithms for logic, mathematics, and artificial intelligence.

Bertrand solves sets of first-order predicate logic statements for satisfiability (consistency), validity, and equivalence. It also checks single statements for "logical truth" (tautology) and "logical falsity" (self-contradiction). Subject-identity is supported. User can "step through" the solution algorithm as Bertrand solves a problem, and/or check the graphic tree produced.

CrocoPat manipulates relations of any arity, including graphs (which are binary relations). Its simple and expressive query and manipulation language is based on first-order predicate calculus. The implementation is based on the data structure binary decision diagram (BDD).

Lean Tableau-based Deduction for Propositional Modal Logics. By Bernhard Beckert.

An interactive proof assistant based on analytic tableaux, and designed for the teaching of deductive reasoning. Ordering information is available at this site, as are academic papers on the design of the software.

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.

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

Application that draws truth-tables for propositional logic formulae. Available for free download and web use.

A semi-automated system for the verification of statements about programs written in a functional programming language. The system is capable of following fully-automated routines for theorem proving and hypotheses formation, as well as operating interactively when these reoutines fail.