| 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.
|
