A Formalization of Abstract Properties of Confluent Reductions in PVS
Revisión del 11:59 7 oct 2010 de Mjoseh (discusión | contribuciones)
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. |