Abstract

On the one hand, equational reasoning is a fundamental part of automated theorem proving with ordered completion as a key technique. On the other hand, the complexity of corresponding, often highly optimized, automated reasoning tools makes implementations inherently error-prone. As a remedy, we provide a formally verified certifier for ordered completion based techniques. This certifier is code generated from an accompanying Isabelle/HOL formalization of ordered rewriting and ordered completion incorporating an advanced ground joinability criterion. It allows us to rigorously validate generated proof certificates from several domains: ordered completion, satisfiability in equational logic, and confluence of conditional term rewriting.

BibTeX

@inproceedings{CSSW-CADE19,
 author    = "Christian Sternagel and Sarah Winkler",
 title     = "Certified Equational Reasoning via Ordered Completion",
 booktitle = "Proceedings of the 27th International Conference on
              Automated Deduction",
 editor    = "Pascal Fontaine",
 series    = "Lecture Notes in Computer Science",
 volume    = 11716,
 pages     = "508--525",
 year      = 2019,
 doi       = "10.1007/978-3-030-29436-6_30"
}