PROTEMO
De WikiGLC
- Title: Proving termination with multiset orderings in PVS: theory,methodology and applications
- Autores: José A. Alonso, María J. Hidalgo y Plantilla:Fjesus.
- Fecha de realización: Noviembre de 2009.
- Abstract: This theory is a simple and smart formalization of abstract confluence properties such Newman's Lemma or the Church-Rosser property. This formalization is based on the paper "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems " of G. Huet.
- Code: La formalización en PVS se encuentra en ...
- Documentation:
