TY - GEN
T1 - Optimal and cut-free tableaux for propositional dynamic logic with converse
AU - Goré, Rajeev
AU - Widmann, Florian
PY - 2010
Y1 - 2010
N2 - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.
AB - We give an optimal (exptime), sound and complete tableau-based algorithm for deciding satisfiability for propositional dynamic logic with converse (CPDL) which does not require the use of analytic cut. Our main contribution is a sound method to combine our previous optimal method for tracking least fix-points in PDL with our previous optimal method for handling converse in the description logic ALCI. The extension is non-trivial as the two methods cannot be combined naively. We give sufficient details to enable an implementation by others. Our OCaml implementation seems to be the first theorem prover for CPDL.
UR - http://www.scopus.com/inward/record.url?scp=77955233683&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-14203-1_20
DO - 10.1007/978-3-642-14203-1_20
M3 - Conference contribution
SN - 3642142028
SN - 9783642142024
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 225
EP - 239
BT - Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings
T2 - 5th International Joint Conference on Automated Reasoning, IJCAR 2010
Y2 - 16 July 2010 through 19 July 2010
ER -