ProofTools

ProofTools is a free, cross-platform software application for automatically and graphically generating semantic tableaux, also known as proof trees, semantic trees and analytic tableaux, generally used to test whether a formula is a logical truth, or whether a proof/argument is deductively valid. As a proof tree program, ProofTools is still under development and lacks some features, however it is usable for many purposes. Currently, it can validate a propositional, a predicate and a (normal) modal logic argument or logical truth using the method of proof tree.

ProofTools is documented in the ProofTools manual and in the ProofTools background and technical addendum page.

The ProofTools program 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.

Other ways to describe ProofTools

(I include these descriptions mostly for the benefit of those searching on the included phrases using online search engines).

In terms of its ability to validate arguments and verify logical truths, ProofTools can be described as a proof tree solver, a proof tree prover, a logical argument prover, a logic proof generator, a propositional, predicate and modal logic proof generator, a propositional logic solver, and a logical argument validator. In terms of its automation, ProofTools might be described as an automated proof constructor, an automated proof generator, an automated constructor of semantic tableaux, and an automated generator of analytic tableaux. ProofTools can also be described in terms of its ability to draw proof trees as a proof tree generator, a semantic tableau generator, and a logic tree generator.

Screenshot

Screenshot of the Linux GTK2 version of ProofTools 0.4 beta

Download

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

[1] Oops, this was a copy of the 64-bit Linux GTK2 file; I've deleted it and won't bother to repackage the correct file given that a new version of ProofTools has since been released

[2] (Update: as of version 0.4 beta, this footnote no longer applies: the required Qt4Pas library files are included with the program, and moving them to /usr/local/lib is optional). Whilst the Qt versions of ProofTools require the Qt library, and you can almost certainly install this library automatically through your package manager, they also require the Qt4Pas shared library to be present at /usr/local/lib, and you will almost certainly need to install this library manually. You can download it from this page, clicking on the "X11 i386 Libray Binary" link if you are downloading the 32-bit version of ProofTools, and clicking on the "X11 x86-64 Libray Binary" link if you are downloading the 64-bit version of ProofTools. Unpack to /usr/local/lib (you will probably need superuser privileges to write to this location) the .so files in the archive that you download. What benefit do you get from this? The Qt version of ProofTools will handle the drawing of larger trees that will cause the GTK2 version to error out.


Known bugs and limitations

Whilst we are not aware of any 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.

Inadequate fonts on Windows XP and earlier

By default, none of the fonts provided on Windows XP (and presumably all earlier versions of Windows) support all of the logic characters used by this program, and those unsupported logic characters show up as rectangles. This can be remedied by installing a font that supports these characters, and by then selecting that font in the program. One set of free fonts that supports these characters is the DejaVu fonts, which can be downloaded from that link, and, after unzipping them, installed using these instructions. Once installed, you can then set one of them to be the program's font by clicking on the font button in the top left of the screen, or by pressing ctrl+F (you will need to separately set the font for both the interface and for the tree; currently settings are not saved so you will need to do this each time you run the program).

Collaboration

Emil Kirkegaard instigated this project and continues to collaborate with me on it.