Résumé de rapport du LIF


Rapport 27-2005
Solange Coupet-Grimal and William Delobel
An Effective Proof of the Well-Foundedness of the Multiset Path Ordering


Téléchargement / Download : pdf 144k , ps.gz 132k , bibtex

Abstract

The contribution of this paper is an effective proof of the well-founded\-ness 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.

Keywords

Termination, well-foundedness, proof-assistant.

Résumé

La contribution de cet article est une preuve effective de la bonne fondation de l'ordre récursif multi-ensemble sur les chemins (Multiset Path Ordering (MPO)), comme terme du Calcul des Constructions Inductives. Cette preuve est directe, courte et simple. Elle ne fait appel qu'à des résultats préliminaires élémentaires et s'applique à des termes contenant des variables, construits sur une signature non nécessairement finie de symboles fonctionnels d'arité variable. Toutes les preuves présentées ici ont été vérifiées par l'assistant de preuves Coq.

Mots clés

Terminaison, bonne fondation, assistant de preuves.

Bibtex

@TECHREPORT{27-2005,
    AUTHOR	= {Solange Coupet-Grimal and William Delobel},
    TITLE	= {{An Effective Proof of the Well-Foundedness of the Multiset Path Ordering }},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {27-2005},
    MONTH	= {December},
    YEAR	= {2005},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/27-2005.html},
}

[css]   [GenRap] [xhtml] Direction : François Denis - Secrétariat de direction : Martine Quessada
Tel. 04 91 11 36 00 - Fax : 04 91 11 36 02 - Mel. Martine.Quessada@cmi.univ-mrs.fr

webmaster - La dernière mise à jour de cette page date du 04 septembre 2008