About the incremental validation of first-order stratified knowledge-based decision-support systems

In this paper, a new efficient technique is introduced to check the logical consistency of first-order stratified knowledge-based decision-support systems (M). 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 efficient very often is proposed. It delivers a good approximation of Benferhat et al.'s preferred maximal inclusion-based consistent sub-bases.