ProofTools
ProofTools is a freely downloadable cross-platform software application for automatically and graphically validating logical formulas and proofs/arguments: it checks either whether an individual formula is a logical truth or whether the conclusion of an argument follows logically from that argument's premises. ProofTools is still under development and this is a preliminary version that lacks some features. Currently it can validate propositional and predicate logic arguments - and it also supports the validation of individual propositional or predicate logic formulas - using the method of proof tree, also known as semantic tree, analytic tableau, analytic tableaux, semantic tableau, and semantic tableaux. Planned is support for truth table proofs and modal logic (S5).
ProofTools is documented in the ProofTools manual and in the ProofTools background and technical addendum page.
ProofTools is developed with Lazarus, a free cross-platform Delphi-like Object Pascal integrated development environment.
The current version of ProofTools may be downloaded freely; please, however, 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. The ProofTools source code is not currently publicly available but that might change for future versions.
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 for any other good reason.
Screenshot
Download
Sorry, no Mac versions as yet.
Version 0.3 beta, released 12 May 2012
linux x86 32-bit, GTK2 linux x86 32-bit, Qt linux x86 64-bit, GTK2 linux x86 64-bit, QT win32 win64
New features:
- Bugfix (a parsing bug): fixed a bug that was exemplified by ∀xCa∧Dx→Fax being incorrectly parsed as (∀xCa∧Dx)→Fax; this was due to unary operators (including quantifiers) being bound to the first binary operator that follows, rather than with 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
linux x86 32-bit, GTK2 linux x86 64-bit, GTK2 win32 win64
New features:
- 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
linux x86 32-bit, GTK2 linux x86 64-bit, GTK2 win32 win64
New features:
- 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
linux x86 32-bit, GTK2 win32 win64
New features:
- 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
linux x86 32-bit, GTK2 win32 win64
- 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.
Known bugs and limitations
Unless otherwise mentioned, the bugs and limitations below refer to the latest version of the software.
There are hard-coded limits of 21 different constant names and 5 different variable names throughout the tree. This uses up all of the lowercase letters of the alphabet. This is a design limitation of the syntax, which allows only for single-character variables and constants. There is also a hard-coded limit of 26 different proposition names and 26 different predicate names. This uses up all of the uppercase letters of the alphabet. It is planned that in the next release, these design limitations will be removed by allowing names to be constructed by appending any number of apostrophes to a base character.
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.
