An abductive proof procedure handling active rules

We present a simple, though powerful extension of an abductive proof procedure proposed in the literature, the so-called KM-procedure, which allows one to properly treat more general forms of integrity constraints than those handled by the original procedure. These constraints are viewed as active rules, and their treatment allows the integration of a limited form of forward reasoning within the basic, backward reasoning framework upon which the KM-procedure is based. We first provide some background on Abductive Logic Programming and the KM-procedure and then formally present the extension, named AKM-procedure. The usefulness of the extension is shown by means of some simple examples.