Skip to main content

A Tableau Method for Interval Temporal Logic

Bowman, Howard and Thompson, Simon (1997) A Tableau Method for Interval Temporal Logic. Technical report. University of Kent at Canterbury (KAR id:21432)

Postscript
Language: English
Download (278kB) Preview
[thumbnail of A_Tableau_Method_for_Interval_Temporal_Logic.ps]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF
Language: English
Download (62kB) Preview
[thumbnail of A_Tableau_Method_for_Interval_Temporal_Logic.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format

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.

Item Type: Monograph (Technical report)
Uncontrolled keywords: tableau interval temporal logic normal form
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 02 Aug 2009 20:20 UTC
Last Modified: 16 Feb 2021 12:31 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21432 (The current URI for this page, for reference purposes)
Bowman, Howard: https://orcid.org/0000-0003-4736-1869
Thompson, Simon: https://orcid.org/0000-0002-2350-301X
  • Depositors only (login required):

Downloads

Downloads per month over past year