A Deductive Approach to Program Synthesis

ABSTRACT

Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs. This approach regards program synthesis as a theorem-proving task and relies on a theorem-proving method that combines the features of transformation rules, unification, and mathematical induction within a single framework.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	BLEDSOE, W.W. Non-resolution theorem proving. Artif. Intell. J. 9, (1977), 1-35.
	2	Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
	3	R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
	4	DARLINGTON, J.L. Automatic theorem proving with equality substitutions and mathematical induction. Machine Intell. 3 (Edinburgh, Scotland) (1968), 113-127.
	5	GREEN, C.C. Application of theorem proving to problem solving, in Proc. Int. Joint Conf. on Artificial Intelligence (Washington D.C., May 1969), 219-239.
	6	HEWiTT, C. Description and theoretical analysis (using schemata) of PLANNER: A language for proving theorems and manipulating models in a robot. Ph.D. Diss., M.I.T., Cambridge, Mass., 1971.
	7	MANNA, Z., AND WALDiNGER, R. Synthesis: dreams ~ programs, iEEE Trans. Sofiw. Eng. SE-5, 4 (July 1979), 294-328.
	8	MURRAY, N. A proof procedure for non-clausal fwst-order logic. Tech. Rep. Syracuse Univ., Syracuse, N.Y., 1978.
	9	Greg Nelson , Derek C. Oppen, A simplifier based on efficient decision algorithms, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-150, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512775]
	10	NiLSSON, N.J. A production system for automatic deduction. Machine Intell. 9, Ellis Horwood, Chichester, England, 1979.
	11	Nils J. Nilsson, Problem-Solving Methods in Artificial Intelligence, McGraw-Hill Pub. Co., 1971
	12	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	13	WALDINGER, R.J., A~o LEE, R.C.T. PROW: A step toward automatic program writing. In Proc. Int. Joint Conf. on Artificial Intelligence (Washington D.C., May 1969), pp. 241-252.
	14	WILKI~S, D. QUEST--A non-clausal theorem proving system. M.Sc. Th., Univ. of Essex, England, 1973.