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.
|Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Thursday, 15-Aug-2013 20:34:27 BST © 1998-2004 by Ullrich Hustadt.|