Isabelle/HOL中3-CTRSs的层级合流
计算机科学中的逻辑
2016-02-24 v1
摘要
我们给出了Suzuki、Middeldorp和Ida早期结果的一个Isabelle/HOL形式化；即某一类条件重写系统是层级合流的。我们的形式化基本遵循原始证明的思路，主要在细节程度以及一些基本定义方面有所偏离。
引用
@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}
}
备注
In Proceedings of the 4th International Workshop on Confluence (IWC 2015)