Reducing Rewrite Properties to Properties on Ground Terms

Alexander Lochmann 📧

June 2, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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