Home // COMPUTATION TOOLS 2014, The Fifth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

First Steps towards Automated Synthesis of Tableau Systems for Interval Temporal Logics

Authors:
Dario Della Monica
Angelo Montanari
Guido Sciavicco
Dmitry Tishkovsky

Keywords: Interval temporal logics; satisfiability; tableau systems; automated tableau system generation

Abstract:
Interval temporal logics are difficult to deal with in many respects. In the last years, various meaningful fragments of Halpern and Shoham's modal logic of time intervals have been shown to be decidable with complexities that range from NP-complete to non-primitive recursive. However, even restricting the attention to finite interval structures, the step from model-theoretic decidability results to the actual implementations of tableau-based decision procedures is quite challenging. In this paper, we investigate the possibility of making use of automated tableau generators. More precisely, we exploit the generator MetTel2 to implement a tableau-based decision procedure for the future fragment of the logic of temporal neighborhood over finite linear orders. We explore and contrast two alternative solutions: a concrete tableau system, that operates on a concrete interval structure explicitly built over a finite, linearly-ordered set of points, and an abstract one, that operates on an interval frame which is forced to be isomorphic to a concrete interval structure by suitably constraining its accessibility relation.

Pages: 32 to 37

Copyright: Copyright (c) IARIA, 2014

Publication date: May 25, 2014

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-344-5

Location: Venice, Italy

Dates: from May 25, 2014 to May 29, 2014