Automated Synthesis of a Finite Complexity Ordering for Saturation - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2012

Automated Synthesis of a Finite Complexity Ordering for Saturation

(1, 2) , (3)
1
2
3

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.
Fichier principal
Vignette du fichier
Paper.pdf (187.85 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00675954 , version 1 (02-03-2012)
hal-00675954 , version 2 (09-03-2012)

Identifiers

Cite

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⟩
249 View
390 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More