In this paper we focus our attention on the decision problem for Propositional Neighborhood Logic (PNL for short). PNL is the proper subset of Halpern and Shoham’s modal logic of intervals whose modalities correspond to Allen’s relations meets and met by. We show that the satisfiability problem for PNL over the integers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure and we prove its optimality.
An optimal tableau-based decision algorithm for Propositional Neighborhood Logic / Davide Bresolin; Angelo Montanari; Pietro Sala. - STAMPA. - 4393:(2007), pp. 549-560. (Intervento presentato al convegno 24th Annual Symposium on Theoretical Aspects of Computer Science STACS 2007 tenutosi a Aachen, Germany nel February 22-24, 2007) [10.1007/978-3-540-70918-3_47].
An optimal tableau-based decision algorithm for Propositional Neighborhood Logic
BRESOLIN, DAVIDE;
2007
Abstract
In this paper we focus our attention on the decision problem for Propositional Neighborhood Logic (PNL for short). PNL is the proper subset of Halpern and Shoham’s modal logic of intervals whose modalities correspond to Allen’s relations meets and met by. We show that the satisfiability problem for PNL over the integers is NEXPTIME-complete. Then, we develop a sound and complete tableau-based decision procedure and we prove its optimality.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
