Recording Completion for Finding and Certifying Proofs in Equational Logic
Logic in Computer Science
2012-08-09 v1
Abstract
When we want to answer/certify whether a given equation is entailed by an equational system we face the following problems: (1) It is hard to find a conversion (but easy to certify a given one). (2) Under the assumption that Knuth-Bendix completion is successful, it is easy to decide the existence of a conversion but hard to certify this decision. In this paper we introduce recording completion, which overcomes both problems.
Cite
@article{arxiv.1208.1597,
title = {Recording Completion for Finding and Certifying Proofs in Equational Logic},
author = {Thomas Sternagel and René Thiemann and Harald Zankl and Christian Sternagel},
journal= {arXiv preprint arXiv:1208.1597},
year = {2012}
}
Comments
pages 6, International Workshop on Confluence 2012