Reducing Rewrite Properties to Properties on Ground Terms

Alexander Lochmann 📧

June 2, 2022

Abstract

This AFP entry relates important rewriting properties between the set of terms and the set of ground terms induced by a given signature. The properties considered are confluence, strong/local confluence, the normal form property, unique normal forms with respect to reduction and conversion, commutation, conversion equivalence, and normalization equivalence.
BSD License

Topics

Theories of Rewrite_Properties_Reduction