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:
| File | Dimensione | Formato | |
|---|---|---|---|
|
43930549.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Non pubblico
Dimensione
388.69 kB
Formato
Adobe PDF
|
388.69 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
