  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.
