Most implemented ILP systems construct hypotheses clause by clause using a refinement operator
for clauses. To avoid the problems faced by such greedy covering algorithms, more
flexible refinement operators
for theories are needed. In this paper we construct a syntactically monotonic, finite and solution-complete refinement operator for theories,
which eliminates certain annoying redundancies (due to clause deletions), while also addressing the limitations faced by HYPER’s
refinement operator (which are mainly due to keeping the number of clauses constant during refinement).
We also show how to eliminate the redundancies due to the commutativity of refinement operations while preserving weak completeness
as well as a limited form of flexibility. The refinement operator presented in this paper represents a first step towards
constructing more efficient and flexible ILP systems with precise theoretical guarantees.