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

• Type: Journal
• Year: 2006
• Where: AAECC
• Authors: Solange Coupet-Grimal, William Delobel
• Keywords: AAECC 2006, Algorithms, Effective Proof, Inductive Constructions, Multiset