Cautious Backtracking and Well-Founded Semantics in Truth Maintenance Systems

摘要

A Truth Maintenance System (TMS) maintains a consistent state of belief given aset J of justifications, i.e., arguments for belief. To resolve contradictions dependency directed backtracking is performed. Cautious backtracking as a method that can be used to track all dependency directed backtracking methods simultaneously is introduced. This was previously done by adding the contrapositions of justifications to J. Contrapositions are shown not to be mandatory: the same result can be reached by adding one disjunctive justification (the consequent is not one atom, but can be a disjunction of atoms). This cautious backtracking is a minimal backscattering in that the revised beliefs are the beliefs agreed upon by every backtracking method. The well founded model for disjunctive logic programs gives a semantics to cautious backtracking. An alternative proof for the correctness of Witteveen's method for computing the well founded model is given.