A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic

The clausal resolution method for propositional linear-time temporal logic 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 resolutioin method can be defined for this impoprtant variety of logics.

Equality and Monodic First-Order Temporal Logic

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.