Educational Logic Software

Please note that this list has no longer been actively maintained after 2009.


Akka , http://staff.science.uva.nl/~lhendrik/AkkaStart.html

  • functions : provability of formulas in several logics, validity of formulas in a model, drawing and editing Kripke models and models for dynamic logic
  • platforms : web
  • developer : Lex Hendriks, ILLC, University of Amsterdam, the Netherlands
  • email : A [dot] Hendriks [at] uva [dot] nl
  • book : no
  • comments :

Alfie , http://www.cs.chalmers.se/~sydow/alfie/index.html

  • functions : natural deduction for propositional logic
  • platforms : web
  • developers : Björn von Sydow, Department of Computing Science, Chalmers University, Göteborg, Sweden
  • email : sydow [at] cs [dot] chalmers [dot] se
  • book : no
  • comments : ascii interface

AProS , http://www.phil.cmu.edu/projects/apros/

  • functions : natural deduction for propositional and predicate logic (including adaptations to intuitionistic and minimal logic), interactive proof construction
  • platforms : anything enabling Java
  • developers : Wilfried Sieg and collaborators, Carnegie Mellon University, USA
  • email : sieg [at] cmu [dot] edu
  • book : no
  • comments : formerly known as 'Carnegie Mellon Proof Tutor' (at that time involving Richard Scheines); website includes an online course in logic.

Aristotle , http://www.utexas.edu/courses/plato/aristotle.html

  • functions : formalizing English sentences into symbolic logic
  • platforms : Windows95/98/NT
  • developers :
  • email : marcow [at] cs [dot] utexas [dot] edu
  • book :
  • comments :

Athena Software , http://www.athenasoft.org/

  • functions : hierarchically structuring arguments and their support, in a graphical interface using a tree format; similar tools for negotation
  • platforms : Windows
  • developers : Bertil Rolf, Blekinge Institute of Technology, Sweden, and others
  • email : info [at] athenasoft [dot] org , bertil [dot] rolf [at] bth [dot] se
  • book : various online documentation, powerpoint, etc.
  • comments : also for use on highschools, teacher support, added to list in 2003

Bertie3 , http://selfpace.uconn.edu/BertieTwootie/software.htm

  • functions : natural deduction in propositional and predicate logic
  • platforms : Windows
  • developer : Austen Clark, University of Connecticut USA
  • email : austen [dot] clark [at] uconn [dot] edu
  • book : Merrie Bergmann, Jim Moor, and Jack Nelson, The Logic Book , 2nd edition. McGrawHill 1992.
  • comments : available as GNU Public Domain License software

Bertrand , http://www.uwosh.edu/faculty_staff/herzberg/Bertrand.html

  • functions : tableau-like validity testing of predicate logic formulas
  • platforms : Apple
  • developers : Larry A. Herzberg, University of Wisconsin - Oshkosh, USA
  • email : herzberg [at] uwosh [dot] edu
  • book : no
  • comments :

blobLogic , http://corinhowitt.com/blob/blobSplash.html

  • functions : semantic tableaux for propositional and predicate logics
  • platforms : web (requires downloading 'Shockwave'), Mac, Windows
  • developers : Corin Howitt, Oxford University, UK
  • email : corin [dot] howitt [at] philosophy [dot] ox [dot] ac [dot] uk
  • book : no (particularly suitable for use with either Jeffrey or Hodges)
  • comments : online proof demonstrations; save/load to web servers; interactive tutorials; modal logic version to be released later; added to list in 2003

blogic , http://www.nyu.edu/classes/velleman/blogic/Logic/

  • functions : Boolean search, logic circuits, truth-tables, semantics of modal logic with possible-worlds diagrams, quantification.
  • platforms : web
  • developers : David Velleman, New York University, USA
  • email : jdvelleman [at] nyu [dot] edu
  • book : this is an interactive textbook
  • comments :

Boole , http://www-csli.stanford.edu/LPL/

  • functions : truth tables
  • platforms : Windows, Mac OSX and Classic MacOS
  • developers : John Etchemendy, Stanford University, USA, Jon Barwise, Indiana University USA
  • email : Dave Barker-Plummer, dbp-at-csli-dot-stanford-dot-edu , or User Support, LPLbugs-at-csli-dot-stanford-dot-edu
  • book : John Etchemendy & Jon Barwise, Language, Proof and Logic . CSLI Publications, 2000.
  • comments : The book comes with the software: Fitch, Boole, and Tarski's World.

BOP a Propositional Proof Generator , http://dutiih.twi.tudelft.nl/~sicco/

  • functions : truthtables and natural deduction for propositional logic
  • platforms : web
  • developers : Jonne Zutt and Joost Broekens, Delft University, the Netherlands
  • email : j [dot] zutt [at] ewi [dot] tudelft [dot] nl or Hans Tonino: J [dot] F [dot] M [dot] Tonino [at] ewi [dot] tudelft [dot] nl
  • book : no
  • comments :

Computational Aristotelian Term Logic , http://logic.glashoff.net/aristotelianlogic/

  • functions : Aristotelian (syllogistic) logic
  • platforms : web
  • developers : Klaus Glashoff, Germany
  • email : logic [at] glashoff [dot] net ,
  • book : no
  • comments :

DC Proof , http://www.dcproof.com/

  • functions : natural deduction, formal arguments
  • platforms : Windows
  • developers : Dan Christensen
  • email : dc [at] dcproof [dot] com
  • book : no
  • comments :

Deriver , http://softoption.us

  • functions : natural deduction for propositional and predicate logic, interactive proof construction, tableaux, elementary semantics, symbolization, modal logic
  • platforms : Java applet (for web pages) or Java web start application
  • developers : Martin Fricke
  • email : mfricke [at] softoption [dot] us
  • book : no
  • comments : a remarkable collection of diverse online tutorials with accompanying applets, and adjusted to various standard notations and (philosophical) logics

Expression Evaluator , http://www.cc.utah.edu/~nahaj/logic/evaluate/

  • functions : semantic (interpreted) evaluation of propositional and predicate logic formulas
  • platforms : web
  • developers : John Halleck, University of Utah, USA
  • email : John [dot] Halleck [at] utah [dot] edu
  • book : no
  • comments : links to other web resources (modal logics)

Fitch , http://www-csli.stanford.edu/LPL/

  • functions : natural deduction for predicate logic
  • platforms : Windows, Mac OSX and Classic MacOS
  • developers : John Etchemendy, Stanford University USA, Jon Barwise, Indiana University USA
  • email : Dave Barker-Plummer, dbp-at-csli-dot-stanford-dot-edu , or User Support, LPLbugs-at-csli-dot-stanford-dot-edu
  • book : John Etchemendy & Jon Barwise, Language, Proof and Logic . CSLI Publications, 2000.
  • comments : The book comes with the software: Fitch, Boole, and Tarski's World.

Gateway to logic , http://logik.phl.univie.ac.at/~chris/formular-uk.html

  • functions : natural deduction for predicate logic (Lemmon- and Fitch-style), truth tables, ...
  • platforms : web
  • developers : Christian Gottschall (University of Vienna, Austria)
  • email : gottschall [at] gmx [dot] de
  • book : no
  • comments : both in English and German

Hexagon , http://www.science.uva.nl/projects/opencollege/cognitie/hexagon/

  • functions : public updates in epistemic logic
  • platforms : web
  • developers : Jan Jaspars, Free-lance logician & University of Amsterdam, the Netherlands
  • email : jaspars [at] science [dot] uva [dot] nl
  • book : no
  • comments : in Dutch (courseware additional to University of Amsterdam lectures)

Hyperproof , http://ggww2.stanford.edu/GUS/openproof/

  • functions : natural deduction for predicate logic, visual reasoning
  • platforms : Apple
  • developers : John Etchemendy, Stanford University USA, Jon Barwise, Indiana University USA
  • email: dbp-at-csli-dot-stanford-dot-edu (Dave Barker-Plummer)
  • book : Hyperproof , John Etchemendy and Jon Barwise, CSLI publications, 1994
  • comments : Hyperproof is currently out of print

Inference Engine , http://blue.butler.edu/~sglennan/InferenceEngine.html

  • functions :
  • platforms : Mac, Windows
  • developers : Stuart Glennan
  • email : sglennan [at] butler [dot] edu
  • book : Joseph Bessie and Stuart Glennan, Elements of Deductive Inference , Wadsworth 2000
  • comments :

Interactive Logic Programs , http://www.thoralf.uwaterloo.ca/htdocs/LOGIC/st_ilp.html

  • functions : truthtables in propositional logic, unification of terms
  • platforms : web
  • developers : Stanley N. Burris, University of Waterloo, Canada
  • email : snburris [at] thoralf [dot] uwaterloo [dot] ca
  • book : Logic for Mathematics and Computer Science , Prentice Hall 1998.
  • comments : added to list in 2003

Jape , http://www.jape.org.uk/

  • functions : natural deduction and sequent proof in classical predicate logic; plus various other logics and formal systems; plus user-defined logics
  • platforms : MacOSX, Windows, Linux, Solaris
  • developers : Bernard Sufrin, Oxford University UK & Richard Bornat, QMW London UK
  • email : Bernard [dot] Sufrin [at] comlab [dot] ox [dot] ac [dot] uk , richard [at] dcs [dot] qmw [dot] ac [dot] uk
  • book : coming
  • comments : Jape is acronym for 'just another proof editor'

LICS web tutor , http://www.cs.bham.ac.uk/research/lics/

  • functions : MC questions and answers about various logical topics, including modal
  • platforms : web
  • developers : Michael Huth and Marc Ryan, School of Computer Science, University of Birmingham, UK
  • email : M [dot] Huth [at] doc [dot] ic [dot] ac [dot] uk , M [dot] D [dot] Ryan [at] cs [dot] bham [dot] ac [dot] uk
  • book : Logic in Computer Science , Cambridge University Press, 2000.
  • comments :

Logic Animations , http://staff.science.uva.nl/~jaspars/animations/

  • functions : semantic computations in propositional, predicate, dynamic, modal logic
  • platforms : web
  • developers : Jan Jaspars, Free-lance logician & University of Amsterdam, the Netherlands
  • email : jaspars [at] science [dot] uva [dot] nl
  • book : no
  • comments : mainly in Dutch

Logic Cafe , http://www.oakland.edu/phil/cafe/

  • functions : truthtables, predicate logic arguments, MC questions
  • platforms : web (Linux, Mac public domain versions)
  • developers : John Halpin, Oakland University
  • email : halpin [at] oakland [dot] edu
  • book : online
  • comments : online logic textbook with integrated web-based exercises, public domain

Logic Daemon , http://logic.tamu.edu/

  • functions : natural deduction for predicate logic, truth tables for propositional logic, countermodels for predicate logic.
  • platforms : web
  • developers : Colin Allen, http://mypage.iu.edu/~colallen/ and Chris Menzel, Texas A&M University, http://philebus.tamu.edu/cmenzel/
  • email : colallen%40indiana%2eedu
  • book : Colin Allen and Michael Hand, Logic Primer (2nd ed.). MIT Press 2001.
  • comments : ascii interface; integrated, context sensitive help system; with multiple choice exercises

 

Logic for Fun , http://logic4fun.rsise.anu.edu.au/

  • functions : expressing puzzles and other problems in first order logic
  • platforms : web
  • developer : John Slaney, Australian National University
  • email : John [dot] Slaney [at] anu [dot] edu [dot] au
  • book : no
  • comments :

Logic Toolbox , http://philosophy.lander.edu/~jsaetti/Welcome.html

  • functions : syllogisms, truthtables, natural deduction for propositional logic
  • platforms : web, windows
  • developers : John Saetti
  • email : john [dot] saetti [at] gcccd [dot] net
  • book : no
  • comments :

LogicCoach III , http://academic.csuohio.edu/polen/

  • functions : truthtables, syllogisms, proofs, informal logic, ...
  • platforms : Windows, Apple
  • developers : Nelson Pole, Cleveland State University, Ohio, USA
  • email : n [dot] pole [at] csuohio [dot] edu
  • book : Patrick Hurley, A Concise Introduction to Logic , 8th edition, Wadsworth 2003.
    Howard Kahane & Paul Tidman, Logic and Philosophy : A Modern Introduction , 9th edition, Wadsworth 2003. Dale Jacquette, Symbolic Logic , Wadsworth 2001.
  • comments : instructor's package available; (updated 2003)

Logics Workbench , http://www.lwb.unibe.ch/

  • functions : proof and computation in propositional logics (minimal, intuitionist, classical, modal, nonmonotonic, ...)
  • platforms : web, Apple, Linux, Solaris
  • developers : Gerhard Jäger (project leader), Peter Balsiger, Alain Heuerding, Stefan Schwendimann, University of Bern, Switzerland
  • email : lwb [at] iam [dot] unibe [dot] ch
  • book : extensive online manual
  • comments : no proof editing

MacLogic , http://www-theory.dcs.st-and.ac.uk/~rd/logic/

  • functions : predicate logic (minimal, intuitionistic, classical), natural deduction and sequent calculus
  • platforms : Apple
  • developers : Roy Dyckhoff, St Andrews University, Scotland UK
  • email : rd [at] dcs [dot] st-andrews [dot] ac [dot] uk
  • book : optional: G. Forbes, Modern Logic , Oxford University Press, 1993
  • comments : MacLogic is no longer updated to current versions of MacOS; however, to run MacLogic under emulation on Apple OSX and other than Apple platforms, see http://fitelson.org/maclogic.htm

New Pandora , http://www.doc.ic.ac.uk/pandora/

  • functions : natural deduction for predicate logic
  • platforms : web
  • developers : Krysia Broda and others, Department of Computing, Imperial College, London, UK
  • email : kb [at] doc [dot] ic [dot] ac [dot] uk
  • book : S. Eisenbach et al, Reasoned Programming , Prentice Hall, 1994.
    See also Ian Hodkinson's coursenotes
  • comments : based on earlier version called 'Pandora'

Organon , http://home.zcu.cz/~ldostal/organon/index_aj.htm

  • functions : propositional logic, predicate logic, syllogistic reasoning support
  • platforms : web; designed for the Internet Explorer
  • developers : Ludmila Dostalova and Jaroslav Lang, University of West Bohemia in Pilsen, Czech Republic
  • email : ldostal [at] kfi [dot] zcu [dot] cz
  • book : no
  • comments : pilot version with a limited number of functions and a raw user interface; in czech language.

Pier , http://gentzen.math.hc.keio.ac.jp/Pier/Pier.html

  • functions : interactive proof editor, natural deduction
  • platforms : web
  • developers : Masaru Shirahata, Keio University, Japan
  • email : sirahata [at] math [dot] hc [dot] keio [dot] ac [dot] jp
  • book :
  • comments : see also: Virtual Math homepage

Plato , http://www.utexas.edu/courses/plato/

  • functions : proofs in propositional and predicate calculus
  • platforms : Windows, Mac
  • developers :
  • email : marcow [at] cs [dot] utexas [dot] edu , Robert C. Koons: rkoons [at] mail [dot] utexas [dot] edu
  • book : Robert C. Koons, A Logical Toolbox, 2000.
  • comments :

Power of Logic , http://www.poweroflogic.com/

Program to learn Natural Deduction in Gentzen-Kleene's style , http://patrice.bailhache.free.fr/dnfn/deductioneng.html

  • functions : sequent-style natural deduction for predicate logic, computation of normal forms
  • platforms : Windows
  • developers : Patrice Bailhache, University of Nantes, France
  • email : not known
  • book : no
  • comments : used by Nantes (France) philosophy students

ProofBuilder , http://www.cis.gvsu.edu/~mcguire/ProofBuilder/

  • functions : natural deduction, resolution, equational reasoning, etc.
  • platforms : anything enabling Java (Windows, LINUX, Apple, UNIX, ...)
  • developers : Hugh McGuire, Grand Valley State University, Michigan, USA
  • email : mcguire [at] cis [dot] gvsu [dot] edu
  • book : no
  • comments : ProofBuilder adapts to the notation that you use, and you can copy/paste from HTML, PDF, MS Word, etc.

ProofWeb , http://proofweb.cs.ru.nl/login.php

  • functions : natural deduction for propositional and predicate logic
  • platforms : web
  • developers : main developer of the system was Cezary Kaliszyk, after ideas by Freek Wiedijk
  • email : proofweb [at] cs [dot] ru [dot] nl
  • book : Huth & Ryan, Logic in Computer Science, CUP
  • comments : almost, but not quite, entirely unlike the Jape system

Reason!Able , http://www.goreason.com

  • functions : visually representing arguments
  • platforms : Windows 95 and up
  • developers : Tim van Gelder, University of Melbourne, Australia
  • email : info [at] goreason [dot] com
  • book : no
  • comments : teachers' resources

Socrates , http://www.utexas.edu/courses/socrates/

  • functions : semantic tableaux
  • platforms : Windows
  • developers :
  • email : marcow [at] cs [dot] utexas [dot] edu , Robert C. Koons: rkoons [at] mail [dot] utexas [dot] edu
  • book : Robert C. Koons, A Logical Toolbox, 2000.
  • comments :

Tableau III , http://logic.philosophy.ox.ac.uk/

  • functions : semantic tableaux for predicate logic
  • platforms : web, Windows
  • developers : (Tableau II) Luciano Floridi, University of Oxford, UK; (Tableau III) Nik Roberts
  • email : logic [at] philosophy [dot] ox [dot] ac [dot] uk
  • book : site contains online tutorials. The material is compatible with: W. Hodges, Logic, 2nd edition (Penguin, 2001).
  • comments : Tableau III is the successor to Tableau II, originally developed in 1988.

Tarski's World , http://ggww2.stanford.edu/GUS/openproof/

  • functions : interpreted semantics of predicate logic
  • platforms : Windows, Apple
  • developers : John Etchemendy, Stanford University USA, Jon Barwise, Indiana University USA
  • email : dbp-at-csli-dot-stanford-dot-edu (Dave Barker-Plummer)
  • book : The Language of First-order Logic (3rd edition), John Etchemendy and Jon Barwise, CSLI publications, 1994 (Also: Tarski "Lite", same authors; also: Language, Proof and Logic, same authors)
  • comments : includes the Hintikka game (semantic tableaux)

TPS and ETPS , http://gtps.math.cmu.edu/tps.html

  • functions : interactive proof of theorems of first-order logic or higher-order logic (type theory)
  • platforms : Unix, Windows, web
  • developers : Peter B. Andrews, Carnegie Mellon University; and others
  • email : andrews [at] cmu [dot] edu
  • book : Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic Publishers, 2002
  • comments : see also "ETPS: A System to Help Students Write Formal Proofs" at http://gtps.math.cmu.edu/tps-papers.html ; added to list in 2003

Tree Proof Generator , http://www.umsu.de/logik/trees/

  • functions : semantic tableaux generator for propositional and predicate logic
  • platforms : web
  • developers : Wolfgang Schwarz
  • email : wo [at] umsu [dot] de
  • book : no
  • comments : no interactive proof construction

Twootie , http://selfpace.uconn.edu/BertieTwootie/software.htm

  • functions : computing truth (trees) in propositional and predicate logic
  • platforms : Dos, Windows
  • developer : Austen Clark, University of Connecticut USA
  • email : austen [dot] clark [at] uconn [dot] edu
  • books : Merrie Bergmann, Jim Moor, and Jack Nelson, The Logic Book , 2nd edition. McGrawHill 1992.
    Richard Jeffrey, Formal Logic: Its Scope and Limits , 3rd edition. McGraw-Hill 1991.
  • comments : available as GNU Public Domain License software