Reducing Rewrite Properties to Properties on Ground Terms

Alexander Lochmann

2 June 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

Depends On

Topics

Theories

Cite

×
@article{Rewrite_Properties_Reduction-AFP,
  author  = {Alexander Lochmann},
  title   = {Reducing Rewrite Properties to Properties on Ground Terms},
  journal = {Archive of Formal Proofs},
  month   = June,
  year    = 2022,
  note    = {\url{http://isa-afp.org/entries/Rewrite_Properties_Reduction.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download