Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»
Línea 10: | Línea 10: | ||
|- | |- | ||
| '''Description:''' | | '''Description:''' | ||
− | | 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. | + | | This theory is a simple and smart formalization of abstract confluence properties such as 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. |
|- | |- | ||
| '''PVS Theories:''' | | '''PVS Theories:''' |
Revisión del 15:25 2 jun 2010
Title: | A Formalization of Abstract Properties of Confluent Reductions in PVS |
Authors: | José A. Alonso and María J. Hidalgo. |
Date: | December 2009. |
Description: | This theory is a simple and smart formalization of abstract confluence properties such as 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. |
PVS Theories: | You can find the PVS theories here. |
Documentation: | A Formalization of Abstract Properties of Confluent Reductions in PVS. |