A general framework for reason maintenance

摘要

There are several different kinds of reason-maintenance system in existence, which provide rather different functionalities. I present a general structure that subsumes most such systems, and that allows some new behaviors to emerge. The general framework is based on logic-style clauses (disjunctions of literals) instead of justifications. Literals are tagged with labels that say what assumption sets make them true and false. Nonmonotonicity is implemented by allowing clauses to contain disjuncts of the form Lp, which supports propagation through a clause whenever p is not known to be true. The resulting system supports two popular styles of dependency-directed backtracking, using nogoods and assumption retraction. Assumption retraction does not require a separate contradiction-elimination phase, but occurs automatically during label propagation. Label propagation can be achieved by the usual variants of Boolean constraint propagation, provided there are no “odd loops” through the clauses, and it can be shown that the system itself never creates odd loops.