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

DOI10.1007/s00200-006-0020-yzbMath1107.68045OpenAlexW2018387388MaRDI QIDQ857884

Solange Coupet-Grimal, William Delobel

Publication date: 5 January 2007

Published in: Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00200-006-0020-y

zbMATH Keywords

terminationconstructive logicwell-foundednesscalculus of inductive constructionsmultiset path order

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Coq formalization of the higher-order recursive path ordering, An effective proof of the well-foundedness of the multiset path ordering, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Uses Software

• Coq
• CoLoR

Cites Work

• Orderings for term-rewriting systems
• An effective proof of the well-foundedness of the multiset path ordering
• An intuitionistic proof of Kruskal's theorem
• Structural Analysis of Narratives with the Coq Proof Assistant
• Term Rewriting and All That
• Computer Science Logic
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item