A clausal resolution method for propositional linear temporal logic is presented. The method, originally proposed by Fisher in 1991 [1], is clausal. It works on formulas transformed to a normal form called separated normal form (SNF), proposed by Fisher in 1992. The authors prove that the complexity of the transformation to SNF is both linear in the number of new propositional symbols introduced and linear in the number of new clauses introduced. Once a formula has been translated into SNF, both step resolution and temporal resolution operations can be applied. Step resolution effectively consists of the application of the standard classical resolution rule together with simplification rules, subsumption rules, and some other rules. The temporal resolution operation effectively resolves together formulas containing the and connectives. The general temporal resolution operation, written as an inference rule, becomes where denotes the Unless operator. It should be stressed that A. Degtiarev and Fisher, by using a union of derivations, for some class of formulas present weak temporal resolution which does not introduce the operator Unless [2].

I think (it is only my hypothesis) that weak temporal resolution is the general case. Fisher has shown that if there is only one eventuality, that is, only one sometime clause, general temporal resolution can be replaced by a weak temporal resolution rule. The completeness and termination of the proposed method are proven. The naive algorithm is presented, and the authors prove that the complexity of applying the resolution rule is of order , where and are some parameters.

Some examples demonstrating the proposed method are presented, and related work is considered. It should be stressed that this method has extensions to branching temporal logic, fixpoint temporal logic, and some decidable fragments of linear first-order temporal logic.