SLDNFA: An abductive procedure for abductive logic programs

AbstractWe present SLDNFA, an extension of SLDNF resolution for abductive reasoning on abductive logic programs. SLDNFA solves the floundering abduction problem: nonground abductive atoms can be selected. SLDNFA also provides a partial solution for the floundering negation problem. Different abductive answers can be derived from an SLDNFA refutation; these answers provide different compromises between generality and comprehensibility. Two extensions of SLDNFA are proposed that satisfy stronger completeness results. The soundness of SLDNFA and its extensions is proved. Their completeness for minimal solutions with respect to implication, cardinality, and set inclusion is investigated. The formalization of SLDNFA presented here is an update of an older version and does not rely on skolemization of abductive atoms