A fixed point semantics for the ATMS - INRAE - Institut national de recherche pour l’agriculture, l’alimentation et l’environnement Access content directly
Journal Articles Journal of Logic and Computation Year : 1993

A fixed point semantics for the ATMS

M. Cayrol
  • Function : Author
O. Palmade
  • Function : Author


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.


No file

Dates and versions

hal-02700521 , version 1 (01-06-2020)


  • 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, 1993, 3 (2), pp.115-130. ⟨hal-02700521⟩
8 View
0 Download


Gmail Facebook X LinkedIn More