Automated Synthesis of a Finite Complexity Ordering for Saturation

Yannick Chevalier 1 Mounira Kourjieh 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present in this paper a new procedure to saturate a set of clauses with respect to a well-founded ordering on ground atoms such that A < B implies Var(A) ⊆ Var(B) for every atoms A and B. This condition is satisfied by any atom ordering compatible with a lexicographic, recursive, or multiset path ordering on terms. Our saturation procedure is based on a priori ordered resolution and its main novelty is the on-the-fly construction of a finite complexity atom ordering. In contrast with the usual redundancy, we give a new redundancy notion and we prove that during the saturation a non-redundant inference by a priori ordered resolution is also an inference by a posteriori ordered resolution. We also prove that if a set S of clauses is saturated with respect to an atom ordering as described above then the problem of whether a clause C is entailed from S is decidable.
Complete list of metadatas
Contributor : Mounira Kourjieh <>
Submitted on : Friday, March 2, 2012 - 2:18:03 PM
Last modification on : Friday, January 10, 2020 - 9:09:12 PM
Long-term archiving on: Friday, November 23, 2012 - 3:30:59 PM


Files produced by the author(s)


  • HAL Id : hal-00675954, version 1


Yannick Chevalier, Mounira Kourjieh. Automated Synthesis of a Finite Complexity Ordering for Saturation. [Research Report] 2012. ⟨hal-00675954v1⟩



Record views


Files downloads