Certified Non-Confluence with ConCon 1.5
Logic in Computer Science
2017-09-18 v1
Abstract
We present three methods to check CTRSs for non-confluence: (1) an ad hoc method for 4-CTRSs, (2) a specialized method for unconditional critical pairs, and finally, (3) a method that employs conditional narrowing to find non-confluence witnesses. We shortly describe our implementation of these methods in ConCon, then look into their certification with CeTA, and finally conclude with experiments on the confluence problems database (Cops).
Cite
@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}
}
Comments
5 pages