Automated synthesis of tableau calculi

Renate A. Schmidt, Dmitry Tishkovsky

    Research output: Contribution to journalArticlepeer-review


    This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules which can then be used to reason within the logic. The method guarantees that the generated rules form a calculus which is sound and constructively complete. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism produces a terminating tableau calculus. The process of generating tableau rules can be completely automated and produces, together with the blocking mechanism, an automated procedure for generating tableau decision procedures. For illustration we show the workability of the approach for propositional intuitionistic logic. © 2009 Springer-Verlag Berlin Heidelberg.
    Original languageEnglish
    Pages (from-to)310-324
    Number of pages14
    JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Publication statusPublished - 2009


    Dive into the research topics of 'Automated synthesis of tableau calculi'. Together they form a unique fingerprint.

    Cite this