Skip to Main content Skip to Navigation

Automated Synthesis of a Finite Complexity Ordering for Saturation

Yannick Chevalier 1, 2 Mounira Kourjieh 3
1 IRIT-LILaC - Logique, Interaction, Langue et Calcul
IRIT - Institut de recherche en informatique de Toulouse
3 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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Mounira Kourjieh Connect in order to contact the contributor
Submitted on : Friday, March 9, 2012 - 12:17:03 PM
Last modification on : Tuesday, October 19, 2021 - 2:23:32 PM
Long-term archiving on: : Wednesday, December 14, 2016 - 11:40:38 AM


Files produced by the author(s)


  • HAL Id : hal-00675954, version 2
  • ARXIV : 1203.2809


Yannick Chevalier, Mounira Kourjieh. Automated Synthesis of a Finite Complexity Ordering for Saturation. [Research Report] IRIT - Institut de recherche en informatique de Toulouse; LORIA (Université de Lorraine, CNRS, INRIA). 2012. ⟨hal-00675954v2⟩



Record views


Files downloads