Abstract
Although there exist several decidable fragments of Halpern and Shoham’s interval temporal logic HS, the computational complexity of their satisfiability problem tend to be generally high. Recently, the fragment HS3 of HS, based on coarser-than-Allen’s relations, has been introduced, and it has been proven to be not only decidable, but also relatively efficient. In this paper we describe an implementation of a tableau-based satisfiability checker for HS3 interpreted in the class of all finite linear orders.
Citation
Please, cite this work as:
[MSS17] E. Mu~noz-Velasco, G. Sciavicco, and I. E. Stan. “Implementation of a Tableau-based Satisfiability Checker for HS3”. In: Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking (2017 IEEE M&N), Naples, Italy, September 26-28, 2017. Ed. by D. D. Monica, A. Murano, S. Rubin and L. Sauro. Vol. 1949. CEUR Workshop Proceedings. CEUR-WS.org, 2017, pp. 326-340. URL: https://ceur-ws.org/Vol-1949/CILCpaper09.pdf.
@InProceedings{MunozVelasco2017,
author = {Emilio Mu~noz-Velasco and Guido Sciavicco and Ionel Eduard Stan},
booktitle = {Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 {IEEE} International Workshop on Measurements and Networking {(2017} {IEEE} M{&}N), Naples, Italy, September 26-28, 2017},
title = {Implementation of a Tableau-based Satisfiability Checker for {HS3}},
year = {2017},
editor = {Dario Della Monica and Aniello Murano and Sasha Rubin and Luigi Sauro},
pages = {326–340},
publisher = {CEUR-WS.org},
series = {{CEUR} Workshop Proceedings},
volume = {1949},
abstract = {Although there exist several decidable fragments of Halpern and Shoham’s interval temporal logic HS, the computational complexity of their satisfiability problem tend to be generally high. Recently, the fragment HS3 of HS, based on coarser-than-Allen’s relations, has been introduced, and it has been proven to be not only decidable, but also relatively efficient. In this paper we describe an implementation of a tableau-based satisfiability checker for HS3 interpreted in the class of all finite linear orders.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/ictcs/Munoz-VelascoSS17.bib},
timestamp = {Fri, 10 Mar 2023 16:23:17 +0100},
url = {https://ceur-ws.org/Vol-1949/CILCpaper09.pdf},
}