ABox abduction in ALC using a DL tableau

The formal definition of abduction asks what needs to be added to a knowledge base to enable an observation to be entailed by the knowledge base. ABox abduction in descrip-tion logics (DLs) asks what ABox statements need to be added to a DL knowledge base, to allow an observation (also in the form of ABox statements) to be entailed. Klarman et al [8] have provided an algorithm for performing ABox abduction in the description logic ALC by converting the knowledge base and observation to first-order logic, using a connection tableau to obtain abductive solutions, and then converting these back to DL syntax. In this paper we de-scribe how this can be done directly using a DL tableau