A Formalization of Abstract Properties of Confluent Reductions in PVS
Revisión del 17:05 1 jun 2010 de Mjoseh (discusión | contribuciones)
- Title: A Formalization of Abstract Properties of Confluent Reductions in PVS
- Autores:
- Fecha de realización: Diciembre 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: