Renate A. Schmidt ; Dmitry Tishkovsky - Automated Synthesis of Tableau Calculi

lmcs:970 - Logical Methods in Computer Science, May 7, 2011, Volume 7, Issue 2 - https://doi.org/10.2168/LMCS-7(2:6)2011
Automated Synthesis of Tableau CalculiArticle

Authors: Renate A. Schmidt ORCID; Dmitry Tishkovsky

    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 that 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 provides 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 a description logic with transitive roles and propositional intuitionistic logic.


    Volume: Volume 7, Issue 2
    Published on: May 7, 2011
    Imported on: May 29, 2010
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Symbolic Computation,cs.SC

    Classifications

    Mathematics Subject Classification 20201

    14 Documents citing this article

    Consultation statistics

    This page has been seen 1916 times.
    This article's PDF has been downloaded 696 times.