iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/BF00244461
Middle-out reasoning for synthesis and induction | Journal of Automated Reasoning Skip to main content
Springer Nature Link
Log in

Middle-out reasoning for synthesis and induction

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

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 variaety of programs fully automatically.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

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

  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 für Informatik Report MPI-I-93-231 and Edinburgh DAI Research Report 654.

  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 Hörnig, 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.

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

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

  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.

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

  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.

  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.

  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.

  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.

  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.

  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.

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

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

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

  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.

  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.

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

  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.

  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.

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

    Article  MATH  MathSciNet  Google Scholar 

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

  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.

  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.

  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.

  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.

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

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

  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 153–175.

    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.

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

  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.

  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.

  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.

  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, U.K.

    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

Additional information

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 EC-US 019-76094, and ARC Project BC/DAAD Grant 438.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Kraan, I., Basin, D. & Bundy, A. Middle-out reasoning for synthesis and induction. J Autom Reasoning 16, 113–145 (1996). https://doi.org/10.1007/BF00244461

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00244461

Key words

Search

Navigation