Skip navigation
Skip navigation

Optimal and Cut-Free Tableaux for propositional dynamic logic with converse

Gore, Rajeev; Widmann, Florian


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]

CollectionsANU Research Publications
Date published: 2010
Type: Conference paper
Source: Proceedings of International Joint Conference on Automated Reasoning (IJCAR 2010)
DOI: 10.1007/978-3-642-14203-1_20


File Description SizeFormat Image
01_Gore_Optimal_and_Cut-Free_Tableaux_2010.pdf276.32 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator