Completeness and properness of refinement operators in inductive logic programming

AbstractWithin Inductive Logic Programming, refinement operators compute a set of specializations or generalizations of a clause. They are applied in model inference algorithms to search in a quasi-ordered set for clauses of a logical theory that consistently describes an unknown concept. Ideally, a refinement operator is locally finite, complete, and proper. In this article we show that if an element in a quasi-ordered set 〈S, ≥〉 has an infinite or incomplete cover set, then an ideal refinement operator for 〈S, ≥〉 does not exist. We translate the nonexistence conditions to a specific kind of infinite ascending and descending chains and show that these chains exist in unrestricted sets of clauses that are ordered by θ-subsumption. Next we discuss how the restriction to a finite ordered subset can enable the construction of ideal refinement operators. Finally, we define an ideal refinement operator for restricted θ-subsumption ordered sets of clauses