A Formalization of Abstract Properties of Confluent Reductions in PVS

De WikiGLC
Revisión del 16:59 1 jun 2010 de Mjoseh (discusión | contribuciones) (New page: {| border="1" | Title | A Formalization of Abstract Properties of Confluent Reductions in PVS |- | Abstract | This theory is a simple and smart formalization of abstract confluence propert...)
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)
Saltar a: navegación, buscar
Title A Formalization of Abstract Properties of Confluent Reductions in PVS
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.