2016/02/23 by Christian Sternagel, Sternagel, Christian, Thomas Sternagel +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1602.07115
In Proceedings of the 4th International Workshop on Confluence (IWC 2015)
arxiv created 2016/02/23 · arxiv updated 2016/02/24
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.