ProofTools: a symbolic logic proof tree generator

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 GTK2 version of ProofTools 0.4.2 beta

Features in development

The following changes have already been made in the development code and will be made available when the next version is packaged and released:

Download

Version 0.4.2 beta, released 29 Apr 2014

Note the presence of the bugs described in the bug listing.

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.

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

Note that only bugs in the current version are listed. Bugs in previous versions can be identified by reading through the feature listings of later versions and noting "bugfix" entries.

Whilst we are not aware of any other bugs with the current release, we do have a question about the semantics of the Substitutivity of Identicals rule for modal tableaux, and I would be grateful if you can help us to answer this question.

Known limitations

Collaboration

Emil Kirkegaard instigated this project and collaborated with me on it for some time.