File:Deriving Inference Rules for DL A Rewriting Approach into Sequent Calculi r111.pdf

Véronique Royer and Joachim Quantz 1993: Description Logics (DL) can be investigated under different perspectives. The aim of this report is to provide the basis for a tighter combination of theoretical investigations with issues arising in the actual implementation of DL systems. We propose to use inference rules, derived via the Sequent Calculus, as a new method for specifying terminological inference algorithms. This approach combines the advantages of the tableaux methods and the normalize-compare algorithms that have been predominant in terminological proof theory so far. In our paper presented at JELIA’92 we proposed a generic method for deriving complete sets of inference rules for DL. The method relies upon translations into Sequent Calculus and systematic rewriting of sequent proofs. We illustrated our method on a relatively restricted terminological logic. In this report the approach is extended to the more expressive logic underlying Back V5. It turns out that concept-forming operators involving equality and role-forming operators considerably increase the complexity of our rewriting strategy. The derived inference rules can be used in two ways for the characterization of DL systems: first, the incompleteness of systems can be documented by listing those rules that have not been implemented; second, the reasoning strategy can be described by specifying which rules are applied forward and which backward.