Certified Non-Confluence with ConCon 1.5
Thomas Sternagel, Christian Sternagel
TL;DR
This paper introduces three methods for verifying non-confluence in conditional term rewriting systems, implemented in ConCon, and validated through experiments and certification with CeTA.
Contribution
It presents novel methods for non-confluence checking in CTRSs, including specialized and narrowing-based approaches, with implementation and experimental validation.
Findings
Effective non-confluence detection methods demonstrated
Implementation in ConCon verified with CeTA
Experimental results on confluence problems database
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).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDigital and Cyber Forensics · Data Quality and Management · Anomaly Detection Techniques and Applications