by Schmidt, R. A.
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.
Reference:
Synthesising Terminating Tableau Calculi for Relational Logics: Invited paper (Schmidt, R. A.), In Relational and Algebraic Methods in Computer Science (RAMiCS 12) (de Swart, H., ed.), Springer, volume 6663, 2011.
Bibtex Entry:
@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 = {http://www.springerlink.com/content/h186p475321256q7/fulltext.pdf},
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.
},
}