caa a22 4500 463182790 CHVBK 20180406164844.0 cr unu---uuuuu 170326e20070401xx s 000 0 eng 10.1007/s10817-006-9051-0 doi (NATIONALLICENCE)springer-10.1007/s10817-006-9051-0 An Optimal Decision Procedure for Right Propositional Neighborhood Logic [Elektronische Daten] [Davide Bresolin, Angelo Montanari, Guido Sciavicco] Propositional interval temporal logics are quite expressive temporal logics that allow one to naturally express statements that refer to time intervals. Unfortunately, most such logics turn out to be (highly) undecidable. In order to get decidability, severe syntactic or semantic restrictions have been imposed to interval-based temporal logics to reduce them to point-based ones. The problem of identifying expressive enough, yet decidable, new interval logics or fragments of existing ones that are genuinely interval-based is still largely unexplored. In this paper, we focus our attention on interval logics of temporal neighborhood. We address the decision problem for the future fragment of Neighborhood Logic (Right Propositional Neighborhood Logic, RPNL for short), and we positively solve it by showing that the satisfiability problem for RPNL over natural numbers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure, and we prove its optimality. Springer Science+Business Media, Inc., 2006 interval temporal logic nationallicence tableaux-based decision procedures nationallicence right propositional neighborhood logic nationallicence Bresolin Davide Dipartimento di Matematica e Informatica, Università degli Studi di Udine, Via Delle Scienze, 208, 33100, Udine, ITALY aut Montanari Angelo Dipartimento di Matematica e Informatica, Università degli Studi di Udine, Via Delle Scienze, 208, 33100, Udine, ITALY aut Sciavicco Guido Department of Information Engineering and Communications, Faculty of Informatics, University of Murcia, Campus de Espinardo, 30100, Espinardo (Murcia), Spain aut Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 173-199 0168-7433 38:1-3<173 2007 38 10817 https://doi.org/10.1007/s10817-006-9051-0 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-006-9051-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Bresolin Davide Dipartimento di Matematica e Informatica, Università degli Studi di Udine, Via Delle Scienze, 208, 33100, Udine, ITALY aut NATIONALLICENCE 700 1- Montanari Angelo Dipartimento di Matematica e Informatica, Università degli Studi di Udine, Via Delle Scienze, 208, 33100, Udine, ITALY aut NATIONALLICENCE 700 1- Sciavicco Guido Department of Information Engineering and Communications, Faculty of Informatics, University of Murcia, Campus de Espinardo, 30100, Espinardo (Murcia), Spain aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Kluwer Academic Publishers 38/1-3(2007-04-01), 173-199 0168-7433 38:1-3<173 2007 38 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer