@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.
}
}