Expressing default abduction problems as quantified Boolean formulas

Abduction is the process of finding explanations for observed phenomena in accord to known laws about a given application domain. This form of reasoning is an important principle of common-sense reasoning and is particularly relevant in conjunction with nonmonotonic knowledge representation formalisms. In this paper, we deal with a model for abduction in which the domain knowledge is represented in terms of a default theory. We show how the main reasoning tasks associated with this particular form of abduction can be axiomatised within the language of quantified Boolean logic. More specifically, we provide polynomial-time constructible reductions mapping a given abduction problem into a quantified Boolean formula (QBF) such that the satisfying truth assignments to the free variables of the latter determine the solutions of the original problem. Since there are now efficient QBF-solvers available, this reduction technique yields a straightforward method to implement the discussed abduction tasks. We describe a realisation of this approach by appeal to the reasoning system QUIP.