M. Ludwig and U. Hustadt (2009b)$ ``Resolution-Based Model Construction for PLTL.'' In C. Lutz and J.-F. Raskin, editors, Proceedings of the 16th International Symposium on Temporal Representation and Reasoning (TIME 2009) [Brixen-Bressanone, Italy, 23-25 July 2009], pp. 73-80. IEEE Computer Society.
Abstract, BibTeX, PDF.

With tableaux-based reasoning approaches or model checking techniques for propositional linear-time tem- poral logics, PLTL, it is easily possible to construct counter examples for formulae that are not valid. In contrast, only the information that a formula is satisfiable is usually avail- able in resolution-based inference systems. In this paper we present a resolution-based approach for constructing models for satisfiable PLTL formulae. Our approach is based on using the standard model construction for sets of propositional clauses saturated under ordered resolution in the different time points of a temporal model. The temporal model construction procedure is also designed in such a way that it can be easily implemented in existing theorem provers for PLTL.