Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse
Logic in Computer Science
2010-04-16 v2
Abstract
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 methodto 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.
Keywords
Cite
@article{arxiv.1002.0172,
title = {Optimal and Cut-free Tableaux for Propositional Dynamic Logic with Converse},
author = {Rajeev Goré and Florian Widmann},
journal= {arXiv preprint arXiv:1002.0172},
year = {2010}
}
Comments
30 pages, minor improvements, some typos, change of title