Validation of first-order stratified KBs

In this paper, a new efficient technique is introduced to check the logical consistency of finite first-order stratified KBs. It is based on a progressive instantiation schema that enables us to benefit from the power of local search techniques for propositional satisfiability and search. It combines a knowledge preference pre-ordering with a concept of depth-limited reasoning. An algorithm that proves to be efficient is proposed. It delivers a good approximation of (Benferhat et al., 1993) preferred maximal inclusion-based consistent sub-bases