%0 Journal Article
%T Recording Completion for Finding and Certifying Proofs in Equational Logic
%A Thomas Sternagel
%A Ren¨¦ Thiemann
%A Harald Zankl
%A Christian Sternagel
%J Computer Science
%D 2012
%I arXiv
%X 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.
%U http://arxiv.org/abs/1208.1597v1