Ideal Theory Refinement under Object Identity

We present a framework for theory refinement operators fulfilling some desirable properties in order to ensure the efficiency and effectiveness of the process. A refinement operator satisfying these requirements is defined ideal. In other frameworks, the search for refinements takes place in spaces ordered by the logical implication or the theta-subsumption relationships. Results have demonstrated the impossibility of defining ideal operators in these search spaces. We show that, by assuming the object identity bias over a clausal representation, we are able to define them in the resulting search space.