Certified Ordered Completion
Christian Sternagel, Sarah Winkler
TL;DR
This paper presents a formally verified certifier for ordered completion proofs in Isabelle/HOL, enhancing the reliability of automated equational theorem proving tools by validating their proof certificates.
Contribution
It introduces a formalization of ordered rewriting and completion in Isabelle/HOL along with a verified certifier for proof certificates, improving tool reliability.
Findings
Verified certifier increases proof validation reliability
Formalization reduces errors in ordered completion processes
Enhances trustworthiness of automated theorem proving tools
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.
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
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge