Locally finite, proper and complete operators for refining Datalog programs

Refinement operators are exploited to change in an automated way incorrect clauses of a logic program. In this paper, we present four refinement operators for Datalog programs and demonstrate that all of them meet the properties of local finiteness,properness, and completeness. Such operators are based on the quasi-ordering induced upon a set of clauses by the generalization model of θ-subsumption under object identity. This model of generalization, as well as the four refinement operators have been implemented in a system for theory revision that proved effective in the area of electronic document classification.