---
title: "Automatic Program Synthesis in Second-Order Logic"
authors:
  - "Jared L. Darlington"
doi: ""
url: "https://ijcai.org/proceedings/1973/67"
pdf: "https://ijcai.org/proceedings/1973/0067.pdf"
venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence"
year: 1973
pages: "537-541"
track: "Automatic Programming"
keywords:
---

# Automatic Program Synthesis in Second-Order Logic

Jared L. Darlington

*Proceedings of the Third International Joint Conference on Artificial Intelligence*, pages 537-541.

## Abstract

A resolution-based theorem prover, incorporating a restricted higher-order unification algorithm, has been applied to the automatic synthesis of SNOBOL-4 programs. The set of premisses includes second-order assignment and iteration axioms derived from those of Hoare. Two examples are given of the synthesis of programs that compute elementary functions.