• << The ProofTools homepage
• >> The ProofTools manual page
• >> The ProofTools background and technical addendum page

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:

• Other notable mentions - proof tree software or code that's not quite a readymade or fully-featured tool.
• The unevaluated list - software that I was unable for various reasons to evaluate, but which might work for you.
• The TODO list - software yet to be added to 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.

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

Legend:

• The software implements the feature fully or near enough to be readily usable out of the box.
• ½ The software does not implement the feature fully, but it either implements it to a significant enough extent not to warrant a cross, or it supports the feature with additional configuration by the user.
• The software does not implement the feature at all, not even with additional configuration by the user.

Feature	Software
	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														[57]	[63]				[85]							[119]	[119]					[119]
Predicate														[53]					½ [79]
With identity														[58]					½ [79]
Basic/normal modal																	½ [72]
With predicates
Multimodal																	½ [72]
Temporal logic
Hybrid logic
Other extended modal
Description logic							½ [43]
3-valued							½ [1]
Intuitionistic
KLM							½ [1]
Misc other
Basic and normal modal logics supported
K					[45]												½ [72]
KB
KD					[45]
T aka KT, KDT					[45]
K4					[45]
K5					[45]
KBD
B aka KBT, KBDT
KB4 aka KB5, KB45
KD4					[45]		½ [43]
KD5					[45]		½ [43]
S4 aka KT4, KDT4					[45]
S5 aka KT5, KBD4, KBD5, KBT4, KBT5, KDT5, KT45, KBD45, KBT45, KDT45, KBDT4, KBDT5, KBDT45
K45					[45]
KD45					[45]
Multimodal logics supported
K2
KConfluence
K + universal
Multimodal KD
Multi S5 PAL
Propositional dynamic logic (PDL)
Propositional dynamic logic with converse (CPDL)							½ [43]
Graded modal logic (GML) [the Q in description logic ALCQ]							½ [43]
Temporal logics supported
Linear-time temporal logic (LTL) aka propositional temporal logic (PTL) aka propositional linear temporal logic (PLTL)
Propositional computation tree logic (CTL)							½ [43]
Alternating-time temporal logic (ATL) [extends CTL]							½ [43]
Coalition logic (CL) [the next-step logic of ATL]							½ [43]
Hybrid logics
Hybrid logic H
Multimodal hybrid logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies							½ [43]
Other extended modal logics supported
K + common knowledge ("KE") [46]					[71]		½ [43]
S4 + common knowledge ("S4E") [46]					[71]		½ [43]
S5 + common knowledge ("S5E" or "CKS5") [46]					[71]		½ [43]
Probabilistic modal logic (PML)							½ [43]
Description logics supported
ALC aka multimodal K							½ [43]																													?
SHOIN(D)																										?	?									?
SROIQ(D), including (partial) support for OWL 2 ontologies																										?										?
SROIQV(D), including support for OWL 2 ontologies																										[121]										?
Intuitionistic logics supported
LJ
G4IP							½ [43]
Through S4-translation							½ [43]
KLM logics supported
Cumulative logic C							½ [43]
Loop-cumulative logic CL							½ [43]
Preferential logic P							½ [43]
Rational logic R							½ [43]
With free variables							½ [43]
3-valued logics supported
Kleene							½ [1]
Lukasiewicz							½ [1]
Gappy objects [41]							½ [1]
Misc other logics supported
First degree entailment (FDE)							½ [1]
Logic of paradox (LP)							½ [1]
StIt
Guarded fragment of predicate logic (GF1-)							½ [43]
Functionality
Supports custom/user-supplied logic definitions
Supports individual toggling of the normal modal logic relations: reflexivity, transitivity, symmetry, extendability/seriality and Euclidean					[40]																													½ [134]		½
Supports the combining of its supported logics							½																		[118]
Can function as a server accepting client requests
Input
Supports end-user input of premises/conclusion									[17]		[32]				[62]				[80]		[95]							[123]
Supports infix notation							[3]				[32]										[95]
Tolerates missing parentheses in infix notation i.e. implements operator precedence											[32]					[67]
Supports Polish notation																			[80]									[123]
Supports WYSIWYG entry i.e. input of actual logic symbols					[4]
Supports XML notation
Supports shortcut keys/phrases for logic symbols i.e. doesn't require mouse button clicks or copy+paste to input symbols														[56]
Supports natural language operator entry e.g. conjunction is "and"					[5]									[56]	[60]												½
Supports cut/copy/paste from/to formula bar(s)									[6]								½ [73]		½ [80]	[86]	½ [95]		½ [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						[16]	½ [44]		[18]		[33]	[16]	[49]	½ [55]		[66]				[88]	[97]	[101]								[131]
Supports changing the font and foreground/background colour of the output tree														[56]
Supports saving of output as an image														[56]
Supports saving of output as LaTeX														[56]							[97]
Output contains actual logic symbols (e.g. ↔ rather than <=>)																				½ [89]	[97]
Outputs counter-models (i.e. for open branches)						[36]	½ [44]				[33][36]			[56]					½ [82]	? [90]	½ [97]
Outputs models (i.e. for closed branches)						[36]	½ [44]							[56]														[125]
Supports all-in-one automated solving														[56]
Supports step-by-step automated solving														[56]
Supports user-led solving i.e. user chooses which node to decompose
Prevents infinite trees	½ [19]	½ [20]	[21]	[22]	½ [70]	[23]	[24]	[25]	? [26]	[25]	[34]	[50]	[50]	[25]	[61]	[68]	?	? [78]	[83]	? [91]	? [98]	? [102]	? [109]	? [112]	? [116]	? [116]	? [116]	[126]	? [116]	? [130]	? [102]	? [116]	? [116]	? [116]	[68]	?
Interface, supported platforms, source code and version/date tested
Web interface					½ [110]
Supports offline use		[27]			½ [30]				[27]				½ [51]	[27]		[69]
Executable or web interface supplied (does not require compilation before use)					½ [30]	[113]	[113]	[114]	[113]	[113]	[113]		[111]			½ [110]														[132]
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				[here]	[here] [106]	[here]	[here]	[28]	[29]	[29]	[here] [35]	[29]	[here] [51]	[29]		[here]							[here]	[here]	[here]	[here]	[here]					[here]				[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

• [1] The author informs me that whilst this logic is not provided predefined for LoTREC, it is possible to construct it as a user-defined logic, however neither he nor I attempted to do so.
• [2] Through the appropriate toggles of reflexivity, transitivity, symmetry and extendability/seriality, as listed here.
• [3] A hotlink is provided in the interface for an infix editor, but clicking on it had no effect for me. The author informs me that infix syntax is supported in the latest beta version of LoTREC, however he has forgotten to upload the file itself to that page, and hopes that he will do so soon.
• [4] Nominally, MOLTAP supports this. Unfortunately, when I copied most of the Unicode characters across from the (unavailable at last check) syntax reference page [web.archive.org copy], the parser spat out errors. In particular, this occurred for the characters ⊤, ⊥, ∨, →, ←, ↔ and ↮. The only character that worked was conjunction, ∧.
• [5] But only for "true", "false", "not", "and", "or" and "implies". Implication written the other way around, logical equivalence, logical inequivalence and modal operators not included.
• [6] But sometimes seems to fail, and does not allow paste for formulas with invalid characters.
• [7] A single letter, uppercase for propositions/predicates, lowercase for constants/variables, optionally appended by any number of digits. Constants and variables use different letters, from different sets depending on whether Tarski's world syntax is enabled.
• [8] A single letter optionally appended by any number of digits.
• [9] 26 proposition/predicate identifiers (A-Z) and 26 constant/variable identifiers (a-z).
• [10] A lowercase letter optionally followed by any number of alphanumeric symbols.
• [11] An uppercase letter optionally followed by any number of letters in any case.
• [12] An uppercase letter optionally followed by any number of letters in any case.
• [13] Proposition/predicate identifiers are a single uppercase letter optionally followed by any number of letters or digits in any case. Constant identifiers are a single lowercase letter optionally followed by any number of letters or digits in any case. The 26 variable identifiers are lowercase a-z.
• [14] 26 proposition/predicate identifiers (A-Z) and 26 constant/variable identifiers (a-z). Constants and variables use different letters..
• [15] 5 proposition/predicate identifiers (P-T) and 5 variable identifiers (u, w, x, y, z).
• [16] But outputs the nodes as a list.
• [17] However, I had problems getting Tableau3 to accept many of the formulas that I input. For example, when I entered formula A↔B, using keypress F3 to generate the biimplication symbol, and then pressed Enter for the formula to be accepted, the status bar showed "The formula is not well formed. (check brackets)". Parenthesising the whole formula then resulted in the parse error "The formula is not well formed. (illegal characters)." I had no better luck when prepending a turnstile character, ⊦, by pressing F9.
• [18] Noting as in the previous footnote that the program would not accept most input I provided, so I could not test the drawing feature too well. In particular, I don't recall ever managing to get Tableau3 to draw a branching rule.
• [19] Provides a status dialogue with a cancellation button in case a branch becomes infinite. Unfortunately, at this point, ProofTools does not guarantee that non-infinite branches will (eventually) be terminated.
• [20] Because predicate logic is undecidable, infinite loops cannot be prevented, however, Tree Proof Generator allows an in-progress proof to be paused and resumed, so that infinite loops can be curtailed without killing the application.
• [21] However, in a sense it does - the sense that given that only a limited number of constants are available in the decomposition process, decomposition eventually stalls.
• [22] As best I can tell, infinite trees are not even possible in any of the logics Doug's software supports.
• [23] Infinite trees are not even possible in the logic Molle supports, modal K.
• [24] However, avoiding infinite loops in those defined logics in which they might occur requires the use of step-by-step solving.
• [25] Because the user decides when s/he wants to stop decomposing.
• [26] Because of my difficulties getting Tableau3 to accept input, I could not test this thoroughly.
• [27] At least by keeping the page open in a browser, and potentially by saving the page to a static file for offline use, but I didn't test this use case.
• [28] But here is asserted an intention to release source code in the future, and source code for the parsers is linked to (on GitHub).
• [29] At least, not that I could determine.
• [30] Executables and source code are provided. Unfortunately, I was unable to either run an executable or build the source code (on a Linux machine). The executable raised a console error, "error while loading shared libraries: libgmp.so.3: cannot open shared object file: No such file or directory", and I was not motivated to track down and install this earlier version of the library (I seem to have version 5 installed). I could not follow the build instructions either, because I could not find in the source tree the referenced file, build.sh.
• [31] An extended version of OOPS is also in development, with a working .jar file available at that link. Some of the ticked features in the comparison table refer to this extended version rather than the official release [3 March 2018 update: this page seems now to require authorisation to access].
• [32] Input is in the form of LUA scripts rather than straight-out formulas. A brief guide to the syntax can be found here [3 March 2018 update: this page seems now to require authorisation to access].
• [33] But this must be specified in the input LUA script. Instructions on how to do so can be found here [3 March 2018 update: this page seems now to require authorisation to access].
• [34] Based on the observation that under S5, calling th:provable() on the formula ~ %_1 #_1 %_1 b did not result in an infinite loop.
• [35] The code for the extended version is available in the "extensions" branch.
• [36] But only for modal logic, not for propositional logic.
• [37] The widget supports "S5Alt" - I am not sure whether this is the same as S5E.
• [38] Neither the author nor I are quite clear on what exactly this logic, supported by the extended version of OOPS, is. It is possible, though, that LoTREC supports it either out-of-the-box by a different name, or through the user-defining process.
• [40] With the exception of symmetry. See MOLTAP's syntax reference page [web.archive.org copy].
• [41] But what is this logic? Google doesn't seem to know, and I sure don't.
• [42] The user interface and manual/instructions for タブ朗 are almost entirely in Japanese, so it is somewhat challenging for non-Japanese-speaking English speakers to use and navigate.
• [43] Whilst the author has not confirmed this to me, it appears that whilst this logic is not provided predefined for LoTREC, it is possible to construct it as a user-defined logic, however I have not attempted to do so.
• [44] LoTREC does not display an all-in-one proof tree for the entire proof. Instead, it displays an overview of all of the branches of the complete proof tree as "Tableau Tree" in the "Premodels List" pane. Below that overview tree in that pane are then listed each of the terminating branches of the tree. Clicking on one of those branches will display the branch as a relational world diagram for modal logics, or just as a propositional branch diagram for propositional logic. This diagram will be similar although not identical to a model and/or counter-model, depending on whether the branch is closed or open respectively.
• [45] Through the system S syntax on the MOLTAP syntax reference page [web.archive.org copy].
• [46] See Wikipedia's "Common knowledge (logic)" article.
• [47] A letter in any case optionally followed by any number of alphanumeric characters in any case.
• [48] A lowercase letter optionally followed by any number of digits.
• [49] But outputs the number of rule applications required to determine the result.
• [50] Based on the observation that the formula <>[]<>p did not result in an infinite loop in the modal logic with the most accessibility relations.
• [51] However, I was unable to compile and test offline usage of the TWB source code - the build system complained about being unable to find OCaml libraries, even though I had installed them through my (Linux Fedora) system's package manager. That build output is listed here.
• [53] But only up to ternary predicates.
• [54] 6 unary predicate identifiers (C, T, P, H, M, S), 7 binary predicate identifiers (=, R, L, V, W, <, >), 1 ternary predicate identifier (I), six constant identifiers (a, b, c, d, e, f) and 6 variable identifiers (x, y, z, u, v, w).
• [55] タブ朗 outputs trees in a tabular format, where the (rectangular) child nodes of a (rectangular) parent node are drawn immediately below the parent node in the table, and take up, combined, the same width as the parent node. I have evaluated this as ½ only because it is not a traditional tree format where nodes are connected by lines.
• [56] At least, not that I could see, but as a non-Japanese speaker, my ability to understand the user interface of タブ朗 is limited, so I may simply have missed this feature.
• [57] But not through unadorned propositional constants; propositional constants must be simulated via unary predicates ranging over a constant, so that, e.g. the (invalid) propositional inference (C→T)→(T→C) is simulated in タブ朗 as (Ca→Ta)→(Ta→Ca).
• [58] The equality operator is entered as for any other predicate i.e. the two variables/constants over which it ranges are entered after it rather than on either side of it as is typical.
• [59] Whilst KLMLean itself is free, it has a runtime requirement, the Prolog compiler SICStus, which is not free (although it can be evaluated for free for a limited time). Initially, I had trouble running KLMLean, but with the author's help got it to work, as described here.
• [60] For negation ("neg"), conjunction ("and") and disjunction ("or"). Implication and conditional can only be entered as -> and => respectively.
• [61] In the words of the author: "Loops are possible in general, but KLMLean implements sound and complete restrictions ensuring termination. Then, it implements a decision procedure for all KLM logics".
• [62] With the unfortunate caveat that entry of certain types of invalid syntax causes KLMLean to hang, requiring a forced quit and restart. An example of input that causes such a freeze is the formula "A and B" (invalid syntax because capital letters are invalid - propositions must start with a lowercase letter).
• [63] In the words of the author: "all KLM logics are extensions of classica[l] logic. Therefore, if you do not use conditional formulas (with =>), you have a prover for propositional classical logic".
• [65] "Free as in beer" i.e. financially free, although many of the programs listed are also "free as in freedom" i.e. open source software.
• [66] Be warned that LogikKriger currently suffers from at least two serious bugs, one of which leads to nodes sometimes being added only to the first of two branches to which they ought to be added, and the other of which leads to nodes sometimes being drawn overlapping one another. Its author is aware of these bugs, and is open to contributions of fixes. Also, When checked on 3 March 2018, the site's homepage was unavailable, and I could not find to where, if anywhere, the project's website has been moved (its GitHub repository remains accessible). The most recent valid web.archive.org copy of the homepage is here.
• [67] LogikKriger does not seem to actually implement operator precedence, however, and seems to simply implement association from right to left when parsing unparenthesised expressions.
• [68] Infinite trees are not even possible in propositional logic, which is the only logic that this tool supports.
• [69] By keeping the page open in a browser after going offline, or by copying LogikKriger's source code to your local machine and accessing it locally in your web browser.
• [70] As noted under "Known problems" on the MOLTAP homepage, "The common knowledge operator can lead to infinite loops".
• [71] Although, as noted under "Known problems" on the MOLTAP homepage, "Common knowledge is not implemented correctly (there is no rule for K*φ+)".
• [72] The logic that ALCI Prover supports, description logic ALC, is not strictly a modal logic, but syntactically is a variant of K.
• [73] ALCI Prover is a console application, so its support for copy and paste depends on support in the terminal within which it is run. Cut isn't supported.
• [74] Identifiers may contain any of the characters A-Z, a-z, 0-9, _, ', but may not start with a number.
• [75] SoftOption offer three separate pieces of proof tree software, but each of them has the same feature-set in terms of this comparison, so I list them together here. They are: a Javascript Tree Widget, a Java Tree Widget (deprecated) and a standalone Java application, Deriver (run it with e.g. "java -jar Deriver.jar"). They also offer a documentation page.
• [76] The first date is for the Javascript widget, and the second is for the Java widget and standalone app.
• [78] I'm not sure whether infinite loops are even possible in the primary logic that TTM supports: propositional linear temporal logic (PLTL).
• [79] Saga implements the guarded fragment of predicate logic (see below), including identity.
• [80] Formulas are input into Saga by loading the Saga code within a Lisp interpreter and then calling the construct-tableau function on the desired formula. That formula is specified as Lisp syntax i.e. it is in Polish notation. Any cut/copy/paste functionality is dependent on your Lisp environment.
• [81] Saga proposition/predicate/variable identifiers seem to have the same (lack of) restrictions as any other Common Lisp variable identifier.
• [82] The Saga homepage explains that if a counter-model is found, it is returned. Based on my testing, something is indeed returned, but it was unclear to me how it could be interpreted as a counter-model. No doubt the author could explain, however I have chosen not to bother him.
• [83] To the best of my understanding, infinite loops are not possible in the logic Saga implements: the guarded fragment of predicate logic.
• [84] All platforms on which a Common Lisp implementation runs, which seem to be pretty comprehensive.
• [85] Note though that Saga implements neither a material conditional (implication) operator (→) nor a biimplication operator (↔), so these must be simulated using conjunction, disjunction and negation.
• [86] Cut/copy/paste supported in the web app; the commandline version's support for copy/paste (at least under Linux) depends on your terminal, and it would seem that cut isn't supported.
• [87] A lowercase letter optionally followed by any number of lowercase letters and/or digits.
• [88] But outputs "Pre-tableau" and "Tableau" lists.
• [89] Yes in the web app; no in the commandline version.
• [90] Being unfamiliar with ATL, I cannot say whether the output "Pre-tableau" and "Tableau" lists can be read as counter-models.
• [91] Being unfamiliar with ATL, I am not even sure whether infinite loops are possible in its tableaux.
• [92] "All" for the web app; "Linux" for the commandline version.
• [93] The first date is that documented for the commandline client; the second date is that on which the (unversioned/undated) web app was tested
• [94] Tableaux for ATL can be accessed as a web app, or downloaded and used as a commandline Linux app.
• [95] Sibyl takes its input from a file (supplied as an argument to Sibyl via the commandline), whose format is described in the Sibyl User Guide. Formulas are specified with infix syntax. Any cut, copy and paste functionality depends on the editor you use to edit the input file.
• [96] Per the Sibyl User Guide (almost word-for-word), a propositional identifier begins with an uppercase letter; a nominal begins with either a lowercase letter or a numeric character; variable and relation identifiers begin with any alphanumeric character. The only other restriction is that no identifier may contain any keyword (i.e. begin, end, Transitive, Inclusions, true, false, binder, All, Some).
• [97] As a commandline program, Sibyl does not output graphical trees, however it can be supplied with an option (-tex or -texn) to generate a LaTeX file. This LaTeX file, when rendered, lists all branches up to the first open one, if any. It does not show a tree as such - each branches is itself a simple list, and branches in their entirety are listed one after the other. The logic symbols in the rendered LaTeX are "actual" symbols rather than shortcuts. The first open branch, if any, can be taken as a "sort of" counter-model.
• [98] From the Sibyl homepage: Sibyl is "based on a tableau calculus that is provably terminating and complete, provided that the negation normal form of the formulae given in input do not contain any occurrence of the binder that is both in the scope and contains in its scope a universal operator". It is not clear to me whether infinite loops are possible in Sibyl for formulae that do not meet this provision.
• [99] Formulas are entered in pdl-tableau in Polish notation with operands enclosed in parentheses, and each operator being a natural word rather than a symbol. An example - unsatisfiable i.e. for which the tableau closes - is not(implies(and(implies(a,b),implies(b,c)),implies(a,c))).
• [100] A lowercase letter optionally followed by any number of alphanumeric letters in any case.
• [101] But outputs the tree textually as a sequence of nodes, one per line, with branching indicated by indentation.
• [102] Being unfamiliar with PDL, I do not know whether infinite loops are even possible in its tableaux.
• [103] Sadly, this link seems now to be dead, and I have not been able to find TABLEAUX anywhere else on the web.
• [104] When checked on 27 March 2015, this site seemed to be unavailable, and the web server at the parent domain dougowings.net was displaying a default Apache page.
• [105] When checked on 3 March 2018, this site was unavailable, and I could not find to where, if anywhere, the project's website has been moved. The most recent valid web.archive.org copy is here.
• [106] As per the previous footnote, this site was unavailable at last check, however, it appears that Moltap's source code has been uploaded to GitHub by a friend of the original author.
• [107] When checked on 3 March 2018, this site was unavailable, and I could not find to where, if anywhere, the project's website has been moved. The most recent valid web.archive.org copy is here.
• [108] CPDL Tableau Prover is a console application, so its support for copy and paste depends on support in the terminal within which it is run. Cut isn't supported.
• [109] Being unfamiliar with CPDL, I do not know whether infinite loops are even possible in its tableaux.
• [110] A web interface was originally provided, however, since at least 3 March 2018 the project website has been unavailable, and since it is dynamic, the archive.org copy of the web interface does not work.
• [111] The web interface is provided, however the executable is not, and I could not compile it from source (see footnote 51).
• [112] Being unfamiliar with CTL, I do not know whether infinite loops are even possible in its tableaux.
• [113] But requires the Java Runtime Environment to be installed.
• [114] But the standalone application requires the Java Runtime Environment to be installed.
• [115] COOL is a console application, so its support for copy and paste depends on support in the terminal within which it is run. Cut isn't supported.
• [116] Being unfamiliar with the supported logics, I do not know whether infinite loops are even possible in their tableaux.
• [117] Built from commit 433c8a2ebf5c1f5b6eda44ee293f37f6bb47524e, as supplied by the developer here.
• [118] COOL's supported logics can be combined in these ways, as described on its homepage:
  • Choice A + B: Any world in the model can either have successors according to logic A or to logic B.
  • Fusion A * B: Any world in the model has both successors according to logic A and to B.
  • Sequence A . B: Any wolrd in the model has successors reachable by doing an A-step and then an B-step. (e.g. simple Segala systems which perform an nondeterministic step followed by an probabilistic step).
• [119] At least, I could not see a way to supply propositional logic formulas and arguments to it.
• [120] Supports only XML input files, so copy and paste functionality is deferred to whichever editor you use to edit your XML files, and identifiers are unlimited per XML constraints.
• [121] (A quote from its web page:) Konclude can handle all of the Web Ontology Language (OWL 2) with almost all datatypes. In addition, Konclude supports nominal schemas which allow for expressing arbitrary DL-safe rules simply by using given ontology syntax extended with variables.
• [122] FaCT++ takes its input from a file (supplied as an argument via the commandline). Formulas are specified in Lisp syntax (Polish notation). Any cut, copy and paste functionality depends on the editor you use to edit the input file.
• [123] Formulas are input into Gost by loading the Gost code within a Lisp interpreter and then calling the solve function on the desired formula. That formula is specified as Lisp syntax i.e. it is in Polish notation. Any cut/copy/paste functionality is dependent on your Lisp environment.
• [124] Gost proposition/predicate/variable identifiers seem to have the same (lack of) restrictions as any other Common Lisp variable identifier.
• [125] Gost returns something when a formula is satisfiable, and its author informs me that this is a counter-model, although I have not concentrated hard enough to be able to interpret it as such. No doubt, this is due simply to lack of effort on my part.
• [126] To the best of my understanding, infinite loops are not possible in the logic Gost implements: the guarded fragment of predicate logic.
• [127] LCKS5 is a console application, so its support for copy and paste depends on support in the terminal within which it is run. Cut isn't supported.
• [128] MLTP takes its input from a file (supplied as an argument via the commandline). Formulas are specified in Polish notation. Any cut, copy and paste functionality depends on the editor you use to edit the input file.
• [129] It seems that (though this is from observation and empirical testing only) identifiers may contain any of the characters A-Z, a-z, 0-9, _, comma,but may not start with a number.
• [130] At this point, I have forgotten whether infinite loops are even possible in the tableaux for modal logic K, which is the only modal logic supported by MLTP.
• [131] But outputs a textual list of tree nodes when the -oindented parameter is supplied.
• [132] But only for Linux.
• [133] This tool is a console application, so its support for copy and paste depends on support in the terminal within which it is run. Cut isn't supported.
• [134] Via the inclusion of curly braces, such as: {transitive: r}.
• [135] This tool is either a console application or a web app, so its support for copy and paste depends on support in the terminal or browser within which it is run. Cut probably isn't supported for the terminal, but may be in the browser for the web app.
• [136] From observation, it appears that an identifier must start with a capital letter, and then may be followed by any number of alphanumeric characters, plus _ and '.
• [137] Supports single-character identifiers, with a broad range, including alphanumeric characters and symbols.
• [138] Supports any sequence of characters which are either alphanumeric or underscore.

Other notable mentions

• MetTeL. Not quite a readymade proof tree software tool; instead, it is a generator of such tools. Like LoTREC, MetTeL allows the user to define a logic, for which it then generates a tableau prover. MetTel1 has been succeeded by MetTeL2. Implemented in Java, its source code is available on request, licensed under the GPL3. The provers it generates are console-based, so there is no output of graphical trees, nor much output at all beyond indicating whether a formula is satisfiable or unsatisfiable - on occasion, though, it outputs a counter-model or indicates where a contradiction was found. Conveniently, it has a web interface demo.
• Semantic Tableaux in Less than 90 Lines of Scala. As found on the void-main-args blog.

Unevaluated software

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

• Bertrand. Unevaluated because this program runs only on PowerPCs and on 680x0 Macs in native mode, and I have no access to such platforms. It does look very good though.
• CardS4. Unevaluated because it became too tedious to try to work out how to compile this Java smart card prover on a PC.
• CardTAP. Unevaluated because I suspected that as for CardS4 it would be too tedious to work out how to compile this Java smart card prover on a PC.
• DLP. [Dead link; link is to a Wayback Machine archival page]. Unevaluated because the source page is no longer accessible, and there appears to no longer be any way to access this software, which is described on its archival page as "an experimental description logic system, designed to investigate various options for checking satisfiability in expressive description logics and propositional modal logics".
• FaCT. Unevaluated because, other than the Java client, I could not get the supplied executables to run on my Linux system. Running the Lisp executables resulted in error messages such as this: dlopen(/path/on/my/system/to/CORBA-FaCT-linux/lisp/shiq-app/libacl612.so, mode) error: /path/on/my/system/to/CORBA-FaCT-linux/lisp/shiq-app/libacl612.so: symbol errno version GLIBC_2.0 not defined in file libc.so.6 with link time reference, which perhaps is not surprising given that, judging by the date at the bottom of the FaCT web page, these files date back to 2003. I was also unable to run the Lisp source code. Attempting to load the CORBA-FaCT-linux/sources/lisp/FaCT-system.cl file in the clisp implementation installed by my package manager (DNF on Fedora) resulted in the error message: ERROR This version of the FaCT and iFaCT system definition is only meant to work with Allegro Common Lisp. Allegro Common Lisp appears to be a commercial software package, and I do not have access to it. In any case, FaCT has been superceded by FaCT++, which is now in the comparison table above.
• ileanTAP. I was unable to get this intuitionistic theorem prover to compile and run under either of the free Prolog compilers by SWI and by GNU. I emailed the author for help at the address given on the program's homepage but have not as yet heard back.
• KtSeqC. Unevaluated because although I was able to build and run this theorem prover for the minimal tense logic Kt, it was aborted with system error messages about memory corruption when I ran it on the examples in the provided "test" directory. I have been in touch with the maintainers of the software, and they are aware of the problem, but have not yet gotten back to me with an analysis/fix.
• leanTAP. As for ileanTAP, I was unable to get this theorem prover for first-order logic to compile and run under either of the free Prolog compilers by SWI and by GNU.
• linTAP. As for ileanTAP and leanTAP, I was unable to get this tableau prover for linear logic to run under either of the free Prolog compilers by SWI and by GNU.
• lolo. The build process resulted in a couple of compilation errors - "Could not find module ‘Data.Generics.Basics’" and "Could not find module ‘Data.Generics.Instances’", and because I am not experienced with the Glasgow Haskell Compiler, I did not attempt to resolve them.
• MleanTAP. Based on my struggles with getting ileanTAP, leanTAP, and linTAP to run, I did not even attempt to try to run this closely related software tool.
• ModLeanTAP. As for ileanTAP, leanTAP, and linTAP, I was unable to get this lean tableau-based deduction prover for propositional modal logics to run under either of the free Prolog compilers by SWI and by GNU (it was designed for the non-free SICStus Prolog compiler).
• Racer. This software looks very impressive, but I was unable to work out how to run it (under Common Lisp). It all seems a bit complicated and daunting to the neophyte, and I would probably need some sort of tutorial to get it working. Here, in any case, are some details about this interesting tool: The successor of the former commercial software known as RacerPro. It is now available under an open licence. It is described as "a knowledge representation system that implements a highly optimized tableau calculus for the description logic SRIQ(D)". The archived homepage for RacerPro described it as tableau software for "a very expressive description logic. It offers reasoning services for multiple T-boxes and for multiple A-boxes as well. The system implements the description logic ALCQHI_R+ also known as SHIQ. This is the basic logic ALC augmented with qualifying number restrictions, role hierarchies, inverse roles, and transitive roles". RacerPro was also described as a "Semantic Web Reasoning System and Information Repository" and "a Combination of Description Logic and Specific Relational Algebras".
• Socrates. [No longer available at last check; link is to the last valid web.archive.org copy]. Unevaluated because whilst I eventually got this program to run on both Windows XP and Windows 7 (in both cases after downloading a few missing DLLs), I could not get its font to display correctly, so that all I could see was gibberish. This problem wasn't solved by installing the Terlingua font as recommended here [web.archive.org copy] - Socrates did not seem to even acknowledge the existence of this new font, let alone use it.
• Semantic Tableaux Solver For Propositional Logic. Unevaluated not because it is non-free ($0.99 is a very reasonable price) but because it only runs on iOS, and I have no access to any devices running that platform.
• The Logics Workbench (LWB). Unevaluated because by the time I went to evaluate it, on 2 September 2019, The Logics Workbench was no longer available at the online location I had for it (this link is to a Wayback Machine archive), and I have been unable to determine to where, if anywhere, it has moved.
• The Tableau Machine. [No longer available at last check; link is to the last valid web.archive.org copy]. Unevaluated because formulas including most operators that I tried (the pattern seems to be: those which cause a branch to split) resulted upon clicking "Construct Tableau" in the error message: Fatal error: Cannot use object of type stdClass as array in /home/ctemple/tm/includes/functions.php on line 198.
• The tableaux package. A Haskell project. I downloaded it and attempted to install it with cabal, except that whereas cabal told me Encountered missing dependencies: QuickCheck >=2.1, cgi >=3001.1, html >=1.0, my package manager, dnf, told me, after running the command sudo dnf install -y ghc-QuickCheck ghc-html (what was required to satisfy the "cgi >=3001.1" component I don't know): Package ghc-QuickCheck-2.10.1-4.fc29.x86_64 is already installed. Package ghc-html-1.0.1.2-40.fc29.x86_64 is already installed. Dependencies resolved. Nothing to do. Complete! . I am not experienced enough with cabal/Haskell to be motivated to investigate further.
• Twootie and Twoocon. Twootie would not run under Windows XP, and I have no access to earlier versions of Windows. I could not compile Twoocon due to lack of access to the Kylix compiler.

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.

Page	Of organisation/group/entity	Maintained by	Notes
AiML: Tools	Advances in Modal Logic (AiML)	Renate Schmidt	The source of many (most?) of the tools currently in this page's listing.
OWL/Implementations	W3C	The community (wiki-based)	Part of the W3C's Semantic Web project/vision.
List of reasoners	OWL @ Manchester	Uli Sattler and Nico Matentzoglu	Only reasoners for description logic are listed.
Software	Chair of Automata Theory of the Institute of Theoretical Computer Science of Technische Universitat Dresden	Francesco Kriegel	This seems to be the group's own software.
Software	Logic 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.