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 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.
Type de document :
[Research Report] 2012
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger
Contributeur : Mounira Kourjieh <>
Soumis le : vendredi 9 mars 2012 - 12:17:03
Dernière modification le : mardi 18 décembre 2018 - 16:38:25
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 11:40:38


Fichiers produits par l'(les) auteur(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] 2012. 〈hal-00675954v2〉



Consultations de la notice


Téléchargements de fichiers