A refinement operator for theories

Abstract

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.