Diferencia entre revisiones de «A Formalization of Abstract Properties of Confluent Reductions in PVS»

Revisión del 11:37 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 Version PVS-3.2 here. Version PVS-4.2 here.
Documentation:	A Formalization of Abstract Properties of Confluent Reductions in PVS.

@@ Línea 12: / Línea 12: @@
 | 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:'''
+| '''Code:'''
-| You can find the PVS theories  [http://www.cs.us.es/~mjoseh/pub/FM.tgz here].
+| You can find the PVS theories
+* Version PVS-3.2 [http://www.cs.us.es/~mjoseh/pub/FM.tgz here].
+* Version PVS-4.2 [http://www.cs.us.es/~mjoseh/pub/FM_4.2.tgz here].
 |-
 | '''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].
 |}