Interactive Logic Software
[Update, 8/28] It seems that Hans van Ditmarsch has thought about compiling such a list long ago; and a mighty list it is! Scroll down to find more interesting software, such as the Carnegie Mellon AProS, or the interactive logic course blogic, created by David Velleman, plus many-many others to try out online, or download and use on your computer. [/update]
Here are several useful web-based tools for teaching logic at the introductory level:
- The Logic Machine at TAMU
Probably the best known. Created by Collin Allen and Chris Menzel. It has a proof checker (for Lemmon-style natural deduction proofs), and countermodel, well-formed-formulas and equivalency checkers. Also has a useful quiz program. It was created for use with Allen and Hand’s Logic Primer, but is suitable for use with, e.g., E.J. Lemmon’s classic Beginning Logic.
- The Gateway to Logic
This is an impressive collection of logic software created by Christian Gottschall. First, there are various functions operating on formulae of propositional logic (like displaying syntax trees, Fregean notation variants, truth-tables, and normal forms), bundled in a server side pack (classical) and a client side pack (supporting various multi-valued propositional logics). Then, it has programs for building proofs, both axiomatic (Hilbert and Principia), natural deduction proofs (Fitch style, Lemmon style), and even in Peirce’s Alpha Graph calculus! And it’s not over: it also has a proof checker and an automated theorem prover (Lemmon-style ND).
- The Logics Workbench
Created by a group from the University of Bern, the LWB offers a bunch of functions (concerning provability, simplification of formulas, computation of normal forms, embeddings etc.) on quite a few propositional logics, including classical, intuitionistic, modal, temporal, linear, and non-monotoni logics! It may not be as simple to use as the others linked here, but it is really nice.
Is a nice program for studying (and learning) proofs in Aristotelian logic (both mediate and immediate inferences, and according to various modern interpretations, from Lukasiewicz to Corcoran and Smiley), by Klaus Glashoff.
- A Truth Table Practice tool
By the Mathematics Department at CalState San Bernardino. Useful for training on simple truth-tables problems, with formulas involving only two sentences.
- And a Logic Tutorial
Using exclusion diagrams to illustrate features of propositional logic, by Russell Johnston.
Have fun trying them out! 🙂