Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»
Línea 17: | Línea 17: | ||
|- | |- | ||
| '''Abstract:''' | | '''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 | + | | 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 [http://portal.acm.org/ft_gateway.cfm?id=322230&type=pdf Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems] of G. Huet. |
|- | |- | ||
| '''Code:''' | | '''Code:''' |
Revisión del 19:53 1 jun 2010
- Title: A Formalization of Abstract Properties of Confluent Reductions in PVS
- Autores: José A. Alonso y María J. Hidalgo.
- 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:
Title: | A Formalization of Abstract Properties of Confluent Reductions in PVS |
Autores: | José A. Alonso y María J. Hidalgo. |
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: | ... |