Dmitry Tishkovsky and Renate Schmidt. Automated Synthesis of Tableau Calculi

It is possible to synthesise tableau deduction calculi from the specifications of logics. In this course we give an introduction to a powerful method for synthesising sound, complete and terminating tableau calculi for description logics, modal logics and related fragments of first-order logic.  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 an unrestricted blocking mechanism yields a terminating tableau calculus.  The method provides a general approach to developing tableau decision procedures for expressive logics. We illustrate the method on several examples from non-classical logic.

Moodle site