@INPROCEEDINGS{TishkovskySchmidt17,
AUTHOR = {Tishkovsky, D. and Schmidt, R. A.},
YEAR = {2017},
TITLE = {Rule Refinement for Semantic Tableau Calculi},
BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2017)},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10501},
PAGES = {228--244},
PUBLISHER = {Springer},
DOI = {https://doi.org/10.1007/978-3-319-66902-1_14},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/TishkovskySchmidt17.html},
ABSTRACT = {
This paper investigates refinement techniques for semantic tableau calculi.
The focus is on techniques to reduce branching in inference rules and thus
allow more effective ways of carrying out deductions. We introduce an easy
to apply, general principle of atomic rule refinement, which depends on a
purely syntactic condition that can be easily verified. The refinement has
a wide scope, for example, it is immediately applicable to inference rules
associated with frame conditions of modal logics, or declarations of role
properties in description logics, and it allows for routine development of
hypertableau-like calculi for logics with disjunction and negation. The
techniques are illustrated on Humberstone's modal logic Km(not) with modal
operators defined with respect to both accessibility and inaccessibility,
for which two refined calculi are given.
}
}