Rule Refinement for Semantic Tableau Calculi

摘要

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 K_m(-) with modal operators defined with respect to both accessibility and inaccessibility, for which two refined calculi are given.