ABox Abduction in Description Logic
Szymon Klarman

Abstract:
In this thesis we elaborate on logic-based automated reasoning tech-
niques for abduction, driven by the principle of goal-oriented rea-
soning. In the first part we develop two variants of a computational
framework for abduction in propositional logic, based on regular con-
nection tableaux and resolution with set-of-support. The procedures
are proven to be sound and complete calculi for finding consistent,
minimal and relevant solutions to abductive problems. In the sec-
ond part we adapt the framework to the Description Logic ALC.
We obtain a procedure for solving ABox abduction problems (i.e.
abductive problems whose main part of the input and every solution
are specified by a set of ABox assertions), for which we prove the
results of (plain) soundness and (minimality) completeness.