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.
展开▼
