Reducing Rewrite Properties to Properties on Ground Terms

Alexander Lochmann 📧

June 2, 2022


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


Session Rewrite_Properties_Reduction