A Deductive Approach to Program Synthesis
Tóm tắt
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.
Từ khóa
Tài liệu tham khảo
BLEDSOE , W.W. Non-resolution theorem proving. Artif. Intell. J. 9 , ( 1977 ), 1 - 35 . BLEDSOE, W.W. Non-resolution theorem proving. Artif. Intell. J. 9, (1977), 1-35.
DARLINGTON , J.L. Automatic theorem proving with equality substitutions and mathematical induction. Machine Intell. 3 (Edinburgh , Scotland) ( 1968 ), 113-127. DARLINGTON, J.L. Automatic theorem proving with equality substitutions and mathematical induction. Machine Intell. 3 (Edinburgh, Scotland) (1968), 113-127.
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 . 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.
HEW i TT, 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 . 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.
MANNA , Z. , AND WALD i NGER , R. Synthesis: dreams ~ programs, i EEE Trans. Sofiw. Eng. SE-5 , 4 ( July 1979 ), 294 - 328 . MANNA, Z., AND WALDiNGER, R. Synthesis: dreams ~ programs, iEEE Trans. Sofiw. Eng. SE-5, 4 (July 1979), 294-328.
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 . 10.1145/512760.512775 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. 10.1145/512760.512775
Ni LSSON , N.J. A production system for automatic deduction. Machine Intell. 9 , Ellis Horwood , Chichester, England , 1979 . NiLSSON, N.J. A production system for automatic deduction. Machine Intell. 9, Ellis Horwood, Chichester, England, 1979.
NXLSSON , N.J. Problem-solving methods in artificial intelligence . McGraw-Hill , New York , 1971 , pp. 165 - 168 . NXLSSON, N.J. Problem-solving methods in artificial intelligence. McGraw-Hill, New York, 1971, pp. 165-168.
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 . 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.
WILKI~S , D. QUEST--A non-clausal theorem proving system. M.Sc. Th ., Univ. of Essex , England , 1973 . WILKI~S, D. QUEST--A non-clausal theorem proving system. M.Sc. Th., Univ. of Essex, England, 1973.