Optimal tableau algorithms for coalgebraic logics

Rajeev Goré*, Clemens Kupke, Dirk Pattinson

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    10 Citations (Scopus)

    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.

    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.
    Pages114-128
    Number of pages15
    DOIs
    Publication statusPublished - 2010
    Event16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 - Paphos, Cyprus
    Duration: 20 Mar 201028 Mar 2010

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume6015 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010
    Country/TerritoryCyprus
    CityPaphos
    Period20/03/1028/03/10

    Fingerprint

    Dive into the research topics of 'Optimal tableau algorithms for coalgebraic logics'. Together they form a unique fingerprint.

    Cite this