School of Computing

A Tableau Method for Interval Temporal Logic

Howard Bowman and Simon Thompson

Technical Report 12-97, Computing Laboratory, University of Kent, November 1997.

Abstract

In this paper we present a complete tableau method for interval temporal logic including the projection operator. Central to our strategy is the identification of normal forms for all the operators of our logic. In effect, these normal forms give inductive definitions of the ITL operators. Then, in the style of Wolper, we define a tableau decision procedure to check satisfiability of our logic. For simplicity of presentation we work in the propositional setting.

Download publication 272 kbytes (PostScript)

Bibtex Record

@techreport{461,
author = {Howard Bowman and Simon Thompson},
title = {{A} {T}ableau {M}ethod for {I}nterval {T}emporal {L}ogic},
month = {November},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/461},
    institution = {Computing Laboratory, University of Kent},
    number = {12-97},
    type = {Technical Report},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014