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(¬) with modal operators defined with respect to both accessibility and inaccessibility, for which two refined calculi are given.
CITATION STYLE
Tishkovsky, D., & Schmidt, R. A. (2017). Rule refinement for semantic tableau calculi. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10501 LNAI, pp. 228–244). Springer Verlag. https://doi.org/10.1007/978-3-319-66902-1_14
Mendeley helps you to discover research relevant for your work.