Automatic program generation using sequent calculus

ABSTRACT

Program development can be made amenable to formal methods by using a logical framework. A logic specification, whose operational semantics is based on proof theory, provides an abstract and “implementation independent” definition of the problem, the data domains and the associated operators. Unlike many of the current efforts in this area that use resolution, our approach is based on natural deduction, more specifically, sequent calculus. Following the methodology proposed by Manna and Waldinger, we propose the synthesis tableau technique by which we construct a proof for the well formed formula representing the specification. The desired program is obtained as a side effect of the proof process.

REFERENCES

• Barr82: A. Barr and E. Feigenbaun (Eds), The Handbook of Artificial Intelligence, Vol. 2, Chapter X, William Kaufmann Inc., pp. 297-325, 1982.
• Bier76: A. Biermann, "Approaches to Automatic Programming," in Advances in Computers, Vol. 15, pp. 1-63, Academic Press, 1976.
• Bled83: W. Bledsoe, "The LIT Prover," Math Department Memo ATP-17B, University of Texas At Austin, April 1983.
• Cohn90: Edward Cohen, Programming in the 1990s: an introduction to the calculation of programs, Springer-Verlag New York, Inc., New York, NY, 1990
• Cons78: R. Constable and M. O'Donnell, A Programming Logic with An Introduction to The PLICV VerOqer, Winthrop Publisher, Inc., 1978.
• Dijk76: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• Drom89: Geoff Dromey, Program derivation: the development of programs from specifications, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• Gold82: Robert Goldblatt, Axiomatising the Logic of Computer Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• Gols88: F. Golshani, W. Scott and P. White, "Languages for Intelligent Specifw.ation Systems," Proc. of IEEE International Conference on Computer Languages, Miami Beach, FL, pp 304-311, 1988.
• Goto78: Shigeki Goto, Program synthesis through Gödel's interpretation, Proceedings of the International Conference on Mathematical Studies of Information Processing, p.302-325, August 23-26, 1978
• Goto79: S. Goto, "Program Synthesis from Natural Deduction Proofs," proc. of Int.Joint Conference on Artificial Intelligence, pp. 339-341, 1979.
• Gren69: C. Green, "Application of Theorem Proving to Problem Solving," proc. oflJCAl, pp. 219-239, 1969.
• Magh91: T. Maghrabi, "Generating Programs from Natural Deduction Proofs," Proc. of The First Golden West Conference on Intelligence Systems, Reno, Nevada, pp. 150-156, June 1991.
• Magh92: T. Maghrabi, "The Synthesis Tableau: An Automatic Programming Approach Using Sequent Calculus," Ph. D dissertation, Delmrtment of Computer Sc~ and Engineering, Arizona State University, 1992.
• Mann80: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• Mann85: Zohar Manna , Richard Waldinger, The logical basis for computer programming: vol. 2, deductive systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• Paul87: Lawrence C. Paulson, Logic and computation: interactive proof with Cambridge LCF, Cambridge University Press, New York, NY, 1987
• Sato79: M. Sato, "Towards A Mathematical Theory of Program Synthesis," proc. of Int.loint Conference on ArtCicial Intelligence, pp. 757-762, 1979.
• Schu90: G. Gordon Schulmeyer, Zero defect software, McGraw-Hill, Inc., New York, NY, 1990
• Szab69: M. Szabo (Ed.), The Collected Papers of Gerhard Gentzen, North-Holland Publishing Company, pp. 68-128, 1969.
• Wald69: R. Waldinger and R. Lee, "PROW: A Step Toward Automatic Program Writing," proc. of IJCAI, pp. 241-252, 1969.
• Wos84: Larry Wos , Ross Overbeek , Ewing Lusk , Jim Boyle, Automated reasoning (2nd ed.): introduction and applications, McGraw-Hill, Inc., New York, NY, 1992

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program synthesis

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Languages, Theory, Verification