@INPROCEEDINGS{SchmidtWaldmann15,
AUTHOR = {Schmidt, R. A. and Waldmann, U.},
YEAR = {2015},
TITLE = {Modal Tableau Systems with Blocking and Congruence Closure},
EDITOR = {{De Nivelle}, H.},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {9323},
PUBLISHER = {Springer},
PAGES = {38--53},
DOI = {http://dx.doi.org/10.1007/978-3-319-24312-2_4},
URL = {\url{http://www.cs.man.ac.uk/~schmidt/publications/SchmidtWaldmann15.html}},
ABSTRACT = {Our interest in this paper are semantic tableau approaches
closely related to bottom-up model generation methods.
Using equality-based blocking techniques these can be used to decide
logics representable in first-order logic that have the finite model
property.
Many common modal and description logics have these properties and can
therefore be decided in this way.
This paper integrates congruence closure, which is probably the most
powerful and efficient way to realise reasoning with ground equations,
into a modal tableau system with equality-based blocking.
The system is described for an extension of modal logic K
characterised by frames in which the accessibility relation is
transitive and every world has a distinct immediate predecessor.
We show the system is sound and complete, and discuss how various forms
of blocking such as ancestor blocking can be realised in this setting.
Though the investigation is focussed on a particular modal logic, the
modal logic was chosen to show the most salient ideas and techniques
for the results to be generalised to other tableau calculi and
other logics.
}
}