Existence and nonexistence of complete refinement operators

Abstract

Inductive Logic Programming is a subfield of Machine Learning concerned with the induction of logic programs. In Shapiro's Model Inference System — a system that infers theories from examples — the use of downward refinement operators was introduced to walk through an ordered search space of clauses. Downward and upward refinement operators compute specializations and generalizations of clauses respectively. In this article we present the results of our study of completeness and properness of refinement operators for an unrestricted search space of clauses ordered by θ-subsumption. We prove that locally finite downward and upward refinement operators that are both complete and proper for unrestricted search spaces ordered by θ-subsumption do not exist. We also present a complete but improper upward refinement operator. This operator forms a counterpart to Laird's downward refinement operator with the same properties.