Completion as a Derived Rule of Inference
A simple first step in the investigation of term rewriting systems in
higher order logic is to just insert the first order Knuth-Bendix
completion algorithm unchanged into the more complicated logic. This
paper presents the details of how this is done in Mike Gordon's HOL
system, an implementation of Church's Simple Type Theory. We present
completion as a derived rule of inference, not (as usual) as an ad
hoc procedure. The completion rule presented here is easily
adaptable to other natural deduction logics with equality.
This paper was written circa 1990 but never published, except as a
University of Calgary technical report (number 90/409/33). However, the
implementation described in the paper is still distributed with the HOL
system; it can be found in the contrib/knuth_bendix
directory.
paper