Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»
| Línea 4: | Línea 4: | ||
|- | |- | ||
| '''Authors:''' | | '''Authors:''' | ||
| − | | {{jalonso}} | + | | {{jalonso}} and {{mjoseh}}. |
|- | |- | ||
| '''Date:''' | | '''Date:''' | ||
| Línea 16: | Línea 16: | ||
|- | |- | ||
| '''Documentation:''' | | '''Documentation:''' | ||
| − | | | + | | [http://www.cs.us.es/~mjoseh/pub/2010-A_Formalization_of_Abstract_Properties_of_Confluent_Reductions_in_PVS.pdf A Formalization of Abstract Properties of Confluent Reductions in PVS]. |
| − | |||
| − | |||
| − | |||
|} | |} | ||
Revisión del 10:47 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 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 in ... |
| Documentation: | A Formalization of Abstract Properties of Confluent Reductions in PVS. |
