Generalization of Clauses under Implication
  In the area of inductive learning, generalization is a main operation, and
the usual definition of induction is based on logical implication. Recently
there has been a rising interest in clausal representation of knowledge in
machine learning. Almost all inductive learning systems that perform
generalization of clauses use the relation theta-subsumption instead of
implication. The main reason is that there is a well-known and simple technique
to compute least general generalizations under theta-subsumption, but not under
implication. However generalization under theta-subsumption is inappropriate
for learning recursive clauses, which is a crucial problem since recursion is
the basic program structure of logic programs. We note that implication between
clauses is undecidable, and we therefore introduce a stronger form of
implication, called T-implication, which is decidable between clauses. We show
that for every finite set of clauses there exists a least general
generalization under T-implication. We describe a technique to reduce
generalizations under implication of a clause to generalizations under
theta-subsumption of what we call an expansion of the original clause. Moreover
we show that for every non-tautological clause there exists a T-complete
expansion, which means that every generalization under T-implication of the
clause is reduced to a generalization under theta-subsumption of the expansion.
