A resolution method for temporal logic

Abstract

In this paper, a resolution method for propositional temporal logic is presented. Temporal formulae, incorporating both past-time and future-time temporal operators, are converted to Separated Normal Form (SNF), then both non-temporal and temporal resolution rules are applied. The resolution method is based on classical resolution, but incorporates a temporal resolution rule that can be implemented efficiently using a graph-theoretic approach. 1 Introduction This report describes a resolution procedure for discrete, linear, propositional temporal logic. This logic incorporates both past-time and future-time temporal operators and its models consist of sequences of states, each sequence having finite past and infinite future. A naive application of the classical resolution rule to temporal logics fails as two complementary literals may not represent a contradictory formula, depending on their temporal context. Because of such problems with resolution, the majority of the decision meth...