Level-Confluence of 3-CTRSs in Isabelle/HOL
Logic in Computer Science
2016-02-24 v1
Abstract
We present an Isabelle/HOL formalization of an earlier result by Suzuki, Middeldorp, and Ida; namely that a certain class of conditional rewrite systems is level-confluent. Our formalization is basically along the lines of the original proof, from which we deviate mostly in the level of detail as well as concerning some basic definitions.
Cite
@article{arxiv.1602.07115,
title = {Level-Confluence of 3-CTRSs in Isabelle/HOL},
author = {Christian Sternagel and Thomas Sternagel},
journal= {arXiv preprint arXiv:1602.07115},
year = {2016}
}
Comments
In Proceedings of the 4th International Workshop on Confluence (IWC 2015)