@ARTICLE{SchmidtTishkovsky11a,
AUTHOR = {Schmidt, R. A. and Tishkovsky, D.},
YEAR = {2011},
TITLE = {Automated Synthesis of Tableau Calculi},
JOURNAL = {Logical Methods in Computer Science},
VOLUME = {7},
NUMBER = {2},
PAGES = {1--32},
DOI = {http://dx.doi.org/10.2168/LMCS-7(2:6)2011},
URL = {http://arxiv.org/pdf/1104.4131},
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 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. 
},
}