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


Autoria(s): Degtyarev, Anatoli; Fisher, Michael; Konev, Boris
Data(s)

2002

Resumo

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.

Formato

application/pdf

Identificador

http://calcium.dcs.kcl.ac.uk/886/1/tableaux02.pdf

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.

Publicador

Springer

Relação

http://calcium.dcs.kcl.ac.uk/886/

Tipo

Conference or Workshop Item

PeerReviewed