Optimal Tableau Algorithms for Coalgebraic Logics
dc.contributor.author | Gore, Rajeev | |
dc.contributor.author | Kupke, Clemens | |
dc.contributor.author | Pattinson, Dirk | |
dc.coverage.spatial | Paphos Cyprus | |
dc.date.accessioned | 2015-12-07T22:23:12Z | |
dc.date.created | March 20-28 2010 | |
dc.date.issued | 2010 | |
dc.date.updated | 2016-02-24T10:21:20Z | |
dc.description.abstract | Deciding 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.uri | http://hdl.handle.net/1885/20563 | |
dc.publisher | Springer | |
dc.relation.ispartofseries | International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010) | |
dc.source | Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010) | |
dc.subject | Keywords: 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.title | Optimal Tableau Algorithms for Coalgebraic Logics | |
dc.type | Conference paper | |
local.contributor.affiliation | Gore, Rajeev, College of Engineering and Computer Science, ANU | |
local.contributor.affiliation | Kupke, Clemens, Imperial College London | |
local.contributor.affiliation | Pattinson, Dirk, Imperial College London | |
local.contributor.authoremail | u9409448@anu.edu.au | |
local.contributor.authoruid | Gore, Rajeev, u9409448 | |
local.description.embargo | 2037-12-31 | |
local.description.notes | Imported from ARIES | |
local.description.refereed | Yes | |
local.identifier.absfor | 080200 - COMPUTATION THEORY AND MATHEMATICS | |
local.identifier.absseo | 970108 - Expanding Knowledge in the Information and Computing Sciences | |
local.identifier.ariespublication | u3968803xPUB13 | |
local.identifier.doi | 10.1007/978-3-642-12002-2_9 | |
local.identifier.scopusID | 2-s2.0-77951617983 | |
local.identifier.uidSubmittedBy | u3968803 | |
local.type.status | Published Version |