ProofTools: a symbolic logic proof tree generator

Update of 18 October 2014: a deficiency in infinite branch detection has come to my attention, the implication of which is that on rare occasions, ProofTools might give the wrong result.

Update of 24 October 2014: it's official, ProofTools's infinite branch detection definitively fails in certain cases.

ProofTools is a free, cross-platform software application for automatically and graphically generating semantic tableaux, also known as proof trees, semantic trees, analytic tableaux and, less commonly, truth trees, generally used to test whether a formula is a logical truth, or whether a proof/argument is deductively valid. ProofTools is still under development and lacks some features, however it is usable for many purposes. Currently, it can draw proof trees for propositional, predicate (including identity) and (basic/normal, constant domain, contingent-identity) modal logic, and it is available for Windows (both 32 and 64 bit), Macintosh OS X and Linux (both 32 and 64 bit).

ProofTools is documented in the ProofTools manual and in the ProofTools background and technical addendum page. A feature comparison of free proof tree software is also available so you can see what other free semantic tableaux software tools are around and whether any of them better suit your needs.

ProofTools is developed with Lazarus, a free, cross-platform, Delphi-like Object Pascal integrated development environment (IDE). The ProofTools source code is not currently publicly available but that might change for future versions.

ProofTools may be downloaded freely and used without limitation. It may also be shared and distributed freely unless money is charged for that distribution, in which case permission is required (this restriction was introduced in version 0.4 beta). Please link to this site for downloads rather than duplicating and hosting the downloadable files elsewhere - this makes it easier for us to keep track of how many people are downloading the program.

Please report any bugs that you find (after first checking that they haven't already been identified), including how to replicate them if known. Also please feel free to contact me about this software project or for any other good reason.

Screenshot

Screenshot of the Linux Qt version of ProofTools 0.5 beta

Download

Version 0.5 beta, released 9 Oct 2014

linux x86 32-bit, GTK2  linux x86 32-bit, Qt  linux x86 64-bit, GTK2  linux x86 64-bit, Qt  win32  win64  mac osx x86

New features:


Version 0.4.2 beta, released 29 Apr 2014

linux x86 32-bit, GTK2  linux x86 32-bit, Qt  linux x86 64-bit, GTK2  linux x86 64-bit, Qt[3]  win32  win64  mac osx x86

New features:


Version 0.4.1 beta, released 22 Jun 2013

Note: earlier I warned here that the implementation of (contingent) identity rule decomposition was under review and might still be buggy. Here I clarify that we no longer believe there might be a bug in the implementation, but we do have a question about the semantics of the Substitutivity of Identicals rule for modal tableaux. I would be grateful if you can help us to answer this question. [Update 15 October 2014: the question has now been answered, see the link for details]

For your peace of mind: Softpedia have certified the Windows and Mac builds of this release to be free from spyware, adware and viruses. All builds of all versions are, of course, equally clean.

Softpedia 100% Clean Award

linux x86 32-bit, GTK2  linux x86 32-bit, Qt  linux x86 64-bit, GTK2  linux x86 64-bit, Qt  win32  win64  mac osx x86

New features:


Version 0.4 beta, released 3 Jun 2013

linux x86 32-bit, GTK2  linux x86 32-bit, Qt  linux x86 64-bit, GTK2  linux x86 64-bit, Qt  win32  win64  mac osx x86

New features:


Version 0.3.2 beta, released 14 Dec 2012

mac osx x86

New features:


Version 0.3.1 beta, released 16 Nov 2012

linux x86 32-bit, GTK2  linux x86 32-bit, Qt [2]  linux x86 64-bit, GTK2  linux x86 64-bit, Qt [2]  win32  win64

New features:


Version 0.3 beta, released 12 May 2012

linux x86 32-bit, GTK2  linux x86 32-bit, Qt[2]  linux x86 64-bit, GTK2  linux x86 64-bit, Qt[1]  win32  win64

New features:


Version 0.2.2 beta, released 19 October 2011

linux x86 32-bit, GTK2  linux x86 64-bit, GTK2  win32  win64

New features:


Version 0.2.1 beta, released 30 October 2010

linux x86 32-bit, GTK2  linux x86 64-bit, GTK2  win32  win64

New features:


Version 0.2 beta, released 25 October 2010

linux x86 32-bit, GTK2  win32  win64

New features:


Version 0.1 beta, released 27 September 2010

linux x86 32-bit, GTK2  win32  win64


Footnotes


Known bugs

The following bugs are known to exist in the current version. Bugs in previous versions can be identified by reading through the feature listings of later versions and noting "bugfix" entries.

Note that our question about the semantics of the Substitutivity of Identicals rule for modal tableaux, for which we had previously been soliciting answers here and above, has now been answered.

Known limitations

Collaboration

Emil Kirkegaard instigated this project and collaborated with me very closely on it for some time. ProofTools is indebted to him for his passion for logic. He is primarily responsible for the design of the application, and for clearly explaining to the programmer (me) through word-processing documents those proof tree rules which were implemented prior to my purchase of the text on which we based ProofTools. These days, he has higher priorities - mostly, publishing papers at the open access, free to publish, open peer review scientific journals that he founded, Open Differential Psychology and Open Behavioral Genetics - but he can still be tempted into offering advice, suggestions and feedback on ProofTools.