Connection Based Strategies for Deciding Propositional Temporal Logic

Abstract

Connection methods have proven their value for efficient automated theorem proving in classical logics. However, these methods have not been extended to temporal logics due to the lack of a subformula property in existing proof procedures. We show that a slightly looser generalized subformula property exists for temporal logics. We then exploit this generalized subformula property to develop a temporal notion of polarities and connections, upon which we base an efficient proof procedure for propositional temporal logic. The proof procedure is structured around semantic tableau augmented with connections, and we propose a number of connection-based strategies. The procedure achieves many of the benefits of connection methods. The method is also sufficiently general to be extensible to other temporal logics. Experimental results indicate substantial speedup resulting from this approach.