A Formalization of Abstract Properties of Confluent Reductions in PVS

De WikiGLC
Saltar a: navegación, buscar
Title: A Formalization of Abstract Properties of Confluent Reductions in PVS
Autores: José A. Alonso y María J. Hidalgo.
Fecha de realización: Diciembre de 2009.
Abstract: 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.
Code: La formalización en PVS se encuentra en ...
Documentation: ...