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.
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.
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.
- Bugfix: the Substitutivity of Identicals rule was not being applied to identities themselves, such that the logical truth (a=b∧c=b)→a=c was not being evaluated as a logical truth.
- Bugfix: world numbers were sometimes displaying when they shouldn't have.
- Bugfix: the form was oversize on initial opening on OS X.
- Changed a symbol replacement: \/ (backslash, forward slash) is now replaced with the disjunction operator, ∨, rather than the universal quantifier, ∀.
Version 0.4 beta, released 3 Jun 2013
- Support for normal modal logics, including both basic, K, and those characterised by one or more of reflexivity, symmetry, transitivity and extendability, which includes support for S5. This implementation of modal logic has constant domain when quantified, and contingent identity.
- Support for identity (a=b) and negated identity (a≠b).
- Support for numbered predicate, proposition, variable and constant names.
- Support for symbol replacements whilst editing formulas (e.g. <-> is replaced with ↔).
- Support for Tarski's world syntax via a checkbox (by request).
- Optimised rule generation/application such that potential applications of rules that would add only nodes that already exist on the branch are ignored.
- Optimised rule choice so that rules that would close the branch are chosen ahead of all others.
- A battery of tests accessible from the File menu.
- Bugfix: the width of the tree panel was sometimes greater than it needed to be for some trees when scrollbars were visible.
- OS X bugfix: the status icon wasn't changing colour.
- Parser error-detection bugfix: the parser failed to pick up a certain type of error in certain cases, that error being when a predicate was specified multiple times with a different number of variables (the actual conditions for the error were more specific than this). An example of a formula containing this type of error (w.r.t. the P predicate) that would fail to be detected by the parser is ∃x∃yPxy∧Qxy∧∃zPxyz∧Qxy.
Version 0.3.2 beta, released 14 Dec 2012
- First Mac release! Contains compatibility fixes for Mac OSX, x86 (Intel) platform only - otherwise is identical with the previous 0.3.1 beta release, hence no new files have been released for existing platforms.
- Note: this first release is not perfect - in particular, the validation status icon (the square at the left of the status bar bottom of application) never changes colour - you will need to rely on the messages in the status bar.
Version 0.3.1 beta, released 16 Nov 2012
- Bugfix: fixed a bug that could cause invalid arguments to be assessed as valid: the same constant was sometimes used for multiple separate applications of the universal quantifier rule.
- Bug/build fix: fixed a bug of unknown origin in the prior release whereby clicking on symbol buttons in the Linux builds resulted in symbols being inserted at the beginning of the active text box rather than at the cursor.
Version 0.3 beta, released 12 May 2012
- Bugfix (a parsing bug): fixed a bug that was exemplified by ∀xCa∧Dx→Fax being incorrectly parsed as ((∀x)Ca∧Dx)→Fax instead of (∀x)(Ca∧Dx→Fax). This was due to unary operators (including quantifiers) being bound to the first binary operator that follows, rather than to the lowest precedence binary operator that follows within the scope of the unary operator.
- Overhauled the drawing code majorly for speed and efficiency, replacing TLabel components with direct drawing to the canvas.
- Bugfix: fixed a bug that had been causing two problems: trees being bigger than they needed to be, and the wrong secondary node (the one from which the constant was taken) being highlighted when mousing over a node generated by a universal quantifier rule application.
- Bugfix: (mostly) solved a problem where scrollbars would appear or disappear when they ought not to during resizing of the main window.
Version 0.2.2 beta, released 19 October 2011
- Bugfix: only the first of multiple identical variables in a predicate was being replaced with a constant in a universal quantifier rule application.
- Bugfix: certain expressions, such as (∀x)(Fx)∨¬(∃x)(¬(Fx)), were being incorrectly parsed.
- A re-fix of the parse error message "fixed" in 0.2.1 beta.
- Bugfix: after hovering the mouse pointer over a node and then changing the tree's background colour using the background colour dialogue button, the node's background colour was not updating from its old colour until the mouse pointer was again hovered over it.
Version 0.2.1 beta, released 30 October 2010
- Bugfix: unclosed branches were randomly falsely being labelled infinite.
- Minor correction: fixed a faulty parse error message.
- The validation status messages for when only a conclusion is set have been adjusted to indicate that rather than being an (in)valid argument it is or is not a logical truth.
Version 0.2 beta, released 25 October 2010
- Support for predicate logic including detection of infinite loops on a branch. There is no support yet for nested functions although this is planned for down the road.
- Holding the mouse pointer over a node now highlights the node/s it was generated from, and displays in the status bar the rule that was used to generate it.
- Operator precedence and tolerance of missing pairs of parentheses.
- Customisable hotkeys.
- The ability to draw a tree based on premises only and without setting a conclusion.
- Enhancements to the status bar including separation of messages from the status of the validation, and colourisation of the status of the validation.
Version 0.1 beta, released 27 September 2010
- Initial public release. Contains support for validation of propositional logic proofs using the method of proof tree, also known as semantic tree, analytic tableau and semantic tableau.
 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
 (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.
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).
Emil Kirkegaard instigated this project and continues to collaborate with me on it.