Solving graded/probabilistic modal logic via linear inequalities (system description). (English) Zbl 1352.68215
Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 383-390 (2012).
Summary: We present the experience gained from implementing a new decision procedure for both graded and probabilistic modal logic. While our approach uses standard tableaux for propositional connectives, modal rules are given by linear constraints on the arguments of operators. The implementation uses binary decision diagrams for propositional connectives and a linear programming library for the modal rules. We compare our implementation, for graded modal logic, with other tools, showing average performance. Due to lack of other implementations, no comparison is provided for probabilistic modal logic, the main new feature of our implementation.
For the entire collection see [Zbl 1238.68012].
For the entire collection see [Zbl 1238.68012].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B45 | Modal logic (including the logic of norms) |
