ML Anthology

Synthesis by Completion

Nachum Dershowitz
IJCAI 1985 pp. 208-214
doi:10.1016/j.amjms.2021.02.021 /ijcai/1985/dershowitz1985ijcai-synthesis/

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 synthesize logic programs, as well as functional programs, from specifications and domain knowledge expressed as equivalence-preserving rewrite rules. An implementation is underway.

PDF Semantic Scholar

Cite

Text

Dershowitz. "Synthesis by Completion." International Joint Conference on Artificial Intelligence, 1985. doi:10.1016/j.amjms.2021.02.021

Markdown

[Dershowitz. "Synthesis by Completion." International Joint Conference on Artificial Intelligence, 1985.](https://mlanthology.org/ijcai/1985/dershowitz1985ijcai-synthesis/) doi:10.1016/j.amjms.2021.02.021

BibTeX

@inproceedings{dershowitz1985ijcai-synthesis,
  title     = {{Synthesis by Completion}},
  author    = {Dershowitz, Nachum},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1985},
  pages     = {208-214},
  doi       = {10.1016/j.amjms.2021.02.021},
  url       = {https://mlanthology.org/ijcai/1985/dershowitz1985ijcai-synthesis/}
}