Sciweavers

Share
AAECC
2006
Springer

An effective proof of the well-foundedness of the multiset path ordering

9 years 4 months ago
An effective proof of the well-foundedness of the multiset path ordering
The contribution of this paper is an effective proof of the well-foundedness of MPO, as a term of the Calculus of Inductive Constructions. This proof is direct, short and simple. It is a sequence of nested inductions and it only requires as preliminary results the transitivity of MPO and the fact that finite multisets whose elements are accessible for the basic relation are themselves accessible for the multiset order. The terms we consider are not supposed to be ground nor the signature to be finite. All the proofs have been carried out in the Coq proof-assistant
Solange Coupet-Grimal, William Delobel
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2006
Where AAECC
Authors Solange Coupet-Grimal, William Delobel
Comments (0)
books