cl-banner

The Z Property

Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, and Christian Sternagel

The Archive of Formal Proofs, 2016.

Abstract

We formalize the Z property introduced by Dehornoy and van Oostrom. First we show that for any abstract rewrite system, Z implies confluence. Then we give two examples of proofs using Z: confluence of lambda-calculus with respect to beta-reduction and confluence of combinatory logic.

 

  PDF  |    AFP entry

BibTeX 

@article{BFJNVOCS-AFP15a,
author = "Bertram Felgenhauer and Julian Nagele and Vincent van Oostrom and Christian Sternagel",
title = "The {Z} Property",
journal = "Archive of Formal Proofs",
year = 2016,
note = "\url{https://www.isa-afp.org/entries/Rewriting_Z.html}, Formal proof development",
ISSN = "2150-914x",
}
Nach oben scrollen