Optimal and Cut-Free Tableaux for propositional dynamic logic with converse
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...[Show more]
|Collections||ANU Research Publications|
|Source:||Proceedings of International Joint Conference on Automated Reasoning (IJCAR 2010)|
|01_Gore_Optimal_and_Cut-Free_Tableaux_2010.pdf||276.32 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.