A feature comparison of free[65] proof tree software

Proof trees are also known as semantic tableaux, analytic tableaux, semantic trees and truth trees, and are generally used to determine whether a formula is a logical truth or whether an argument is valid. The free programs and web applications listed below are based on the proof tree method.

See also below for proof tree and related software that isn't (yet) in the comparison:

Note that this comparison does not take into account any optimisations (e.g. use of the unification method) or suitability for large-scale use (many formulas) that a proof tree software tool might support: it assumes student-level or casual use on relatively small (sets of) formulae.

Legend:

FeatureSoftware
  ProofTools Tree Proof Generator Gabriel Lemonde-Labrecque's Truth Tree Solvers Douglas Owings' Logic Tableaux Generator [104] MOLTAP Molle LoTREC Generic Tableau Prover SoftOption ® Tree Widgets and Deriver app [75] Tableau3 TABLEAUX [103] OOPS [31] LIG's tableaux methods The Tableau Workbench (TWB) タブ朗 [42] KLMLean [59] LogikKriger [66] ALCI prover TTM Saga Tableaux for ATL Sibyl pdl-tableau

Overview of logics supported

 
Propositional Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes [57] Yes [63] Yes Yes Yes Yes [85] Yes Yes Yes
Predicate Yes Yes Yes No No No No Yes Yes Yes No No No Yes [53] No No No No ½ [79] No No Yes
With identity Yes No No No No No No Yes Yes No No No No Yes [58] No No No No ½ [79] No No No
Basic/normal modal Yes No No Yes Yes Yes Yes Yes No No Yes Yes Yes No No No ½ [72] No No No No No
With predicates Yes No No No No No No Yes No No No No No No No No No No No No No No
Multimodal No No No No No No Yes No No No No No Yes No No No ½ [72] Yes No No Yes Yes
Other extended modal No No No No No No Yes No No No Yes No Yes No No No No No No Yes No No
Description logic No No No No No No ½ [43] No No No No No No No No No Yes No No No No No
3-valued No No No Yes No No ½ [1] No No No No No No No No No No No No No No No
Intuitionistic No No No No No No Yes No No No No Yes Yes No No No No No No No No No
KLM No No No No No No ½ [1] No No No No No Yes No Yes No No No No No No No
Misc other No No No Yes No No Yes No No No No No No No No No No No Yes No No No
  
Supports custom/user-supplied logic definitions No No No No No No Yes No No No No No No No No No No No No No No No

Basic and normal modal logics supported

 
K Yes No No Yes Yes [45] Yes Yes Yes No No Yes No Yes No No No ½ [72] No No No No No
KB Yes No No No No No Yes No No No Yes No No No No No No No No No No No
KD Yes No No Yes Yes [45] No Yes No No No Yes No Yes No No No No No No No No No
T aka KT, KDT Yes No No Yes Yes [45] No Yes Yes No No Yes No No No No No No No No No No No
K4 Yes No No No Yes [45] No Yes No No No Yes No Yes No No No No No No No No No
K5 Yes No No No Yes [45] No Yes No No No No No No No No No No No No No No No
KBD Yes No No No No No Yes No No No No No No No No No No No No No No No
B aka KBT, KBDT Yes No No No No No Yes No No No No No No No No No No No No No No No
KB4 aka KB5, KB45 Yes No No No No No Yes No No No No No No No No No No No No No No No
KD4 Yes No No No Yes [45] No ½ [43] No No No No No No No No No No No No No No No
KD5 Yes No No No Yes [45] No ½ [43] No No No No No No No No No No No No No No No
S4 aka KT4, KDT4 Yes No No No Yes [45] No Yes Yes No No Yes Yes Yes No No No No No No No No No
S5 aka KT5, KBD4, KBD5, KBT4, KBT5, KDT5, KT45, KBD45, KBT45, KDT45, KBDT4, KBDT5, KBDT45 Yes No No No Yes Yes Yes Yes No No Yes No No No No No No No No No No No
K45 Yes No No No Yes [45] No Yes No No No Yes No No No No No No No No No No No
KD45 Yes No No No Yes [45] No Yes No No No Yes No Yes No No No No No No No No No
  
Supports individual toggling of reflexivity, transitivity, symmetry, extendability/seriality and Euclidean relations Yes No No No Yes [40] No No No No No No No No No No No No No No No No No

Multimodal logics supported

 
K2 No No No No No No Yes No No No No No No No No No No No No No No No
KConfluence No No No No No No Yes No No No No No No No No No No No No No No No
K + universal No No No No No No Yes No No No No No No No No No No No No No No No
Multi S5 PAL No No No No No No Yes No No No No No No No No No No No No No No No
Propositional dynamic logic (PDL) No No No No No No Yes No No No No No Yes No No No No No No No No Yes
Multimodal hybrid logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies No No No No No No No No No No No No No No No No No No No No Yes No

Other extended modal logics supported

 
K + common knowledge ("KE") [46] No No No No Yes [71] No ½ [43] No No No Yes No No No No No No No No No No No
S4 + common knowledge ("S4E") [46] No No No No Yes [71] No ½ [43] No No No Yes No No No No No No No No No No No
S5 + common knowledge ("S5E") [46] No No No No Yes [71] No ½ [43] No No No Yes No No No No No No No No No No No
Hybrid logic H No No No No No No Yes No No No No No No No No No No No No No No No
Linear-time temporal logic (LTL) aka propositional temporal logic (PTL) aka propositional linear temporal logic (PLTL) No No No No No No Yes No No No No No Yes No No No No Yes No No No No
Propositional computation tree logic (CTL) No No No No No No ½ [43] No No No No No Yes No No No No No No No No No
Alternating-time temporal logic (ATL) No No No No No No No No No No No No No No No No No No No Yes No No

Description logics supported

 
ALC No No No No No No ½ [43] No No No No No No No No No Yes No No No No No

Intuitionistic logics supported

 
LJ No No No No No No Yes No No No No No No No No No No No No No No No
G4IP No No No No No No ½ [43] No No No No No Yes No No No No No No No No No
Through S4-translation No No No No No No ½ [43] No No No No Yes No No No No No No No No No No

KLM logics supported

 
Cumulative logic C No No No No No No ½ [43] No No No No No No No Yes No No No No No No No
Loop-cumulative logic CL No No No No No No ½ [43] No No No No No No No Yes No No No No No No No
Preferential logic P No No No No No No ½ [43] No No No No No Yes No Yes No No No No No No No
Rational logic R No No No No No No ½ [43] No No No No No No No Yes No No No No No No No
With free variables No No No No No No ½ [43] No No No No No No No Yes No No No No No No No

3-valued logics supported

 
Kleene No No No Yes No No ½ [1] No No No No No No No No No No No No No No No
Lukasiewicz No No No Yes No No ½ [1] No No No No No No No No No No No No No No No
Gappy objects [41] No No No Yes No No ½ [1] No No No No No No No No No No No No No No No

Misc other logics supported

 
First degree entailment (FDE) No No No Yes No No ½ [1] No No No No No No No No No No No No No No No
Logic of paradox (LP) No No No Yes No No ½ [1] No No No No No No No No No No No No No No No
StIt No No No No No No Yes No No No No No No No No No No No No No No No
Guarded fragment of predicate logic No No No No No No No No No No No No No No No No No No Yes No No No

Input

 
Supports end-user input of premises/conclusion Yes Yes Yes Yes Yes Yes Yes Yes Yes [17] Yes Yes [32] Yes Yes Yes Yes [62] Yes Yes Yes Yes [80] Yes Yes [95] Yes
Supports infix notation Yes Yes Yes Yes Yes Yes No [3] Yes Yes Yes Yes [32] Yes Yes Yes Yes Yes Yes Yes No Yes Yes [95] No
Tolerates missing parentheses in infix notation i.e. implements operator precedence Yes Yes No No Yes Yes No Yes Yes Yes Yes [32] Yes Yes Yes Yes Yes [67] Yes No No Yes Yes No
Supports Polish notation No No No Yes No No Yes No No No No No No No No No No No Yes [80] No No Yes
Supports WYSIWYG entry i.e. input of actual logic symbols Yes No Yes No No [4] No No Yes Yes No No No No Yes No Yes No No No No No No
Supports shortcut keys/phrases for logic symbols i.e. doesn't require mouse button clicks or copy+paste to input symbols Yes Yes No Yes Yes Yes Yes No Yes Yes Yes Yes Yes No [56] Yes Yes No Yes Yes Yes Yes Yes
Supports natural language operator entry e.g. conjunction is "and" No No No No Yes [5] No Yes No No No No No No No [56] Yes [60] Yes No No Yes No No Yes
Supports cut/copy/paste from/to formula bar(s) Yes Yes Yes Yes Yes Yes Yes Yes Yes [6] Yes Yes Yes Yes Yes Yes Yes ½ [73] Yes ½ [80] Yes [86] ½ [95] Yes
Number of unique valid identifiers possible for input propositional/predicate and constant/variable names Infinite [7] Infinite [8] 26 and 26 [9] 5 (A to E) Infinite [10] Infinite [11] Infinite [12] Infinite and 26 [13] 26 and 26 [14] 5 and 5 [15] 26 (a-z) Infinite [47] Infinite [48] 14 and 12 [54] Infinite [10] 26 (A-Z) Infinite [74] 26 (a-z) Infinite [81] Infinite [87] Infinite [96] Infinite [100]

Output

 
Draws trees graphically Yes Yes Yes Yes No No [16] ½ [44] Yes Yes [18] Yes Yes [33] No [16] No [49] ½ [55] Yes Yes [66] No No No No [88] No [97] No [101]
Supports changing the font and foreground/background colour of the output tree Yes No No No No No No No No No No No No No [56] No No No No No No No No
Supports saving of output as an image Yes No Yes Yes No No No No No No No No No No [56] No Yes No No No No No No
Supports saving of output as LaTeX No No No Yes No No No No No No No No No No [56] Yes No No No No No Yes [97] No
Output contains actual logic symbols (e.g. ↔ rather than <=>) Yes Yes Yes No Yes No No Yes Yes No Yes No No Yes No Yes No No No ½ [89] Yes [97] No
Outputs counter-models (i.e. for open branches) Yes Yes No No Yes Yes [36] ½ [44] No No No Yes [33][36] Yes No No [56] No No No Yes ½ [82] ? [90] ½ [97] No
Outputs models (i.e. for closed branches) No No No No No Yes [36] ½ [44] No No No No No No No [56] No No No No No No No No
Supports all-in-one automated solving Yes Yes Yes Yes Yes Yes Yes No Yes No Yes Yes Yes No [56] Yes Yes Yes Yes Yes Yes Yes Yes
Supports step-by-step automated solving Yes No No No No No Yes No No No No No No No [56] No No No No No No No No
Supports user-led solving i.e. user chooses which node to decompose No No No No No No No Yes No Yes No No No Yes No No No No No No No No
Prevents infinite trees ½ [19] ½ [20] No [21] Yes [22] ½ [70] Yes [23] Yes [24] Yes [25] ? [26] Yes [25] Yes [34] Yes [50] Yes [50] Yes [25] Yes [61] Yes [68] ? ? [78] Yes [83] ? [91] ? [98] ? [102]

Interface, supported platforms, source code and version/date tested

 
Web interface No Yes Yes Yes Yes No No Yes Yes Yes No Yes Yes Yes No Yes No No No Yes No Yes
Supports offline use Yes Yes [27] No No Yes [30] Yes Yes Yes Yes [27] Yes Yes No Yes [51] Yes [27] Yes Yes [69] Yes Yes Yes Yes Yes No
Supported platforms Win, Mac, Linux All All All All All All All All All All All All All Win, Mac, Linux, Solaris All Linux, possibly others that run OCaml Win, Linux All [84] All/Linux [92] Linux All
Development language(s) Lazarus (Object Pascal) Javascript (browser-based) ? PHP (browser-based) Ghc: the Glasgow Haskell Compiler Java Java Javascript (browser-based) and Java (browser-based and standalone) [75] Java (browser-based) Java (browser-based) Java ? OCaml Javascript (browser-based) Java / SICStus Prolog Javascript (browser-based) OCaml ? Common Lisp OCaml and PHP (browser-based) [94] OCaml ?
Source code available No Yes No Yes [here] Yes [here] Yes [here] Yes [here] No [28] No [29] No [29] Yes [here] [35] No [29] Yes [here] [51] No [29] Yes Yes [here] Yes No Yes No No No
Version/date tested 0.5 beta (2014-10-09) v2.08 (2013-12-28) Circa 2014-05-18 Circa 2014-05-18 Circa 2014-05-18 1.0 2.0 Circa 2014-05-18 and 2014-10-22 [76] 0.21 Circa 2014-05-18 Extensions circa 2014-05-18 Circa 2014-05-18 Circa 2014-05-18 Circa 2014-05-29 2.1 (supplied privately) GitHub commit f82a..37e3 of 2014-03-13 2014-07-17 0.8-1? (downloaded Linux build on 2015-02-06) ? (downloaded 2015-02-07) September 2014 and 2015-02-07 [93] 2.1.2 23 Feb 2007 (per footer)

Footnotes

Other notable mentions

Unevaluated software

For the reasons stated below, I have not added comparisons for the following other proof tree packages:

TODO

Yet to be evaluated and added to the comparison is the following proof tree software. Most of these were found on, or by following links on, the AiML: Tools page maintained by Renate Schmidt.

Export the data behind this page

The data used to generate this page can be downloaded in PHP format and used without restriction: I release it into the public domain.