ANU Open Research Repository has been upgraded. We are still working on a few minor issues, which may result in short outages throughout the day. Please get in touch with repository.admin@anu.edu.au if you experience any issues.
 

Optimal Tableau Algorithms for Coalgebraic Logics

dc.contributor.authorGore, Rajeev
dc.contributor.authorKupke, Clemens
dc.contributor.authorPattinson, Dirk
dc.coverage.spatialPaphos Cyprus
dc.date.accessioned2015-12-07T22:23:12Z
dc.date.createdMarch 20-28 2010
dc.date.issued2010
dc.date.updated2016-02-24T10:21:20Z
dc.description.abstractDeciding whether a modal formula is satisfiable with respect to a given set of (global) assumptions is a question of fundamental importance in applications of logic in computer science. Tableau methods have proved extremely versatile for solving this problem for many different individual logics but they typically do not meet the known complexity bounds for the logics in question. Recently, it has been shown that optimality can be obtained for some logics while retaining practicality by using a technique called "global caching". Here, we show that global caching is applicable to all logics that can be equipped with coalgebraic semantics, for example, classical modal logic, graded modal logic, probabilistic modal logic and coalition logic. In particular, the coalgebraic approach also covers logics that combine these various features. We thus show that global caching is a widely applicable technique and also provide foundations for optimal tableau algorithms that uniformly apply to a large class of modal logics.
dc.identifier.urihttp://hdl.handle.net/1885/20563
dc.publisherSpringer
dc.relation.ispartofseriesInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010)
dc.sourceProceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010)
dc.subjectKeywords: Coalgebraic; Coalgebraic logic; Coalgebraic semantics; Complexity bounds; Large class; Logic in computer science; Modal formulas; Modal logic; Optimality; Tableau algorithm; Tableau method; Algorithms; Computer software; Probabilistic logics
dc.titleOptimal Tableau Algorithms for Coalgebraic Logics
dc.typeConference paper
local.contributor.affiliationGore, Rajeev, College of Engineering and Computer Science, ANU
local.contributor.affiliationKupke, Clemens, Imperial College London
local.contributor.affiliationPattinson, Dirk, Imperial College London
local.contributor.authoremailu9409448@anu.edu.au
local.contributor.authoruidGore, Rajeev, u9409448
local.description.embargo2037-12-31
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.absfor080200 - COMPUTATION THEORY AND MATHEMATICS
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
local.identifier.ariespublicationu3968803xPUB13
local.identifier.doi10.1007/978-3-642-12002-2_9
local.identifier.scopusID2-s2.0-77951617983
local.identifier.uidSubmittedByu3968803
local.type.statusPublished Version

Files