Synthesis by completion
Nachum Dershowitz · International Joint Conference on Artificial Intelligence · 1985
The Knuth-Bendix completion procedure was introduced as a means of deriving canonical term-rewriting systems to serve as decision procedures for given equational theories. The procedure generates new rewrite rules to resolve ambiguities resulting from existing rules that overlap. We propose using this procedure to synthesize logic programs, as well as functional programs, from specifications and domain knowledge expressed as equivalence-preserving rewrite rules. An implementation is underway.