Logically-Complete Local Search for Propositional Nonmonotonic Knowledge Bases
Éric Grégoire, Bertrand Mazure, Lakhdar Saïs · 1998
In this paper, a new approach to compute nonmonotonic inferences in a simple but useful propositional model-preference formalism is presented. It is original from at least two points of view. First, it makes use of local search techniques while preserving logical completeness. Second, it proves experimentally efficient for an important class of very large nonmonotonic knowledge bases. More precisely, it extends recent SAT-related practical computational results to a nonmonotonic framework. The proof-strategy is based on the use of local search techniques for SAT together with an efficient heuristic when these techniques fail to deliver a model. It is applied to a formalism allowing prioritized rules of default reasoning to be expressed, using McCarthy's Abnormality propositions. A typical application domain concerns the forms of defeasible reasoning that can be held from a deep model of a complex device or system, where Abnormality propositions are used to represent possible (but unexp...