@INPROCEEDINGS{Schmidt11a,
AUTHOR = {Schmidt, R. A.},
YEAR = {2011},
TITLE = {Synthesising Terminating Tableau Calculi for Relational Logics: Invited paper},
EDITOR = {de Swart, H.},
BOOKTITLE = {Relational and Algebraic Methods in Computer Science (RAMiCS 12)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {6663},
PUBLISHER = {Springer},
PAGES = {40--49},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/Schmidt11a.html}},
DOI = {http://dx.doi.org/10.1007/978-3-642-21070-9_3},
ABSTRACT = {Tableau-based deduction is an active and well-studied area of 
several branches of logic and automated reasoning.  In this paper we 
discuss the challenge of automatically generating tableau calculi from 
the semantic specification of logics, while guaranteeing soundness, 
completeness and termination, when possible.
},
}