zbMATH — the first resource for mathematics

A new one-pass tableau calculus for PLTL. (English) Zbl 0903.03015
de Swart, Harrie (ed.), Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX ’98, Oisterwijk, the Netherlands, May 5–8, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1397, 277-290 (1998).
Summary: The paper presents a one-pass tableau calculus \(\text{PLTL}_T\) for propositional linear time logic PLTL. The calculus is correct and complete and, unlike in previous decision methods, there is no second phase that checks for the fulfillment of the so-called eventuality formulae. This second phase is performed locally and is incorporated into the rules of the calculus. Derivations in \(\text{PLTL}_T\) are cyclic trees rather than cyclic graphs. When used as a basis for a decision procedure, it has the advantage that only one branch needs to be kept in memory at any time. It may thus be a suitable starting point for the development of a parallel decision method for PLTL.
For the entire collection see [Zbl 0888.00018].

03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
PDF BibTeX Cite