Lambda a program for solving lambda definability problems of order at most two The Lego literature Logic Software for Macintosh Logic Software. Still a useful bibliography, though now slightly outdated, compiled by E. J. Forbis. Logic tutor (info in Dutch), Vrije Universiteit Amsterdam NL. For more information write to Hans Groen Logical Frameworks LogicCoach , for information write to Nelson Pole. Cleveland State University OH, USA. LogicCoach is also available with Patrick Hurley's A Concise Introduction to Logic , published by Wadsworth. Site which uses the LogicCoach. Logics Workbench , Bern CH LogicWorks , Stetson University USA, Rob R. Brady; publisher is the Philosophy Documentation Center , for order information Pat Swope. Version n. 7.0 is avvailabel for both PC and Mac, both as "Instructor" and as a "Student". MacLogic , St Andrews Scotland UK, for an evaluation copy write to Roy Dyckhoff Merit Archive at U. Michigan (gopher service) Midway at U. Chicago (ftp service) Natural Deduction Categorial Grammar and Lambda-Calculus Parser ftp://ftp.cs.cmu.edu/afs/andrew/usr13/bc10/ftp/nat_ded_cg_parser.tar.Z (184k) Natural Language Software Registry is a concise summary of the capabiliti es and sources of language processing software available to researchers. It comprises academic, commercial, and proprietary software, with theory, specifications, and terms on which it can be acquired clearly indicated. The second edition contains about one hundred software descriptions. Deutsches Forschungszentrum fuer Kuenstliche Intelligenz (DFKI), Saarbruecken, Germany Perseus Porgi - Proof-Or-Refutation Generator for Intuitionistic propositional logic Prisoner's Dilemma. Exercises in applied rationality: "a fiendish cyberspace wizard has locked you and Serendip into a diabolical game with the following rules...". Program to learn Natural Deduction in Gentzen-Kleene's style , Patrice Bailhache, Nantes University. Prolog Resource Guide Saetti's Sentential Proof Checkers SCOTT (Semantically Constrained Otter) FINDER (Finite Domain Enumerator), MaGIC (Matrix Generator for Implication Connectives), BWSTATES (Generate States of Blocks World), MINLOG (A Theorem Prover for Minimal and Intuitionistic Logic), KRIPKE (A Theorem Prover for the Relevant Logic LR). Software for proofs of mathematical theorems Isabelle | HOL | Coq Tableau Logic Teaching Software. To be used with W. Hodges' textbook (also translated into Italian by Laterza). Tableau-based Theorem Prover Bernhard Beckert, Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme Tableau-based Theorem Prover Version 3. 0. 3TAP is a many-valued tableau-based theorem prover developed at the University of Karlsruhe. It can be instantiated for arbitrary finitely-valued first-order logics, and it can handle equality (two-valued), sorts, and non-clausal input.You can retrieve the complete 3TAP source code and a lot of information on 3TAP (including a 190 page handbook) from http://i12www.ira.uka.de/~threetap/ see also http://i12www.ira.uka.de/~beckert/ Tanel Tammet (Computing Science Department of the University of Göteborg and the Chalmers University of Technology) provides the following tools (free ftp-able software, all the sources are gzipped. Automated theorem provers for linear logic): C source of a tableau theorem prover and a resolution theorem prover for full propositional linear logic. Manual for the prover. The paper 'Proof Strategies in Linear Logic' mentioned above. Tarski's World , CSLI Stanford USA The HOL Theorem Proving System The Language of First-order Logic, The LEGO Proof Assistant Truth Tables Maker (ttm120.arc) Truth Tables Software (truth.zip) Venn Diagram Program (venn.zip) Web page drawing type assignment figures (by Sachio Hirokawa) World Wide Web Virtual Library on Formal Methods, by Jonathan Bowen of Oxford University. Mechanized Reasoning Home Page , Stanford CSLI, USA Courseware, though not software: David Gries' pages on teaching logic as a tool