Menu_Home Home   Menu_Latest Latest   Menu_Search Advanced Search   Menu_Browse_by_Year By Year   Menu_Browse_by_Division By Division
  
Screen decoration graphicsLogo

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.

[img]PDF - Repository staff only - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
169Kb

Abstract

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.

Item Type:Conference or Workshop Item (Paper)
Subjects:UNSPECIFIED
ID Code:886
Deposited By:Dr Anatoli Degtyarev
Deposited On:08 Nov 2007 08:33
Last Modified:08 Nov 2007 08:33

Repository Staff Only: item control page