Skip navigation
Skip navigation
A change is coming. Click to see a sneak peek of the new Open Research Repository.

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

Download (276.32 kB)

link to publisher version

  • Altmetric Citations

Gore, Rajeev; Widmann, Florian

Description

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]

dc.contributor.authorGore, Rajeev
dc.contributor.authorWidmann, Florian
dc.coverage.spatialEdinburgh Scotland
dc.date.accessioned2015-12-07T22:21:35Z
dc.date.createdJuly 16-19 2010
dc.identifier.urihttp://hdl.handle.net/1885/20111
dc.description.abstractWe 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.
dc.publisherConference Organising Committee
dc.relation.ispartofseriesInternational Joint Conference on Automated Reasoning (IJCAR 2010)
dc.sourceProceedings of International Joint Conference on Automated Reasoning (IJCAR 2010)
dc.subjectKeywords: Description logic; Non-trivial; Optimal methods; Propositional dynamic logic; Satisfiability; Theorem provers; Automata theory; Data description; Formal logic; Problem solving; Optimization
dc.titleOptimal and Cut-Free Tableaux for propositional dynamic logic with converse
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2010
local.identifier.absfor080200 - COMPUTATION THEORY AND MATHEMATICS
local.identifier.ariespublicationu3968803xPUB11
local.type.statusPublished Version
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.contributor.affiliationWidmann, Florian, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage225
local.bibliographicCitation.lastpage239
local.identifier.doi10.1007/978-3-642-14203-1_20
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
dc.date.updated2016-02-24T10:21:19Z
local.identifier.scopusID2-s2.0-77955233683
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Gore_Optimal_and_Cut-Free_Tableaux_2010.pdf276.32 kBAdobe PDFThumbnail
Show simple item record


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

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator