Previous: AIDA-97-01 Next: AIDA-97-03 Index 1997

Intellectics Group: Technical Report 97-02

Which Hypotheses Can Be Found with Inverse Entailment ?

Akihiro Yamamoto

In this paper we give a completeness theorem of an inductive inference rule inverse entailment proposed by Muggleton. Our main result is that a hypothesis clause H can be derived from an Example E under a backround theory B with inverse entailment iff H subsumes E relative to B in Plotkin's sense. The theory B can be any clausal theory, and the example E can be any clause which is neither a tautology nor implied by B. The derived hypothesis H is a clause which is not always definite. In order to prove the result we give declarative semantics for arbitrary consistent clausal theories, and show that SB-resolution, which was originally introduced by Plotkin, is complete procedural semantics. The completeness is shown as an extension of the completeness theorem of SLD-resolution. We also show that every hypothesis H derived with saturant generalization, proposed by Rouveirol, must subsume E w.r.t. B in Buntine's sense. Moreover we show that saturant generalization can be obtained from inverse entailment by giving some restriction to its usage.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry