Completion procedures as transition rules + Control

Abstract

A description of the completion of a set of identities by a set of inference rules has allowed recent progresses in proving its completeness. But there existed no attempt to use this description in an actual implementation. This paper shows that this is feasible using a functional programming language namely CAML. The implementation uses a toolkit, a set of transition rules and a short procedure for describing the control. A major role is played by the data structure on which both the transition rules and the control operate. Three versions of the classical Knuth-Bendix completion and two versions of the unfailing completion are proposed.