Zohar Manna
Abstract
An elementary outline of the theorem-proving approach to automatic program synthesis is given, without dwelling on technical details. The method is illustrated by the automatic construction of both recursive and iterative programs operating on natural numbers, lists, and trees.
In order to construct a program satisfying certain specifications, a theorem induced by those specifications is proved, and the desired program is extracted from the proof. The same technique is applied to transform recursively defined functions into iterative programs, frequently with a major gain in efficiency.
It is emphasized that in order to construct a program with loops or with recursion, the principle of mathematical induction must be applied. The relation between the version of the induction rule used and the form of the program constructed is explored in some detail.
- 1 Ashcroft, E. A. Mathematical logic applied to the semantics of computer programs. Ph.D. Thesis, 1970, Imperial College, London.Google Scholar
- 2 Brice, C., and Derksen, J. A heuristically guided equality rule in a resolution theorem prover. Tech. Note 45, Stanford Res. Inst., Artificial Intelligence Group, Menlo Park, Calif.Google Scholar
- 3 Burstall, R. M. Proving properties of programs by structural induction. Comp. J. 12, 1 (1969), 41---48.Google ScholarCross Ref
- 4 ----. Formal description of program structure and semantics in first-order logic. In Machine Intelligence 5, Meltzer and Michie, Eds., Edinburgh U. Press, Edinburgh, 1970, pp. 79-98.Google Scholar
- 5 Floyd, R. W. Assigning meaning to programs. In Proc. Symposia in Applied Mathematics, Vol. 19, American Mathematical Society, 1967, pp. 19-32.Google ScholarCross Ref
- 6 Green, C. Application of theorem proving to problem solving. Proc. International Joint Conf. on Artificial Intelligence, Washington, D.C., 1969.Google ScholarCross Ref
- 7 ----. The application of theorem proving to question-answering systems. Ph.D. Thesis, 1969, Stanford U., Standford, Calif. Google ScholarDigital Library
- 8 ----, and Raphael, B. The use of theorem-proving techniques in question-anwering systems. Proc. 23rd Nat. Conf. ACM. Brandon/Systems Press, Princeton, N. J., 1968. Google ScholarDigital Library
- 9 Hayes, P. J. A machine-oriented formulation of the extended functional calculus. Memo 62, Stanford Artificial Intelligence Proj., Stanford U., Stanford, Calif., 1969. Also appeared as Metamathematics Unit Report, U. of Edinburgh, Scotland.Google Scholar
- 10 King, J. A program verifier. Ph.D. Thesis, 1969, Carnegie-Mellon U., Pittsburgh, Pa. Google ScholarDigital Library
- 11 ----, and Floyd, R. W. Interpretation Oriented Theorem Prover Over Integers. Second Ann. ACM Symp. on Theory of Computing, Northampton, Mass., 1970. Google ScholarDigital Library
- 12 Luckham, D., and Nilsson, N. J. Extracting information from resolution proof trees. Tech. Note 32, Stanford Res. Inst., Artificial Intelligence Group, Menlo Park, Calif., 1970.Google Scholar
- 13 Manna, Z. The correctness of programs. J. Computer and System Sciences 3, 2, (1969), 119-127.Google ScholarDigital Library
- 14 ----, and McCarthy, J. Properties of programs and partial function logic. In Machine Intelligence 5, Meltzer and Michie, Eds., Edinburgh U. Press, Edinburgh, 1970, pp. 79-98.Google Scholar
- 15 ----, and Pnueli, A. Formalization of Properties of Functional Programs. J. ACM 17, 3 (1970), 555-569. Google ScholarDigital Library
- 16 McCarthy, J. Towards a mathematical science of computation. Proc. iviP Cong. 1962, North-Holland Pub. Co., Amsterdam.Google Scholar
- 17 ----. A Basis for a Mathematical Theory of Computation. In Computer Programming and Formal Systems, Braffort and Hirshberg, Eds., North Holland Pub. Co., Amsterdam, 1963.Google Scholar
- 18 ----. Predicate calculus with "undefined" as a truth-value. Memo 1, Stanford Artificial Intelligence Proj. Stanford U., 1963.Google Scholar
- 19 Mendelson, E. Introduction to Mathematical Logic. Van Nostrand, Princeton, N. J., 1964. Google ScholarDigital Library
- 20 Morris, J. B. E-resolution: extension of resolution to include the equality relation. Proc. International Joint Conf. on Artificial Intelligence, Washington, D. C., 1969.Google Scholar
- 21 Park, D. Fixpoint induction and proofs of program properties. In Machine Intelligence 5. Meltzer and Michie, Eds., Edinburgh U. Press, Edinburgh, pp. 59-78.Google Scholar
- 22 Patterson, M. S. and Hewitt, C. E. Comparative Schematology, Part 1. Artificial Intel. Memo No. 201, Mrr, 1970. Google ScholarDigital Library
- 23 Robinson, I. A machine-oriented logic based on the resolution principle. J. ACM 12, 1 (Jan. 1965), 23--41. Google ScholarDigital Library
- 24 Scott, D. A type-theoretical alternative to CUCH, ISWlM, OWHY. Unpublished memo, 1969.Google Scholar
- 25 Simon, H. Experiments with a heuristic compiler. J. ACM, 10, 4 (Oct. 1963), 493-506. Google ScholarDigital Library
- 26 Slagle, J. Experiments with a deductive question-answering program. Comm. ACM 8, 12 (Dec. 1965), 792-798. Google ScholarDigital Library
- 27 Strong, H. R. Translating recursion equations into flow charts. Second Ann. ACM Symp. on Theory of Computing, Northampton, Mass., 1970. Google ScholarDigital Library
- 28 Waldinger, R. J. Constructing programs automatically using theorem proving. Ph.D. Thesis, 1969, Carnegie-Mellon U., Pittsburgh, Pa.Google Scholar
- 29 ----, and Lee, R. C. T. PROW: a step toward automatic program writing. Proc. International Joint Conf. on Artificial Intelligence, Washington, D.C., 1969.Google Scholar
Index Terms
- Toward automatic 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 ...
Program Synthesis in Saturation
Automated Deduction – CADE 29AbstractWe present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both ...
Automatic program synthesis in second-order logic
IJCAI'73: Proceedings of the 3rd international joint conference on Artificial intelligenceA 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 ...
Comments