ProofTools: a symbolic logic proof tree generator

Update of 18 October 2014: a deficiency in infinite branch detection has come to my attention, the implication of which is that on rare occasions, ProofTools might give the wrong result.

Update of 24 October 2014: it's official, ProofTools's infinite branch detection definitively fails in certain cases.

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 Qt version of ProofTools 0.5 beta

Download

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:

  • Bugfix: sometimes, when starting the app, its main window's status bar was invisible until that window was resized.
  • Added copy-to-clipboard support for both individual nodes (plain text) and the entire tree (as an image), accessible via a right-click context menu.
  • Added counter-model popups, fully supporting propositional, predicate and modal logic in any combination, with a copy-to-clipboard feature accessible via a right-click context menu.
  • Added support and a toggle box for the modal Euclidean accessibility relation ε, equivalent to toggling modal axiom 5.
  • Added a new dropdown box for all basic/normal modal logic variants - selecting an item in the dropdown sets the appropriate toggles of reflexivity, symmetry, transitivity, extendability, Euclidean and S5. Items in the dropdown are prefixed by a number - equivalent modal logic variants share the same number. For completeness, all included modal logic variants parenthesised into their fifteen equivalent groups are: (K), (KB), (KD), (KT, KDT, T), (K4), (K5), (KBD), (KBT, KBDT), (KB4, KB5, KB45), (KD4), (KD5), (KT4, KDT4, S4), (KT5, KBD5, KBD4, KBT4, KBT5, KDT5, KT45, KBD45, KBT45, KDT45, KBDT4, KBDT5, KBDT45, S5), (K45) and (KD45).
  • Decoupled the S5 toggle box from the other modal accessibility relation toggle boxes (toggling it on now untoggles the rest), because in actuality the S5 proof tree rules are distinct from the other modal accessibility relation proof tree rules.
  • Added several new tests based around the normal modal axioms.
  • Bugfix: sometimes, adding a premise to, or changing the conclusion of, an existing argument, or clearing and then rerunning a proof, gave the wrong result (different to the original run, if any), due to state data not being correctly cleared. e.g. toggling S5 on and then setting a premise of □P, and a conclusion of □□P∨∀xQx→Px∧x=a, then clicking "Show proof", (correctly) showed a "Valid argument" result, but then clicking "Clear proof" followed by "Show proof" (incorrectly) showed an "Invalid argument" result.
  • Corrected the hints for constant/variable shortcut buttons.
  • Bugfix: sometimes, randomly, the second branch of a disjunct which should have had a modal extensibility rule applied to it and then been labelled infinite was instead left open.

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:

  • Turned the "abbreviated tree" feature into an option (accessible via a checkbox), defaulting to off rather than mandatorily on as it had been.
  • Implemented greater sophistication of handling of parentheses, including:
    • Provided an interface option (a dropdown box) to (de)normalise parentheses, either universally across the tree, or from the current point onwards.
    • Implemented the parsing, storing and reproducing of all parentheses including those subsequent to unary operators, to any level of nesting.
    • Bugfix: individual constants/variables were being incorrectly parenthesised in identities under Tarski syntax.
    • Bugfix: when applying a negated universal/existential quantifier rule, or a negated necessity/possibility rule, and the negation operator is switched inside to apply to a term involving a binary operator which wasn't yet parenthesised, parentheses weren't being generated to make it clear that the negation operator applied to the entire binary term rather than to just the first one.
  • Split the settings toolbars into four, so that the minimum width of the app can be reduced to approximately 640 pixels - to support resolutions of 640x480.
  • Added symbols for several common proposition/predicate/variable/constant names, so that the mouse can be used entirely for entry without needing to intersperse mouse clicks with keyboard entry.
  • Added three new symbol replacements, /\ (forward slash, backslash) for conjunction, -| for negation, and -] for the existential quantifier.
  • Bugfix: when "abbreviated tree" was enabled (which until now it had been mandatorily), sometimes duplicate identity nodes were not being detected.
  • Bugfix: under the GTK2 widgetset, when the active premise/conclusion entry box cursor was at a location prior to the end of the text in the box, clicking a symbol button would insert the symbol in the wrong place (at the beginning or end of the text).
  • Propagated font changes to secondary windows (the hotkey editor and test results windows).

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. [Update 15 October 2014: the question has now been answered, see the link for details]

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:

  • 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

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:

  • 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

mac osx x86

New features:

  • 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

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:

  • 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

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:

  • 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

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.

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.
  • [3] Something seems to have gone wrong with the build process, and the binary I originally provided here was in fact a GTK2 build rather than a Qt build. I have deleted the file to avoid any further confusion.

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.

  • This wording updated majorly on 24 Oct 2014. The infinite branch detection algorithm (see also its documentation in the manual) that Emil and I developed for ProofTools is flawed: it gives the wrong results in certain cases. The simplest example of which I'm aware is the formula (entered as a premise) ∀x(∃y(Ry∧¬Rx)). The proof tree built from this formula should close, however ProofTools incorrectly marks it as infinite. I understand why this occurs, and am working on fixing the algorithm. I believe that it is possible to fix the algorithm such that it is reliable, however this belief seems to be contradicted by something that I learnt recently: that predicate logic is considered to be undecidable due to the separate efforts of Alonzo Church and Alan Turing in solving the Entscheidungsproblem, and thus that a perfect infinite branch detection algorithm for it does not exist (Emil believes he told me this at the time we developed it, however I don't recall this, I must have misunderstood him - had I registered what he said, I would have back then taken the approach that, as I describe next, we will take in the next release). I intend to research this further to discover exactly what these proofs prove, and whether they are limited to certain types of formulas, because it is obvious that at least some infinite loops can be detected mechanically. Nevertheless, out of respect for these findings, in the next version, not only will the known infinite branch detection bugs be fixed, but infinite branch detection will also be togglable, and it will be possible to, in the case that any branch is labelled infinite, repeat the proof with detection disabled, stepping through a given number of rule applications at a time (the existing "Step" button will be augmented with an integer input to stipulate the number of rule applications to apply at each step, defaulting to one), to get a sense for yourself as to whether it does indeed seem to be infinite (even though it is not possible to confirm this for certain).

    What this bug means for you: put simply, if ProofTools marks any branch as infinite, it might be wrong, and the branch might actually close. Thus, any formula (conclusion) / argument deemed by ProofTools to be NOT a logical truth / valid argument due to infinite branches might in fact BE a logical truth / valid argument. If, however, ProofTools doesn't mark any branches as infinite, then this bug does not apply, and as far as we know the results that ProofTools gives can be trusted.

  • Parentheses normalisation sometimes adds extraneous pairs of parentheses. For example, the formula ◊∀xPx∨Qx∧¬a=b when parentheses are normalised appears as (◊(∀x)((Px∨Qx)))∧(¬(a=b)) i.e. there is an extraneous pair of outer parentheses, and an extraneous pair of parentheses around Px∨Qx. I am yet to look into this bug and come up with a fix - it's kind of a fiddly area of the code.
  • The tooltip (popup hint) for the "T" shortcut button mistakenly classifies it as a variable identifier when it is in fact a proposition/predicate identifier.

Note that our question about the semantics of the Substitutivity of Identicals rule for modal tableaux, for which we had previously been soliciting answers here and above, has now been answered.

Known limitations

  • Awkward counter-model popup behaviour: The counter-model popups are coded as "normal" windows (albeit lacking borders), which on some platforms means that they must be switched through separately when using task-switching (e.g. using Alt+Tab). If anyone can suggest to me a better cross-platform way to code popup windows with Lazarus, I'd be very grateful.
  • Slow drawing for large trees: The code for drawing trees slows dramatically as the number of nodes increases, so that trees of several thousand nodes or more take very unreasonable periods of time (in the realm of hours) to be drawn. Unfortunately, whilst modest improvements are possible for only a little effort, the primary culprit is the fundamental design of the positioning code, and the fix will take some effort - I have no ETA for it.
  • Very large trees aren't supported: Depending on your platform, ProofTools will either crash, or fail to correctly display, very large trees. How large is "very" large? I don't have exact figures, and it depends on your platform, but roughly in the realm of tens of screen widths wide or high.
    Explanation: ProofTools draws the entire tree to an image component (TImage), which it then allows the user to scroll within the viewport. There appear to be certain undocumented constraints, depending on the runtime platform, on the size to which a TImage can grow, outside of which either an exception is raised (which ProofTools currently does not handle, leading to a crash), or methods to draw to its canvas do not do what they are supposed to do. It would be possible to remove this constraint, and to allow for unlimited (other than the constraint of available memory) size trees by eliminating the full-tree image drawing, and instead drawing on demand only the region of the tree within the viewport. This, however, would require fairly extensive changes to the code, and there is at this point no expected timeframe within which those changes will be made.
  • 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 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 has higher priorities - mostly, publishing papers at the open access, free to publish, open peer review scientific journals that he founded, Open Differential Psychology and Open Behavioral Genetics - but he can still be tempted into offering advice, suggestions and feedback on ProofTools.