Presents a new and unifying formalization of the inference techniques involved in assumption-based truth maintenance systems (ATMS). Basic concepts of ATMS are briefly reviewed. Then an original inference system, called P-deduction, is presented, which enables us to build a propositional backward-chaining prover. It is shown how to exploit the results provided by the proof algorithm in order to compute labels, interpretations, and nogoods.

The ATMS resolution mechanisms have been formalized, using the concept of DK-tree. We propose in this paper a new and simple approach based on the fixed point theory and an original demonstration of the completeness of these mechanisms. We first introduce the basic definitions of terms, sets and functions which are used in the paper and build a lattice. Then, the basic formal tools to describe the ATMS mechanisms are introduced: The notion of DK-clash (in fact, the inference rule), and a monotonic function, which represents the deduction process and whose least fixed point corresponds to the output of an ATMS. We prove the soundness and the completeness (for specific clauses) of these mechanisms. This demonstration brings to light an original and interesting property, whose applications are discussed at the end of the paper.