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
BRESOLIN, Davide;MONTANARI, Angelo;SALA, Pietro
2007-01-01
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
