|Home Latest Advanced Search By Year By Division|
|Not Logged in. Login|
A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic
Degtyarev, Anatoli and Fisher, Michael and Konev, Boris (2002) A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. In: Automated Reasoning with Analytic Tableaux and Related Methods, International Conference.
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.
Repository Staff Only: item control page