PROTEMO
Revisión del 19:02 1 jun 2010 de Mjoseh (discusión | contribuciones) (New page: * '''Title:''' Proving termination with multiset orderings in PVS: theory,methodology and applications * '''Autores:''' {{jalonso}}, {{mjoseh}} y {{fjesus}}. * '''Fecha de realización:'''...)
- 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:
