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.

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: