cl-banner

Recording Completion for Finding and Certifying Proofs in Equational Logic

Thomas Sternagel, René Thiemann, Harald Zankl, and Christian Sternagel

Proceedings of the 1st International Workshop on Confluence (IWC 2012), pp. 31 – 36, 2012.

Abstract

We introduce recording completion, a variant of Knuth-Bendix completion, facilitating certification and the construction of proof trees in equational logic.

 

  PDF

BibTeX 

@inproceedings{TSRTHZCS-IWC12,
author = "Thomas Sternagel and Ren{\'e} Thiemann and Harald Zankl and Christian Sternagel",
title = "Recording Completion for Finding and Certifying Proofs in Equational Logic",
booktitle = "Proceedings of the 1st International Workshop on Confluence",
pages = "31--36",
year = 2012
}
Nach oben scrollen