A tableau system for right propositional neighborhood logic over finite linear orders: an implementation. (English) Zbl 1401.68275
Galmiche, Didier (ed.) et al., Automated reasoning with analytic tableaux and related methods. 22nd international conference, TABLEAUX 2013, Nancy, France, September 16–19, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40536-5/pbk). Lecture Notes in Computer Science 8123. Lecture Notes in Artificial Intelligence, 74-80 (2013).
Summary: 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.
For the entire collection see [Zbl 1272.68020].
For the entire collection see [Zbl 1272.68020].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B44 | Temporal logic |
