Abstract

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

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
}