A New Mapping from ALCI to ALC

Abstract. This paper studies a technique for mapping ALCI knowledge bases into ALC. Worst-case optimal tableau-based procedures for the satisfiability/consistency problem w.r.t. general/acyclic axioms are available through such a mapping. By applying this mapping, a tableaubased reasoner succeeds in solving some very hard real-world problems. 1 Concept Satisfiability with General Axioms The proposed mapping process is based on the idea to capture possible backpropagation caused by the use of inverse roles. This process uses three techniques, tagging, recording, polarisation, which are introduced below. We refer to [BCM+ 03] for usual background knowledge on description logics (DLs). Concept expressions are assumed to be in negation normal form (NNF). For simplicity, we consider only one GCI of the form C, where C is in NNF.

• Type: Conference
• Year: 2007
• Where: DLOG
• Authors: Yu Ding, Volker Haarslev, Jiewen Wu
• Keywords: ALCI Knowledge Bases, Automated Reasoning, DLOG 2007, General/acyclic Axioms, Optimal Tableau-based Procedures