Selective refutation of integrity constraints in deductive databases

In this paper we have presented a method that allows the selection of those branches of a derivation tree that contain a specific clause as input clause. We have applied such method to integrity constraint checking but it seems useful in other application areas as well. Despite to its simplicity in the case of definite goals and programs, when introducing negation problems arise. We restricted ourselves to definite programs and normal goals because in the case of integrity checking it seems quite a general framework since constraints act as goals in our method. Note that if one makes the assumption that all the negative literals in the goal are ground, the verification method sensibly improves. The presented examples serve as an explanatory framework rather than providing convincing elements with respect to the advantages of the method. In order to get such an evidence examples that give rise to a more complex search spaces are needed. Much work has to be done to extend the approach to normal programs even if we foresee less advantages.