Completing Inverse Entailment

Yamamoto has shown that the Inverse Entailment (IE) mechanism described previously by the author is complete for Plotkin’s relative subsumption but incomplete for entailment. Such a form of incompleteness impedes the learning of mutually recursive definitions such as those found in grammar learning. Thus Yamamoto shows that an hypothesised clause can be derived from an example under a background theory ff using IE if and only if subsumes relative to ff in Plotkin’s sense. Yamamoto gives examples of for which ffflfi ffi but cannot be constructed using IE from ff and . The main result of the present paper is a theorem to show that by enlarging the bottom set used within IE, it is possible to make a revised version of IE complete with respect to entailment for Horn theories. Furthermore, it is shown for function-free definite clauses that given a bound! on the arity of predicates used in ff and , the cardinality of the enlarged bottom set is bounded above by the polynomial function "$#&%')(+*-, , where " is the number of predicates in ff/.0 and % is the number of constants in ff1fi