A New Mapping from ALCI to ALC.
Yu Ding, Volker Haarslev, Jiewen Wu · 2007
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. Definition 1. (Tagging-1) The tagging techniques introduces new concept names for concept expressions and axioms. tag(·) on formula x is defined as: (1) if x is C ⊓ D, then tag(x) = tag(C) ⊓ tag(D);