ABox abduction in ALC using a DL tableau

Abstract

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 description 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 rst-order logic, using a connection tableau to obtain abductive solutions, and then converting these back to DL syntax. In this paper we describe how this can be done directly using a DL tableau.