Refinement operators can be (weakly) perfect

Our aim is to construct a perfect (i.e. minimal and optimal) ILP refinement operator for hypotheses spaces bounded below by a most specific clause and subject to syntactical restrictions in the form of input/output variable declarations (like in Progol). Since unfortunately no such optimal refinement operators exist, we settle for a weaker form of optimality and introduce an associated weaker form of subsumption which exactly captures a first incompleteness of Progol's refinement operator. We argue that this sort of incompleteness is not a drawback, as it is justified by the examples and the MDL heuristic. A second type of incompleteness of Progol (due to subtle interactions between the requirements of non-redundancy, completeness and the variable dependencies) is more problematic, since it may sometimes lead to unpredictable results. We remove this incompleteness by constructing a sequence of increasingly more complex refinement operators which eventually produces the first (weakly) perfect refinement operator for a Progol-like ILP system.