---
title: "Synthesis by Completion"
authors:
  - "Nachum Dershowitz"
doi: ""
url: "https://ijcai.org/proceedings/1985/38"
pdf: "https://ijcai.org/proceedings/1985/0038.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "208-213"
track: "Automatic Programming"
keywords:
---

# Synthesis by Completion

Nachum Dershowitz

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 208-213.

## Abstract

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 synth es ize logic programs, as well as functional programs, from specifications and domain knowledge expressed as equivalencepreserving rewrite rules. An implementation is underway.