TY - GEN
T1 - Solving graded/probabilistic modal logic via linear inequalities (system description)
AU - Snell, William
AU - Pattinson, Dirk
AU - Widmann, Florian
PY - 2012
Y1 - 2012
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84858302853&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-28717-6_30
DO - 10.1007/978-3-642-28717-6_30
M3 - Conference contribution
SN - 9783642287169
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 383
EP - 390
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Proceedings
T2 - 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
Y2 - 11 March 2012 through 15 March 2012
ER -