Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»
| Línea 14: | Línea 14: | ||
| '''Code:''' | | '''Code:''' | ||
| You can find the PVS theories | | You can find the PVS theories | ||
| − | * [http://www.cs.us.es/~mjoseh/pub/FM.tgz Version PVS-3.2]. | + | * [http://www.cs.us.es/~mjoseh/pub/TeoriasPVS/Version_PVS-3.2/FM.tgz Version PVS-3.2]. |
* [http://www.cs.us.es/~mjoseh/pub/FM_4.2.tgz Version PVS-4.2]. | * [http://www.cs.us.es/~mjoseh/pub/FM_4.2.tgz Version PVS-4.2]. | ||
|- | |- | ||
Revisión del 12:09 7 oct 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. |
| Code: | You can find the PVS theories |
| Documentation: | A Formalization of Abstract Properties of Confluent Reductions in PVS. |
