Skip to main content
SpringerLink
Log in

Middle-Out Reasoning for Synthesis and Induction

  • Chapter
Automated Mathematical Induction

  • 71 Accesses

Abstract

We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control.

Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete.

Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program.

We have implemented these techniques as an extension of the proof planning system CL A M, called Periwinkle, and synthesized a variety of programs fully automatically.

Supported by the Swiss National Science Foundation and ARC Project BC/DAAD Grant 438. The work described in this paper was carried out while the first author was at the Department of Artificial Intelligence of the University of Edinburgh.

Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9102 and ARC Project BC/DAAD Grant 438. Responsibility for the contents of this publication lies with the authors.

Supported by SERC grant GR/J/80702, ESPRIT BRP grant 6810, ESPRIT BRP grant ECUS 019-76094, and ARC Project BC/DAAD Grant 438.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aubin, R.: Mechanizing structural induction, Ph.D. thesis, University of Edinburgh, 1976.

    Google Scholar 

  2. Basin, D., Bundy, A., Kraan, I., and Matthews, S.: A framework for program development based on schematic proof, in Proc. 7th Int. Workshop on Software Specification and Design (IWSSD-93),1993. Also available as Max-Planck-Institut fur Informatik Report MPI-I-93–231 and Edinburgh DAI Research Report 654.

    Google Scholar 

  3. Basin, D. and Walsh, T.: A calculus for and termination of rippling, J. Automated Reasoning 16 (1–2) (1996), 145–178.

    MathSciNet  Google Scholar 

  4. Bibel, W.: Syntax-directed, semantics-supported program synthesis, Artificial Intelligence 14 (1980), 243–261.

    Article  Google Scholar 

  5. Bibel, W. and Hornig, K. M.: LOPS–a system based on a strategical approach to program synthesis, in A. Biermann, G. Guiho, and Y. Kodratoff (eds), Automatic Program Construction Techniques, Macmillan, 1984, pp. 69–90.

    Google Scholar 

  6. Biundo, S.: Automated synthesis of recursive algorithms as a theorem proving tool, in Y. Kodratoff (ed.), 8th Eue Conf. Artificial Intelligence, Pitman, 1988, pp. 553–558.

    Google Scholar 

  7. Biundo, S.: Automatische Synthese rekursiver Programme als Beweisverfahren, Ph.D. thesis, Universität Karlsruhe, 1989.

    Google Scholar 

  8. Biundo, S., Hummel, B., Hutter, D., and Walther, C.: The Karlsruhe induction theorem proving system, in J. Siekmann (ed.), 8th Conf. Automated Deduction, Lecture Notes in Computer Science 230, Springer-Verlag, 1986, pp. 672–674.

    Google Scholar 

  9. Boyer, R. S. and Moore, J S.: A Computational Logic Handbook,Academic Press, 1988. Perspectives in Computing, Vol. 23.

    Google Scholar 

  10. Bundy, A.: The use of explicit plans to guide inductive proofs, in R. Lusk and R. Overbeek (eds), 9th Conf. Automated Deduction,Springer-Verlag, 1988, pp. 111–120. Longer version available from Edinburgh as DAI Research Paper 349.

    Google Scholar 

  11. Bundy, A. and Lombart, V.: Relational rippling: A general approach, in C. Mellish (ed.), Proc. 14th Int. Joint Conf. Artificial Intelligence, Morgan Kaufmann, 1995, pp. 175–181.

    Google Scholar 

  12. Bundy, A., Smaill, A., and Hesketh, J.: Turning eureka steps into calculations in automatic program synthesis, in S. L. H. Clarke (ed.), Proc. UK IT 90, 1990, pp. 221–226.

    Google Scholar 

  13. Bundy, A., Smaill, A., and Wiggins, G. A.: The synthesis of logic programs from inductive proofs, in J. Lloyd (ed.), Computational Logic, Springer-Verlag, 1990, pp. 135–149. Esprit Basic Research Series. Also available from Edinburgh as DAI Research Paper 501.

    Google Scholar 

  14. Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., and Smaill, A.: Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence 62(1993), 185–253. Also available from Edinburgh as DAI Research Paper 567.

    Google Scholar 

  15. Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A., and Stevens, A.: A rational reconstruction and extension of recursion analysis, in N. S. Sridharan (ed.), Proc. 11th Int. Joint Conf. Artificial Intelligence,Morgan Kaufmann, 1989, pp. 359–365. Also available from Edinburgh as DAI Research Paper 419.

    Google Scholar 

  16. Bundy, A., van Harmelen, F., Horn, C., and Smaill, A.: The Oyster-Clam system, in M. E. Stickel (ed.), 10th Int. Conf. Automated Deduction,Lecture Notes in Artificial Intelligence 449, Springer-Verlag, 1990, pp. 647–648. Also available from Edinburgh as DAI Research Paper 506.

    Google Scholar 

  17. Clark, K. L.: Predicate Logic as a Computational Mechanism, Technical Report 79–59, Dept. of Computing, Imperial College, 1979.

    Google Scholar 

  18. Clark, K. L. and Tärnlund, S.-A.: A first order theory of data and programs, in B. Gilchrist (ed.), Information Processing IFIP, 1977, pp. 939–944.

    Google Scholar 

  19. Deville, Y.: Logic Programming. Systematic Program Development, Int. Series in Logic Programming, Addison-Wesley, 1990.

    Google Scholar 

  20. Deville, Y. and Lau, K. K.: Logic program synthesis, J. Logic Programming 19/20 (May/July 1994 ), 321–350.

    Article  MathSciNet  Google Scholar 

  21. Fribourg, L.: Extracting logic programs from proofs that use extended Prolog execution and induction, in Proc. 8th Int. Conf. Logic Programming, MIT Press, June 1990, pp. 685–699.

    Google Scholar 

  22. Gallier, J.: Logic for Computer Science, Harper & Row, New York, 1986.

    MATH  Google Scholar 

  23. Gordon, M. J., Milner, A. J., and Wadsworth, C. P.: Edinburgh LCF - A Mechanised Logic of Computation, Lecture Notes in Computer Science 78, Springer-Verlag, 1979.

    Google Scholar 

  24. Hesketh, J. T.: Using middle-out reasoning to guide inductive theorem proving, Ph.D. thesis, University of Edinburgh, 1991.

    Google Scholar 

  25. Huet, G.: A unification algorithm for lambda calculus, Theoretical Computer Science 1 (1975), 27–57.

    Article  MathSciNet  Google Scholar 

  26. Hutter, D.: Synthesis of induction ordering for existence proofs, in Proc. 12th Conf. Automated Deduction, 1994.

    Google Scholar 

  27. Ireland, A.: The use of planning critics in mechanizing inductive proofs, in A. Voronkov (ed.), Int. Conf. Logic Programming and Automated Reasoning (LPAR 92), St. Petersburg,Lecture Notes in Artificial Intelligence 624, Springer-Verlag, 1992, pp. 178–189. Also available from Edinburgh as DAI Research Paper 592.

    Google Scholar 

  28. Ireland, A. and Bundy, A.: Productive use of failure in inductive proof, J. Automated Reasoning 16 (1–2) (1996), 79–111.

    Article  MathSciNet  MATH  Google Scholar 

  29. Kraan, I.: Proof planning for logic program synthesis, Ph.D. thesis, University of Edinburgh, 1994.

    Google Scholar 

  30. Kraan, I., Basin, D., and Bundy, A.: Logic program synthesis via proof planning, in K. K. Lau and T. Clement (eds), Logic Program Synthesis and Transformation,Springer-Verlag, 1993, pp. 1–14. Also available as Max-Planck-Institut für Informatik Report MPI-I-92–244 and Edinburgh DAI Research Report 603.

    Google Scholar 

  31. Kraan, I., Basin, D., and Bundy, A.: Middle-out reasoning for logic program synthesis, in D. S. Warren (ed.), Proc. 10th Int. Conf. Logic Programming,MIT Press, 1993. Also available as Max-Planck-Institut für Informatik Report MPI-I-93–214 and Edinburgh DAI Research Report 638.

    Google Scholar 

  32. Lau, K. K. and Prestwich, S. D.: Synthesis of Recursive Logic Procedures by Top–Down Folding, Technical Report UMCS–88–2–1, Dept. of Computer Science, University of Manchester, February 1988.

    Google Scholar 

  33. Lau, K. K. and Prestwich, S. D.: Top-down synthesis of recursive logic procedures from first-order logic specifications, in D. H. D. Warren and P. Szeredi (eds), Proc. 7th Int. Conf. Logic Programming, MIT Press, 1990, pp. 667–684.

    Google Scholar 

  34. Lloyd, J. W.: Foundations of Logic Programming , Symbolic Computation,Springer-Verlag, 1987, second, extended edition.

    Google Scholar 

  35. Manning, A.: Representing preference in proof plans, Master’s thesis, Edinburgh, 1992.

    Google Scholar 

  36. Martin-Löf, P.: Constructive mathematics and computer programming, in 6th Int. Congr. for Logic , Methodology and Philosophy of Science,North Holland, Amsterdam, 1982, pp. 153175.

    Google Scholar 

  37. Miller, D.: A logic programming language with lambda abstraction, function variables and simple unification, in Extensions of Logic Programming, Lecture Notes in Artificial Intelligence 475, Springer-Verlag, 1991.

    Google Scholar 

  38. Nipkow, T.: Higher-order critical pairs, in Proc. 6th IEEE Symp. Logic in Computer Science, 1991, pp. 342–349.

    Chapter  Google Scholar 

  39. Protzen, M.: Lazy generation of induction hypotheses, in A. Bundy (ed.), Proc. 12th Conf on Automated Deduction, Lecture Notes in Artificial Intelligence 814, Springer-Verlag, 1994.

    Google Scholar 

  40. Richards, B. L., Kraan, I., Smaill, A., and Wiggins, G. A.: Mollusc: A general proof development shell for sequent-based logics, in A. Bundy (ed.), Proc. 12th Conf Automated Deduction,Lecture Notes in Artificial Intelligence 814, Springer-Verlag, 1994, pp. 826–830. Also available from Edinburgh as DAI Research Paper 723.

    Google Scholar 

  41. Stevens, A.: A rational reconstruction of Boyer and Moore’s technique for constructing induction formulas, in Y. Kodratoff (ed.), Proc. European Conference on Artificial Intelligence (ECAI-88),1988, pp. 565–570. Also available from Edinburgh as DAI Research Paper 360.

    Google Scholar 

  42. Wiggins, G. A.: Synthesis and transformation of logic programs in the Whelk proof development system, in K. R. Apt (ed.), Proc. Joint Int. Conf. Symp. Logic Programming (JICSLP-92), MIT Press, Cambridge, MA, 1992, pp. 351–368.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Zürich, CH-8057, Zürich, Switzerland

    Ina Kraan

  2. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    David Basin

  3. Department of Artificial Intelligence, University of Edinburgh, Scotland, UK

    Alan Bundy

Authors
  1. Ina Kraan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alan Bundy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Iowa, Iowa City, IA, 52242, USA

    Hantao Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Kluwer Academic Publishers

About this chapter

Cite this chapter

Kraan, I., Basin, D., Bundy, A. (1996). Middle-Out Reasoning for Synthesis and Induction. In: Zhang, H. (eds) Automated Mathematical Induction. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-1675-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-94-009-1675-3_4

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-94-010-7250-2

  • Online ISBN: 978-94-009-1675-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation