Ideal refinement of Datalog programs

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