Abductive Logic Programming - Formal Semantics

Formal Semantics

The formal semantics of the central notion of an abductive explanation in ALP, can be defined in the following way:

Given an abductive logic program, an abductive explanation for a problem is a set of ground atoms on abducible predicates such that:

This definition is generic in the underlying semantics of logic programming. Each particular choice of semantics defines its own entailment relation, its own notion of consistent logic programs and hence its own notion of what an abductive solution is. In practice, the three main semantics of logic programming --- completion, stable and well-founded semantics --- have been used to define different ALP frameworks.

The integrity constraints define how they constrain the abductive solutions. There are different views on this. Early work on abduction in Theorist in the context of classical logic was based on the consistency view on constraints. In this view, any extension of the given theory with an abductive solution is required to be consistent with the integrity constraints IC: is consistent. The above definition formalizes the entailment view: the abductive solution together with should entail the constraints. This view is the one taken in most versions of ALP and is stronger than the consistency view in the sense that a solution according to the entailment view is a solution according to the consistency view but not vice versa.

The difference between the two views can be subtle but in practice the different views usually coincide. E.g. it frequently happens that has a unique model, in which case the two views are equivalent. In practice, many ALP systems use the entailment view as this can be easily implemented without the need for any extra specialized procedures for the satisfaction of the integrity constraints since this semantics treats the constraints in the same way as the goal.