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
Implementation of a Tableau-Based Satisfiability Checker for HS3
Stan, Ionel Eduard;SCIAVICCO, Guido
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 ordersFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
