Recording completion for finding and certifying proofs in equational logic

Solving the word problem requires to decide whether an equation s ≈ t follows from an equa-tional system (ES) E. By Birkhoff’s theorem this is equivalent to the existence of a conversion s ↔∗E t. Knuth-Bendix completion [5] (if successful) gives a decision procedure: If an ES E is transformed into an equivalent convergent term rewrite system (TRS) R, then s ↔∗E t iff th