Diferencia entre revisiones de «PROTEMO»
(New page: * '''Title:''' Proving termination with multiset orderings in PVS: theory,methodology and applications * '''Autores:''' {{jalonso}}, {{mjoseh}} y {{fjesus}}. * '''Fecha de realización:'''...) |
(Sin diferencias)
|
Revisión actual del 18:02 1 jun 2010
- 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:
