Inductive completion for transformation of equational specifications

Abstract

The Knuth-Bendix completion procedure is a tool for algorithmically completing term rewriting systems which are operationally incomplete in the sense that the uniqueness of normal forms is not guaranteed. As the problem of operational completeness is undecidable, one may only expect a technique applicable to an enumerable number of cases. The Knuth-Bendix completion procedure may fail either by generating a critical pair which can not be oriented to form a new rewrite rule or by generating an infinite sequence of critical pairs to be introduced as new rewrite rules. The latter case is investigated. The basic idea is to invoke inductive inference techniques for abbreviating infinitely long sequences of rules by finitely many other rules. If simple syntactic generalization does not do, there will be automatically generated auxiliary operators. This is the key idea of the present paper. It contains a calculus of five learning rules for extending Knuth-Bendix completion procedures by inductive inference techniques. These rules are shown to be correct. The problem of completeness remains open.