A feature comparison of free proof tree aka semantic tableau 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[65] programs and web applications listed below are based on the proof tree method, or, in other words, this is a list of free semantic tableau software.

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 a need only for student-level or casual use on relatively small (sets of) formulae.

Information sign Tip: Check the feature checkboxes to narrow down the list to software that supports those features.

Legend:

FeatureSoftware
  ProofTools Tree Proof Generator Gabriel Lemonde-Labrecque's Truth Tree Solvers Douglas Owings' Logic Tableaux Generator [104] MOLTAP [105] 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 [107] Sibyl pdl-tableau An Optimal Tableau Prover for CPDL-Satisfiability CTL-satisfiability provers COOL - The Coalgebraic Ontology Logic Reasoner Konclude FaCT++ Gost LCKS5-satisfiability tableau prover (optimal) MLTP PDL-satisfiability tableau prover (optimal) Pellet PLTL-satisfiability theorem prover (tree) Spartacus semantic-tableau-cpp SPASS v3.5+: A tableau-resolution prover

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 Yes Yes Yes No [119] No [119] Yes Yes Yes Yes No [119] Yes 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 No No No No No No No No No No No 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 No No No No No No No No No No No No No Yes
Basic/normal modal Yes No No Yes Yes Yes Yes Yes No No Yes Yes Yes No No No ½ [72] No No No Yes Yes No No Yes No No No No Yes No No No Yes No Yes
With predicates Yes No No No No No No Yes No No No No No No No No No No No No No No 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] No No No Yes Yes Yes No Yes No No No No No Yes No No No No No
Temporal logic No No No No No No Yes No No No No No Yes No No No No Yes No Yes No No No Yes Yes No No No No No No No Yes No No No
Hybrid logic No No No No No No Yes No No No No No No No No No No No No No Yes No No No No No No No No No No No No Yes No No
Other extended modal No No No No No No Yes No No No Yes No No No No No No No No No No No No No Yes No No No Yes No No No No No 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 No No Yes Yes Yes No No No No Yes No No No Yes
3-valued No No No Yes No No ½ [1] No No No No No No No No No No No No No No 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 No No No No No 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 No No No No No No No 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 No No No No No Yes 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 Yes Yes Yes No Yes No No No No Yes No No No Yes No Yes
KB Yes No No No No No Yes No No No Yes No No No No No No No No No No No No No No No No No No No No No No No No Yes
KD Yes No No Yes Yes [45] No Yes No No No Yes No Yes No No No No No No No No No No No Yes No No No No No No No No Yes No Yes
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 No No No No No No No No No No No Yes No Yes
K4 Yes No No No Yes [45] No Yes No No No Yes No Yes No No No No No No No Yes No No No No No No No No No No No No Yes No Yes
K5 Yes No No No Yes [45] No Yes No No No No No No No No No No No No No No No No No No No No No No No No No No No No Yes
KBD Yes No No No No No Yes No No No No No No No No No No No No No No No No No No No No No No No No No No No No Yes
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 No No No No No No No No No No No No No Yes
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 No No No No No No No No No No No No No Yes
KD4 Yes No No No Yes [45] No ½ [43] No No No No No No No No No No No No No No No No No No No No No No No No No No Yes No Yes
KD5 Yes No No No Yes [45] No ½ [43] No No No No No No No No No No No No No No No No No No No No No No No No No No No No Yes
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 No No No No No No No No No No No Yes No Yes
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 No No No No No No Yes No No No No No No Yes
K45 Yes No No No Yes [45] No Yes No No No Yes No No No No No No No No No No No No No No No No No No No No No No No No Yes
KD45 Yes No No No Yes [45] No Yes No No No Yes No Yes No No No No No No No No No No No No No No No No No No No No No No Yes
  

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 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 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 No No No No No No No No No No No No No No
Multimodal KD No No No No No No No No No No No No No No No No No No No No No No No No Yes 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 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 No No No No No No No No Yes No No No No No
Propositional dynamic logic with converse (CPDL) No No No No No No ½ [43] No No No No No No No No No No No No No No No Yes No No No No No No No No No No No No No
Graded modal logic (GML) [the Q in description logic ALCQ] No No No No No No ½ [43] No No No No No No No No No No No No No No No No No Yes No No No No No No No No No No No

Temporal logics supported

 
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 No No No No No No No No No No Yes 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 No Yes No No No No No No No No No No No No
Alternating-time temporal logic (ATL) [extends CTL] No No No No No No ½ [43] No No No No No No No No No No No No Yes No No No No No No No No No No No No No No No No
Coalition logic (CL) [the next-step logic of ATL] No No No No No No ½ [43] No No No No No No No No No No No No No No No No No Yes No No No No No No No No No No No

Hybrid logics

 
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 No No No No No No No No No No No Yes No No
Multimodal hybrid logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies No No No No No No ½ [43] No No No No No No No No No No No No No Yes No No No No No No No No No No No No No No 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 No No No 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 No No No No No No No No No No No No No No
S5 + common knowledge ("S5E" or "CKS5") [46] No No No No Yes [71] No ½ [43] No No No Yes No No No No No No No No No No No No No No No No No Yes No No No No No No No
Probabilistic modal logic (PML) No No No No No No ½ [43] No No No No No No No No No No No No No No No No No Yes No No No No No No No No No No No

Description logics supported

 
ALC aka multimodal K No No No No No No ½ [43] No No No No No No No No No Yes No No No No No No No Yes No No No No No No No No No No ?
SHOIN(D) No No No No No No No No No No No No No No No No No No No No No No No No No ? ? No No No No Yes No No No ?
SROIQ(D), including (partial) support for OWL 2 ontologies No No No No No No No No No No No No No No No No No No No No No No No No No ? Yes No No No No Yes No No No ?
SROIQV(D), including support for OWL 2 ontologies No No No No No No No No No No No No No No No No No No No No No No No No No Yes [121] No No No No 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 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 No No No No No 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 No No No No 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 No No No No No No No 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 No No No No No No No 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 No No No No No No No 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 No No No No No No No 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 No No No No No No No 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 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 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 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 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 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 No No No No No No No No No No No No No No
Guarded fragment of predicate logic (GF1-) No No No No No No ½ [43] No No No No No No No No No No No Yes No No No No No No No No Yes No No No No No No No No

Functionality

 
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 No No No No No No No No No No No No No No
Supports individual toggling of the normal modal logic relations: reflexivity, transitivity, symmetry, extendability/seriality and Euclidean Yes No No No Yes [40] No No No No No No No No No No No No No No No No No No No No No No No No No No No No ½ [134] No ½
Supports the combining of its supported logics Yes No No No No No ½ No No No No No No No No No No No No No No No No No Yes [118] No No No No No No No No No No No
Can function as a server accepting client requests No No No No No No No No No No No No No No No No No No No No No No No No No Yes No No No No No No No 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 Yes Yes Yes Yes Yes Yes [123] Yes Yes Yes Yes Yes Yes Yes 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 Yes Yes Yes No No No Yes No Yes No Yes Yes Yes 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 Yes Yes Yes No No No Yes No Yes No Yes 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 No No No No Yes Yes [123] No Yes No No No 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 No No No No No No No No No No No No No No
Supports XML notation No No No No No No No No No No No No No No No No No No No No No No No No No Yes No No No No No Yes 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 Yes Yes Yes No No Yes Yes Yes Yes No 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 No No No No ½ No No Yes No No No No No No
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 ½ [108] ½ [108] ½ [115] ½ [120] ½ [122] ½ [123] ½ [127] ½ [128] ½ [133] ½ [120] ½ [133] ½ [135] ½ [133] ½ [133]
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] Infinite [74] Infinite [74] Infinite [74] Infinite [120] Infinite Infinite [124] Infinite [74] Infinite [129] Infinite [74] Infinite [120] Infinite [74] Infinite [136] Roughly 50(?) [137] Infinite [138]

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] No No No No No No No No [131] No No No No No No
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 No No No No No No 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 No No No No No No No No 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 No No No No No No No No No No No No No 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 No No No No No No No No No No No No No 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 No No No No No Yes No No No No No Yes No 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 No No No No No Yes [125] 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 Yes Yes Yes Yes Yes Yes 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 No No No No No No 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 No No No No No No 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] ? [109] ? [112] ? [116] ? [116] ? [116] Yes [126] ? [116] ? [130] ? [102] ? [116] ? [116] ? [116] Yes [68] ?

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

 
Web interface No Yes Yes Yes ½ [110] No No Yes Yes Yes No Yes Yes Yes No Yes No No No Yes No Yes No No No No No No No No No No No Yes No No
Supports offline use Yes Yes [27] No No ½ [30] Yes Yes Yes Yes [27] Yes Yes No ½ [51] Yes [27] Yes Yes [69] Yes Yes Yes Yes Yes No Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes Yes
Executable or web interface supplied (does not require compilation before use) Yes Yes Yes Yes ½ [30] Yes [113] Yes [113] Yes [114] Yes [113] Yes [113] Yes [113] Yes Yes [111] Yes No ½ [110] No Yes No Yes Yes Yes No No Yes Yes Yes No No Yes [132] No No No No No No
Supported platforms Windows, Mac OS X, and Linux All All All All All All All All All All All All All Windows, Mac OS X, Linux, and Solaris All Linux, and probably any that runs OCaml Windows, Linux All [84] All/Linux [92] Linux All Linux, and probably any that runs OCaml Linux, and probably any that runs OCaml Linux, and probably any that runs OCaml Windows, Mac OS X, and Linux Windows, Mac OS X, Linux All [84] Linux, and probably any that runs OCaml Linux, and probably any platform that supports a C++ compiler Linux, and probably any that runs OCaml All Linux, and probably any that runs OCaml Linux, and all others that support the MLton compiler All 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 ? OCaml OCaml OCaml C++ C++ Common Lisp OCaml C++ OCaml Java OCaml ML C++ C
Source code available No Yes No Yes [here] Yes [here] [106] 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 Yes [here] Yes [here] Yes [here] Yes [here] Yes [here] Yes Yes Yes Yes Yes [here] Yes Yes Yes Yes [here]
Version/date tested 0.6.1 (2019-06-13) 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) r1368 (downloaded 2019-07-11) r1368 (downloaded 2019-07-12) Build of 2014-07-21 19:41:25 CEST [117] 0.6.2 1.6.3 (30 May 2014) ? (downloaded 2019-07-21) r1368 (downloaded 2019-08-26) ? (downloaded 2019-10-24) ? (downloaded 2019-11-04) GitHub commit 4c7d...956b of 2017-01-05 r1424 (downloaded 2019-11-07) 1.1.3, downloaded 2019-11-08 GitHub commit bef4...8b47 of 2018-10-02 v3.5+

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.

[None]

Sources

The following listing pages have been or might be used to source tools for listing on this page.

PageOf organisation/group/entityMaintained byNotes
AiML: ToolsAdvances in Modal Logic (AiML)Renate SchmidtThe source of many (most?) of the tools currently in this page's listing.
OWL/ImplementationsW3CThe community (wiki-based)Part of the W3C's Semantic Web project/vision.
List of reasonersOWL @ ManchesterUli Sattler and Nico MatentzogluOnly reasoners for description logic are listed.
SoftwareChair of Automata Theory of the Institute of Theoretical Computer Science of Technische Universitat DresdenFrancesco Kriegel This seems to be the group's own software.
SoftwareLogic and Computation Group, Research School of Computer Science, Australian National University Professor Rajeev P. GoréThis seems to be the group's/professor's own software.

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.