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

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00675954
Contributeur : Mounira Kourjieh <>
Soumis le : vendredi 9 mars 2012 - 12:17:03
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 11:40:38

Fichiers

Paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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

Citation

Yannick Chevalier, Mounira Kourjieh. Automated Synthesis of a Finite Complexity Ordering for Saturation. [Research Report] 2012. 〈hal-00675954v2〉

Partager

Métriques

Consultations de la notice

304

Téléchargements de fichiers

139