使用ConCon 1.5的认证非合流性
计算机科学中的逻辑
2017-09-18 v1
摘要
我们提出三种检测CTRSs(条件项重写系统)非合流性的方法：(1) 针对4-CTRSs的特设方法，(2) 针对无条件临界对的专业方法，以及(3) 采用条件窄化来寻找非合流性见证的方法。我们简要描述了在ConCon中这些方法的实现，随后考察其通过CeTA的认证，最后以在合流问题数据库(Cops)上的实验作结。
引用
@article{arxiv.1709.05162,
title = {Certified Non-Confluence with ConCon 1.5},
author = {Thomas Sternagel and Christian Sternagel},
journal= {arXiv preprint arXiv:1709.05162},
year = {2017}
}
备注
5 pages