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.

License

BSD License

Topics

Session Rewrite_Properties_Reduction

Depends on

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{https://isa-afp.org/entries/Rewrite_Properties_Reduction.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: