Computing Publications

Publications Home » A Minimal Hybrid Logic for Intervals

A Minimal Hybrid Logic for Intervals

Altaf Hussain

Journal Article
Journal of the IGPL
Volume 14
pp.35–62
2006
Oxford University Press
Abstract

Taking our inspiration from van Benthem's treatment of temporal interval structures, and Halpern and Shoham's work on intervals, we introduce an interval hybrid temporal logic with two binary relations, precedence and inclusion, for talking about interval temporal structures. This paper can be seen as an continuation of the work began in an earlier paper, in which we undertook a purely modal treatment of interval temporal structures. By introducing an interval hybrid temporal logic, we enrich the logic with nominals, and thereby increase the expressivity of the logic. We study the interval hybrid temporal logic in its full generality and identify two important classes of interval temporal structures: the class of minimal interval structures, and the class of van Benthem minimal interval structures. We present sound and complete tableau calculi for both classes of structures. We prove that the logic of minimal interval structures is decidable, by developing a novel bulldozing technique that handles both the presence of nominals and the interaction between the two relations. We go on to show that the satisfiability problem is EXPTIME-complete. We conclude the paper with the remark that the decidability (or otherwise) and complexity of the logic of van Benthem minimal interval structures remains an interesting open problem

Key Words: tableau method, interval logics, hybrid logic, bulldozing

PDF of full publication (291 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.