The study of interval temporal logics on linear orders is a meaningful research area in computer science and artificial intelligence. Unfortunately, even when restricted to propositional languages, most interval logics turn out to be undecidable. Decidability has been usually recovered by imposing severe syntactic and/or semantic restrictions. In the last years, tableau-based decision procedures have been obtained for logics of the temporal neighborhood and logics of the subinterval relation over specific classes of temporal structures. In this paper, we develop an optimal NEXPTIME tableau-based decision procedure for the future fragment of Propositional Neighborhood Logic over the whole class of linearly ordered domains.
Optimal tableaux for Right Propositional Neighborhood Logic over Linear Orders / D. Bresolin; A. Montanari; P. Sala; G. Sciavicco. - STAMPA. - 5293:(2008), pp. 62-75. (Intervento presentato al convegno JELIA 2008: 11th European Conference on Logics in Artificial Intelligence tenutosi a Dresda, Germania nel Settembre-Ottobre 2008) [10.1007/978-3-540-87803-2_7].
Optimal tableaux for Right Propositional Neighborhood Logic over Linear Orders
BRESOLIN, DAVIDE;
2008
Abstract
The study of interval temporal logics on linear orders is a meaningful research area in computer science and artificial intelligence. Unfortunately, even when restricted to propositional languages, most interval logics turn out to be undecidable. Decidability has been usually recovered by imposing severe syntactic and/or semantic restrictions. In the last years, tableau-based decision procedures have been obtained for logics of the temporal neighborhood and logics of the subinterval relation over specific classes of temporal structures. In this paper, we develop an optimal NEXPTIME tableau-based decision procedure for the future fragment of Propositional Neighborhood Logic over the whole class of linearly ordered domains.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
