cl-banner

Certified Ordered Completion

Christian Sternagel, Sarah Winkler

Proceedings of the 7th International Workshop on Confluence (IWC 2018),  2018.

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.

 

  PDF

BibTeX 

@inproceedings{CSSW-IWC18,
author = "Christian Sternagel and Sarah Winkler",
title = "Certified Ordered Completion",
booktitle = "Proceedings of the 7th International Workshop on Confluence",
year = 2018
}
Nach oben scrollen