Skip to Main content Skip to Navigation
Journal articles

A fixed point semantics for the ATMS

Abstract : 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Migration ProdInra Connect in order to contact the contributor
Submitted on : Monday, June 1, 2020 - 1:11:25 PM
Last modification on : Friday, March 18, 2022 - 3:32:48 AM


  • HAL Id : hal-02700521, version 1
  • PRODINRA : 135941



M. Cayrol, O. Palmade, Thomas Schiex. A fixed point semantics for the ATMS. Journal of Logic and Computation, Oxford University Press (OUP), 1993, 3 (2), pp.115-130. ⟨hal-02700521⟩



Record views