Résumé de rapport du LIF

Téléchargement / Download : pdf 152k , ps.gz 136k , bibtex

Abstract

We give an axiomatization of Recursive Path Orders in the Calculus of Inductive Constructions. Then, we show that they are monotonic strict partial orders, and that they are well-founded. The proof of the well-foundedness is particularly short and elementary. Finally, we produce three relations that are proved to model the axiomatization: the Multiset Path Ordering, the Lexicographic Path Ordering, and the Recursive Path Ordering with status.

All this work is implemented in the Coq proof assistant.

Keywords

Term Rewriting Systems, Termination, Constructive Proofs, Theorem Proving, Coq.

Résumé

Nous présentons une axiomatisation constructive des Ordres Récursifs sur les Chemins. Puis, nous démontrons que ce sont des ordres stricts, monotones et bien-fondés. La preuve de bonne fondation est particulièrement courte et élémentaire. Enfin, nous produisons trois modèles: l'ordre multi-ensemble sur les chemins, l'ordre lexicographique sur les chemins, et l'ordre récursif sur les chemins avec status.

Tout ce travail est implémenté dans l'assistant de preuves Coq.

Mots clés

Systèmes de réécriture sur les termes, Terminaison, Preuves constructives, Assistant de preuves, Coq.

Bibtex

@TECHREPORT{28-2006,
    AUTHOR	= {Solange Coupet-Grimal and William Delobel},
    TITLE	= {{A Constructive Axiomatization of the Recursive Path Ordering}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {28-2006},
    MONTH	= {January},
    YEAR	= {2006},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/28-2006.html},
}