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.

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

Accessibility | Terms and Conditions | Last Modified 01 November 2007