Method of analytic tableaux

The assumption that free variables are universally quantified is what makes the application of a most general unifier a sound rule: since ${\displaystyle \gamma (x')}$ means that ${\displaystyle \gamma }$ is true for every possible value of ${\displaystyle x'}$, then ${\displaystyle \gamma (t)}$ is true for the term ${\displaystyle t}$ that the most general unifier replaces ${\displaystyle x}$ with.

Free variables in a tableau are rigid: all occurrences of the same variable have to be replaced all with the same term. Every variable can be considered a symbol representing a term that is yet to be decided. This is a consequence of free variables being assumed universally quantified over the whole formula represented by the tableau: if the same variable occurs free in two different nodes, both occurrences are in the scope of the same quantifier. As an example, if the formulae in two nodes are ${\displaystyle A(x)}$ and ${\displaystyle B(x)}$, where ${\displaystyle x}$ is free in both, the formula represented by the tableau is something in the form ${\displaystyle \forall x.(...A(x)...B(x)...)}$. This formula implies that ${\displaystyle (...A(x)...B(x)...)}$ is true for any value of ${\displaystyle x}$, but does not in general imply ${\displaystyle (...A(t)...A(t')...)}$ for two different terms ${\displaystyle t}$ and ${\displaystyle t'}$, as these two terms may in general take different values. This means that ${\displaystyle x}$ cannot be replaced by two different terms in ${\displaystyle A(x)}$ and ${\displaystyle B(x)}$.

Free variables in a formula to check for validity are also considered universally quantified. However, these variables cannot be left free when building a tableau, because tableau rules works on the converse of the formula but still treats free variables as universally quantified. For example, ${\displaystyle P(x)\rightarrow P(c)}$ is not valid (it is not true in the model where ${\displaystyle D=\{1,2\},P(1)=\bot ,P(2)=\top ,c=1}$, and the interpretation where ${\displaystyle x=2}$). Consequently, ${\displaystyle \{P(x),\neg P(c)\}}$ is satisfiable (it is satisfied by the same model and interpretation). However, a closed tableau could be generated with ${\displaystyle P(x)}$ and ${\displaystyle \neg P(c)}$, and substituting ${\displaystyle x}$ with ${\displaystyle c}$ would generate a closure. A correct procedure is to first make universal quantifiers explicit, thus generating ${\displaystyle \forall x.(P(x)\rightarrow P(c))}$.

Resolution (logic)

(1955). "Semantic entailment and formal derivability". Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde. 18 (13): 309–42. Reprinted in Intikka, Jaakko, ed. (1969). The Philosophy of Mathematics. Oxford University Press. ISBN 978-0-19-875011-6.

Beth, Evert W.

Bostock, David (1997). . Oxford University Press. ISBN 978-0-19-156707-0.

Intermediate Logic

(1987). "Systematization of Finite Many-Valued Logics Through the Method of Tableaux". The Journal of Symbolic Logic. 52 (2): 473–493. doi:10.2307/2274395. JSTOR 2274395. S2CID 42822367.

Carnielli, Walter A.

(1991). "On sequents and tableaux for many-valued logics" (PDF). The Journal of Non-Classical Logics. 8 (1): 59–76. Archived from the original (PDF) on 2016-03-05. Retrieved 2014-10-11.

Carnielli, Walter A.

D'Agostino, M.; ; Haehnle, R.; Posegga, J., eds. (1999). Handbook of Tableau Methods. Kluwer. ISBN 978-94-017-1754-0.

Gabbay, D.

(1996) [1990]. First-order logic and automated theorem proving (2nd ed.). New York: Springer. doi:10.1007/978-1-4612-2360-3. ISBN 978-1-4612-7515-2. S2CID 10411039.

Fitting, Melvin

Girle, Rod (2014). (2nd ed.). Taylor & Francis. ISBN 978-1-317-49217-7.

Modal Logics and Philosophy

Goré, Rajeev. "Tableau Methods for Modal and Temporal Logics". . pp. 297–396.

Handbook of Tableau Methods

Hähnle, Reiner (2001). . In Robinson, Alan J.A.; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. Elsevier. pp. 101–179. ISBN 978-0-08-053279-0.

"3. Tableaux and Related Methods"

(11 October 2005) [1997]. Logic with trees: an introduction to symbolic logic. Routledge. ISBN 978-1-134-78550-6.

Howson, Colin

(2006) [1967]. Formal Logic: Its Scope and Limits (4th ed.). Hackett. ISBN 978-0-87220-813-1.

Jeffrey, Richard

Letz, Reinhold; Stenz, Gernot. "28. Model Elimination and Connection Tableau Procedures". . pp. 2015–2114.

Handbook of Automated Reasoning

(1995) [1968]. First Order-Logic. Dover. ISBN 978-0-486-68370-6.

Smullyan, Raymond

(2014). A Beginner's Guide to Mathematical Logic. Dover. ISBN 978-0486492377.

Smullyan, Raymond

The Encyclopedia of Philosophy, ed. (11 December 2023). . The Encyclopedia of Philosophy. Retrieved 26 December 2023.

"Modern Logic: The Boolean Period: Carroll"

Zeman, Joseph Jay (1973). . Clarendon Press. ISBN 978-0-19-824374-8. OCLC 641504.

Modal Logic: The Lewis-modal Systems

: an annual international conference on automated reasoning with analytic tableaux and related methods

TABLEAUX

: Journal of Automated Reasoning

JAR

: an interactive prover for propositional and first-order logic using tableaux

The tableaux package

: another interactive prover for propositional and first-order logic using tableaux

Tree proof generator

: a generic tableaux-based prover for modal logics from IRIT/Toulouse University

LoTREC

on YouTube

Intro to Truth Trees