
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Z. Manna, R. Waldinger, "Fundamentals of Deductive Program Synthesis," IEEE Transactions on Software Engineering, vol. 18, no. 8, pp. 674704, August, 1992.  
BibTex  x  
@article{ 10.1109/32.153379, author = {Z. Manna and R. Waldinger}, title = {Fundamentals of Deductive Program Synthesis}, journal ={IEEE Transactions on Software Engineering}, volume = {18}, number = {8}, issn = {00985589}, year = {1992}, pages = {674704}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.153379}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Fundamentals of Deductive Program Synthesis IS  8 SN  00985589 SP674 EP704 EPD  674704 A1  Z. Manna, A1  R. Waldinger, PY  1992 KW  deductive program synthesis; specification; proof; deductivetableau system; theoremproving framework; nonclausal resolution rule; reasoning; induction rule; artificial intelligence; formal specification; inference mechanisms; program testing; theorem proving VL  18 JA  IEEE Transactions on Software Engineering ER   
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 conditions. The proof is restricted to be sufficiently constructive, in the sense that, in establishing the existence of the desired output, the proof is forced to indicate a computational method for finding it. That method becomes the basis for a program that can be extracted from the proof. The exposition is based on the deductivetableau system, a theoremproving framework particularly suitable for program synthesis. The system includes a nonclausal resolution rule, facilities for reasoning about equality, and a wellfounded induction rule.
[1] P. B. Andrews "Theorem proving via general matings,"J. ACM, vol. 28, no. 2, pp. 193214, 1981.
[2] W. Bibel, "Matings in matrices,"Commun. ACM, vol. 26, pp. 844852, 1983.
[3] R. M. Burstall and J. Darlington, "A transformation system for developing recursive programs,"J. ACM, vol. 24, no. 1, pp. 4467, Jan. 1977.
[4] W. W. Bledsoe and L. Hines, "Variable elimination and chaining in a resolutionbased prover for inequalities," inProc. 5th Conf. on Auto. Deduction, 1980, pp. 281292.
[5] R. S. Boyer and J. S. Moore,A Computational Logic. New York: Academic Press, 1979.
[6] R. Burback,et al., "Using the deductive tableau system," inMacintosh Educational Software Collection, Chariot Software Group, 1990.
[7] R. L. Constableet al., Implementing Mathematics with the Nuprl Proof Development System. Englewood Cliffs, NJ: PrenticeHall, 1986.
[8] T. Coquand and G. Huet, "The calculus of constructions,"Inform. Contr., vol. 76, nos. 2/3, pp. 95120, 1988.
[9] N. Dershowitz,The Evolution of Programs. Boston, MA: Birkhäuser, 1983.
[10] E. W. Dijkstra,A Discipline of Programming. Englewood Cliffs, NJ: PrenticeHall, 1976.
[11] E. Eder, "Properties of substitutions and unifications,"J. Symbolic Comput., vol. 1, pp. 3146, 1985.
[12] M. Fay, "Firstorder unification in an equational theory," inProc. 4th Conf. on Auto. Deduction, 1979, pp. 161167.
[13] A. Felty and D. Miller, "Specifying theorem provers in a higherorder logic programming language," inProc. 9th Int. Conf. on Auto. Deduction, 1988, pp. 6180.
[14] M. J. Gordon, A. J. Milner, and C.P. Wadsworth,Edinburgh LCF: A Mechanised Logic of Computation. Berlin: SpringerVerlag, 1979.
[15] J. V. Guttag and J. J. Horning, "Formal specification as a design tool," inProc. 7th ACM Symp. Principles of Programming Languages, 1980, pp. 251261.
[16] P. Harrison and H. Khoshnevisan, "Efficient compilation of linear recursive functions into objectlevel loops," inProc. SIGPLAN '86 Sym. on Compiler Constructions, 1986, pp. 207218.
[17] S. Hayashi and H. Nakano,PX: A Computational Logic. Cambridge, MA: MIT Press, 1988.
[18] L. Hines, "Str+ve ??: the Str+ve based subset prover," inProc. 10th Int. Conf. on Auto. Deduction, 1990, pp. 193206.
[19] D. Kapur and P. Narendran, "An equational approach to theorem proving in the firstorder predicate calculus,"Proc. 9th Int. Joint Conf. on Art. Intell., 1985, pp. 11461153.
[20] R. Kowalski, "Predicate logic as a programming language," inProc. IFIP Congress '74, pp. 569544.
[21] W. W. McCune, "OTTER 2.0 users' guide," Math. and Comput. Sci. Div., Argonne Natl. Lab., 1990.
[22] Z. Manna, M. Stickel, and R. Waldinger, "Monotonicity properties in automated deduction," inArtificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, V. Lifschitz, Ed. New York: Academic, 1991, pp. 261280.
[23] Manna, Z., and R. Waldinger, "A Deductive Approach to Program Synthesis,"Trans. Programming Languages and Systems, Vol. 2, No. 1, Jan. 1980, pp. 90121.
[24] Z. Manna and R. Waldinger, "Deductive synthesis of the unification algorithm,"Sci. Comput. Program., vol. 1, pp. 548, 1981.
[25] Z. Manna and R. Waldinger,The Logical Basis for Computer Programming, vol. 1,Deductive Reasoning. Reading, MA: AddisonWesley, 1985.
[26] Z. Manna and R. Waldinger, "Special relations in automated deduction,"J. ACM, vol. 33, no. 1, pp. 159, 1986.
[27] Z. Manna and R. Waldinger, "The origin of a binarysearch paradigm,"Sci. Comput. Program., vol. 9, pp. 3783, 1987.
[28] Z. Manna and R. Waldinger, "The deductive synthesis of imperative LISP programs," inProc 6th AAAI Nat. Conf. on Art. Intell., 1987, pp. 155160.
[29] Z. Manna and R. Waldinger,The Logical Basis for Computer Programming, vol. 2,Deductive Systems. Reading, MA: AddisonWesley, 1990.
[30] P. MartinLöf, "Constructive mathematics and computer programming," inProc. 6th Int. Cong. for Logic, Method., and Phil. of Sci., 1982, pp. 153175.
[31] N. Murray, "Completely nonclausal theorem proving,"Art. Intell., vol. 18, no. 1, pp. 6785, 1982.
[32] D. Nardi, "Formal synthesis of a unification algorithm by the deductivetableau method,"J. Logic Program., vol. 7, pp. 143, 1989.
[33] B. Nordström, K. Petersson, and J. M. Smith,Programming in MartinLöf's Type Theory: An Introduction. New York: Oxford Univ. Press, 1990.
[34] L. C. Paulson, "The foundations of a generic theorem prover,"J. Auto. Reasoning, vol. 5, pp. 363397, 1989.
[35] A. Pnueli and R. Rosner, "A framework for the synthesis of reactive modules," inProc. Concurency '88, 1988, pp. 417.
[36] J. A. Robinson, "A machinedoriented logic based on the resolution principle,"J. Assoc. Comput. Mach., vol. 12, no. 1, pp. 2341, Jan. 1965.
[37] M. Sato, "Towards a mathematical theory of program synthesis," inProc. 6th Int. Joint Conf. on Art. Intell., 1979, pp. 757762.
[38] M. SchmidtSchauss, "Computational aspects of an order sorted logic with term declarations," Universität Kaiserslautern, SEKI Rep. SR 8810, 1988.
[39] J. Siekmann, "Unification theory,"J. Symbolic Comput., vol. 7, nos. 3/4, pp. 207274, 1989.
[40] D. R. Smith, "Topdown synthesis of divideandconquer algorithms,"Artificial Intell., vol. 27, no. 1, pp. 4396, Sept. 1985; reprinted inReadings in Artificial Intelligence and Software Engineering, C. Rich and R. Waters, Eds. Los Altos, CA: Morgan Kaufmann, 1986.
[41] N. Shankar, "Checking the proof of Gödel's incompleteness theorem," Instit. Comput. Sci., Univ. Texas at Austin, 1985.
[42] E. Shapiro,Algorithmic Program Debugging. Cambridge, MA: MIT Press, 1983.
[43] M. E. Stickel, "A unification algorithm for associativecommutative functions,"J. ACM, vol. 28, no. 3, pp. 423434, 1981.
[44] M.E. Stickel, "Automated deduction by theory resolution,"J. Auto. Reason., vol. 1, no. 4, pp. 333355, 1985.
[45] J. Traugott, "Deductive synthesis of sorting programs,"J. Symbolic Comput., vol. 7, pp. 533572, 1989.
[46] L. Wos and G. Robinson, "Paramodulation and theorem proving in firstorder theories with equality," inMachine Intelligence 4, B. Meltzer and D. Michie, Eds. New York: Elsevier, 1969, pp. 135150.
[47] L. Wos and S. Winkler, "Open questions solved with the assistance of AURA," inAutomated Theorem Proving: After 25 Years, W. W. Bledsoe and D. W. Loveland, Eds. Providence, RI: Ameri. Math. Soc., 1983, pp. 7388.