@INPROCEEDINGS{SchmidtTishkovsky09b,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2009},
TITLE = {Automated Synthesis of Tableau Calculi},
EDITOR = {Giese, M. and Waaler, A.},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {5607},
PUBLISHER = {Springer},
PAGES = {310--324},
DOI = {http://dx.doi.org/10.1007/978-3-642-02716-1_23},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/SchmidtTishkovsky09b.html},
ABSTRACT = {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.
}
}