Generalization of certain types of clauses of the first-order predicate logic

Abstract

In the area of inductive learning, generalization is the main operation, and the usual definition of induction I based on logical implication, Plotkin’s well-known technique for computing least general generalizations of clauses under {u1D719}-subsumption sometimes sometimes produces results which are too general with respect to implication. Muggleton has shown that this problem only occurs in one type of gencralization of recursive clauses, called an indirect root. Idestam-Almguist presented a technique, called recursive anti-unification, to compute indirect roots of clauses. However there exist cases for which recursive anti-unification does not work, cases where at least one of the clauses contains a structure called a cross connection. In this research, we develop a technique for computing indirect roots of Horn clauses. We firat introduce a relation equivalent to implication, called {u1D719}-proof, which is syntactically defined, using resolution and {u1D719}-subsumption. This leads us to an algorithm, the J-algorithm, for computing indirect roots of clauses. Because the J-algorithm makes no assumptions about the structure of its input clause, it can compute roots of clauses containing cross connections. We also prove that the output from the algorithm is a generalization under implication of the input.