Interval temporal logics are quite expressive temporal logics, which turn out to be difficult to deal with in many respects. Even finite satisfiability of simple interval temporal logics presents non-trivial technical issues when it comes to the implementation of efficient tableau-based decision procedures. We focus our attention on the logic of Allen's relation meets, a.k.a. Right Propositional Neighborhood Logic (RPNL), interpreted over finite linear orders. Starting from a high-level description of a tableau system, we developed a first working implementation of a decision procedure for RPNL, and we made it accessible from the web. We report and analyze the outcomes of some initial tests. © 2013 Springer-Verlag.
A tableau system for right propositional neighborhood logic over finite linear orders: An implementation
Sciavicco G.
Ultimo
2013
Abstract
Interval temporal logics are quite expressive temporal logics, which turn out to be difficult to deal with in many respects. Even finite satisfiability of simple interval temporal logics presents non-trivial technical issues when it comes to the implementation of efficient tableau-based decision procedures. We focus our attention on the logic of Allen's relation meets, a.k.a. Right Propositional Neighborhood Logic (RPNL), interpreted over finite linear orders. Starting from a high-level description of a tableau system, we developed a first working implementation of a decision procedure for RPNL, and we made it accessible from the web. We report and analyze the outcomes of some initial tests. © 2013 Springer-Verlag.File | Dimensione | Formato | |
---|---|---|---|
tab2013.pdf
solo gestori archivio
Descrizione: Articolo
Tipologia:
Full text (versione editoriale)
Licenza:
NON PUBBLICO - Accesso privato/ristretto
Dimensione
161.07 kB
Formato
Adobe PDF
|
161.07 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.