×

zbMATH — the first resource for mathematics

A simplified clausal resolution procedure for propositional linear-time temporal logic. (English) Zbl 1015.03015
Egly, Uwe (ed.) et al., Automated reasoning with analytic tableaux and related methods. 11th international conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 - August 1, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2381, 85-99 (2002).
Summary: The clausal resolution method for propositional linear-time temporal logics is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. In this paper, we show how the normal form can be radically simplified and, consequently, how a simplified clausal resolution method can be defined for this important variety of logic.
For the entire collection see [Zbl 0993.00044].

MSC:
03B35 Mechanization of proofs and logical operations
03B44 Temporal logic
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
SPIN
PDF BibTeX XML Cite
Full Text: Link