ProofTools: a symbolic logic proof tree generator

19 June 2020: ProofTools 0.6.2 fixes a bug and adds support for 64-bit macOS. This means ProofTools now works on Catalina.

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 aka semantic tableau 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 Qt5 version of ProofTools 0.6

Download

Version 0.6.2, released 19 June 2020

linux x86 32-bit, GTK2  linux x86 32-bit, Qt  linux x86 64-bit, GTK2  linux x86 64-bit, Qt5  win32  win64  macos 64-bit

New features:


Version 0.6.1, released 13 June 2019

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

New features:


Version 0.6, released 16 Feb 2019

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

New features:


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

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.

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.

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 prioritises other activities higher - mostly, publishing papers at the open-access journals that he founded. He can still be tempted, though, into offering advice, suggestions and feedback on ProofTools.