Program Synthesis from Natural Deduction Proofs

Goto, Shigeki

Program Synthesis from Natural Deduction Proofs

Download BibTeX Cite

Proceedings of the Sixth International Joint Conference on Artificial Intelligence. .

Abstract

There have already been many program synthesizers which are based on classical logic . There is, however, some evidence that intuitionistic logic is more suitable for computer programs. This paper presents a program synthesis method based on intuitionistic logic. The synthesizing method is essentially an application of ~del's interpretation. An experimental program synthesizer NJL, which performs ~del's interpretation, is implemented in LISP. NJL takes natural deduction proofs as input and produces LISP programs.

Shigeki Goto. 1979. Program Synthesis from Natural Deduction Proofs. In Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79. IJCAI, https://ijcai.org/proceedings/1979/74

@inproceedings{ijcai1979p74,
  title     = {Program Synthesis from Natural Deduction Proofs},
  author    = {Goto, Shigeki},
  booktitle = {Proceedings of the Sixth International Joint Conference on
               Artificial Intelligence, {IJCAI-79}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Bruce G. Buchanan},
  year      = {1979},
  month     = {8},
  url       = {https://ijcai.org/proceedings/1979/74},
}

TY  - CPAPER
TI  - Program Synthesis from Natural Deduction Proofs
AU  - Goto, Shigeki
T2  - Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1979
UR  - https://ijcai.org/proceedings/1979/74
ER  -