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.
Muñoz-Velasco, E., Sciavicco, G., Stan, I. (2017). 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) (pp.326-340). CEUR-WS.
Implementation of a Tableau-Based Satisfiability Checker for HS3
Stan, IE
2017
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
Muñoz-Velasco-2017-CEUR Workshop Proceedings-VoR.pdf
Solo gestori archivio
Tipologia di allegato:
Publisher’s Version (Version of Record, VoR)
Licenza:
Tutti i diritti riservati
Dimensione
395.16 kB
Formato
Adobe PDF
|
395.16 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
