An implementation of the semantic tableaux method for classical propositional and predicate logic, written in JavaScript/DOM.
http://www.umsu.de/logik/trees
a digital logic simulator written for the SCM Scheme implementation.
http://www-swiss.ai.mit.edu/~jaffer/SIMSYNCH.html
A generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). Includes logic, documentation and free download.
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
A PROver with a Theory Extension INterface. Theorem prover for first-order clause logic, written in ECRC's Prolog-dialect ECLiPSe. Free download, documentation.
http://www.uni-koblenz.de/ag-ki/Implementierungen/Protein/
Tool for minimizing boolean logic functions.
http://incolor.inetnebr.com/double/softlib/switchmin.html