Zohar Manna
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.
- 1 BLEDSOE, W.W. Non-resolution theorem proving. Artif. Intell. J. 9, (1977), 1-35.Google Scholar
- 2 BoYER, R.S., AND MOOI~R, JS. Proving theorems about LISP functions J. ACM 22, 1 (Jan. 1975), 129-144. Google Scholar
- 3 BURSTALL, R.M., AND DARLINGTON, J. A transformation system for developing recursive programs. J. ACM 24, 1 (Jan. 1977), 44-67. Google Scholar
- 4 DARLINGTON, J.L. Automatic theorem proving with equality substitutions and mathematical induction. Machine Intell. 3 (Edinburgh, Scotland) (1968), 113-127.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 7 MANNA, Z., AND WALDiNGER, R. Synthesis: dreams ~ programs, iEEE Trans. Sofiw. Eng. SE-5, 4 (July 1979), 294-328.Google Scholar
- 8 MURRAY, N. A proof procedure for non-clausal fwst-order logic. Tech. Rep. Syracuse Univ., Syracuse, N.Y., 1978.Google Scholar
- 9 NELSON, G., AND OPPEN, D.C. A simplifier based on efficient decision algorithms. In Proc. 5th ACM Syrup. Principles of Programming Languages (Tucson, Ariz., Jan. 1978), pp. 141-150. Google Scholar
- 10 NiLSSON, N.J. A production system for automatic deduction. Machine Intell. 9, Ellis Horwood, Chichester, England, 1979.Google Scholar
- 11 NXLSSON, N.J. Problem-solving methods in artificial intelligence. McGraw-Hill, New York, 1971, pp. 165-168. Google Scholar
- 12 ROBINSON, J.A. A machine-oriented logic based on the resolution principle. J.4CM 12, 1 (Jan. 1965), 23-41. Google Scholar
- 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.Google Scholar
- 14 WILKI~S, D. QUEST--A non-clausal theorem proving system. M.Sc. Th., Univ. of Essex, England, 1973.Google Scholar
Index Terms
- A Deductive Approach to Program Synthesis
Recommendations
Fundamentals of Deductive Program Synthesis
An informal tutorial for program synthesis is presented, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, the authors prove the existence of an object meeting the specified ...
Reconciling enumerative and deductive program synthesis
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationSyntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate ...
Comments