Certified Equational Reasoning via Ordered Completion

Christian Sternagel and Sarah Winkler

27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 508 – 525, 2019.


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.


  PDF |    doi:10.1007/978-3-030-29436-6_30  


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"
Nach oben scrollen