Subsumption and refinement in model inference

Abstract

In his famous Model Inference System, Shapiro [10] uses socalled refinement operators to replace too general hypotheses by logically weaker ones. One of these refinement operators works in the search space of reduced first order sentences. In this article we show that this operator is not complete for reduced sentences, as he claims. We investigate the relations between subsumption and refinement as well as the role of a complexity measure. We present an inverse reduction algorithm which is used in a new refinement operator. This operator is complete for reduced sentences. Finally, we will relate our new refinement operator with its dual, a generalization operator, and its possible application in model inference using inverse resolution.