Certified Ordered Completion
Logic in Computer Science
2018-05-28 v1
Abstract
On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we give an Isabelle/HOL formalization of ordered rewriting and completion that comes with a formally verified certifier for ordered completion proofs. By validating generated proof certificates, our certifier increases the reliability of ordered completion tools.
Cite
@article{arxiv.1805.10090,
title = {Certified Ordered Completion},
author = {Christian Sternagel and Sarah Winkler},
journal= {arXiv preprint arXiv:1805.10090},
year = {2018}
}
Comments
accepted at 7th International Workshop on Confluence 2018