Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Synthesis of Programs in Computational Logic

  • Chapter
Program Development in Computational Logic

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3049))

Abstract

Since the early days of programming and automated reasoning, researchers have developed methods for systematically constructing programs from their specifications. Especially the last decade has seen a flurry of activities including the advent of specialized conferences, such as LOPSTR, covering the synthesis of programs in computational logic. In this paper we analyze and compare three state-of-the-art methods for synthesizing recursive programs in computational logic. The three approaches are constructive/deductive synthesis, schema-guided synthesis, and inductive synthesis. Our comparison is carried out in a systematic way where, for each approach, we describe the key ideas and synthesize a common running example. In doing so, we explore the synergies between the approaches, which we believe are necessary in order to achieve progress over the next decade in this field.

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

Access this chapter

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

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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.

Similar content being viewed by others

References

  1. Anderson, P., Basin, D.: Program development schemata as derived rules. Journal of Symbolic Computation 30(1), 5–36 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Ayari, A., Basin, D.: Generic system support for deductive program development. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 313–328. Springer, Heidelberg (1996)

    Google Scholar 

  3. Ayari, A., Basin, D.: A higher-order interpretation of deductive tableau. Journal of Symbolic Computation (2002) (to appear)

    Google Scholar 

  4. Balzer, R.: A 15 year perspective on automatic programming. IEEE Transactions. on Software Engineering 11(11), 1257–1268 (1985)

    Article  Google Scholar 

  5. Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics, 2nd revised edn. Studies in Logic, vol. 103. North-Holland, Amsterdam (1984)

    MATH  Google Scholar 

  6. Basin, D.: IsaWhelk: Whelk interpreted in Isabelle. In: Van Hentenryck, P. (ed.) Proc. of ICLP 1994, p. 741. The MIT Press, Cambridge (1994)

    Google Scholar 

  7. Basin, D.: Logic frameworks for logic programs. In: Fribourg, L., Turini, F. (eds.) LOPSTR 1994 and META 1994. LNCS, vol. 883, pp. 1–16. Springer, Heidelberg (1994)

    Google Scholar 

  8. Basin, D.: Logical-framework-based program development. ACM Computing Surveys 30(3es), 1–4 (1998)

    Article  Google Scholar 

  9. Basin, D., Friedrich, S.: Modeling a hardware synthesis methodology in Isabelle. Formal Methods in Systems Design 15(2), 99–122 (1999)

    Article  Google Scholar 

  10. Basin, D., Krieg-Brückner, B.: Formalization of the development process. In: Astesiano, E., Kreowski, H.-J., Krieg-Brückner, B. (eds.) Algebraic Foundations of System Specification, pp. 521–562. Springer, Heidelberg (1998)

    Google Scholar 

  11. Basin, D., Matthews, S.: Adding metatheoretic facilities to first-order theories. Journal of Logic and Computation 6(6), 835–849 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  12. Basin, D., Walsh, T.: Annotated rewriting in inductive theorem proving. Journal of Automated Reasoning 16(1–2), 147–180 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  13. Biermann, A.W.: Automatic programming. In: Shapiro, S.C. (ed.) Encyclopedia of Artificial Intelligence, 2nd extended edn., pp. 59–83. John Wiley, Chichester (1992)

    Google Scholar 

  14. Biermann, A.W., Guiho, G., Kodratoff, Y. (eds.): Automatic Program Construction Techniques. Macmillan, Basingstoke (1984)

    MATH  Google Scholar 

  15. Blaine, L., Gilham, L., Liu, J., Smith, D.R., Westfold, S.: PlanWare: Domainspecific synthesis of high-performance schedulers. In: Proc. of ASE 1998, pp. 270–279. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  16. Bundy, A., Smaill, A., Wiggins, G.A.: The synthesis of logic programs from inductive proofs. In: Lloyd, J.W. (ed.) Computational Logic. Esprit Basic Research Series, pp. 135–149. Springer, Heidelberg (1990)

    Google Scholar 

  17. Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence 62(2), 185–253 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  18. Buntine, W.: Generalized subsumption and its application to induction and redundancy. Artificial Intelligence 36(2), 375–399 (1988)

    Article  MathSciNet  Google Scholar 

  19. Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, London (1973)

    MATH  Google Scholar 

  20. Chasseur, E., Deville, Y.: Logic program schemas, constraints and semiunification. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 69–89. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  21. Christiansen, H.: Implicit program synthesis by a reversible metainterpreter. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 90–110. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  22. Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)

    Article  Google Scholar 

  23. Coen, M.D.: Interactive program derivation. Technical Report 272, Cambridge University Computer Laboratory, UK (1992)

    Google Scholar 

  24. Coquand, T., Huet, G.: The calculus of constructions. In: Information and Computation, pp. 95–120 (1988)

    Google Scholar 

  25. Deville, Y.: Logic Programming: Systematic Program Development. International Series in Logic Programming. Addison-Wesley, Reading (1990)

    Google Scholar 

  26. Deville, Y., Lau, K.-K.: Logic program synthesis. Journal of Logic Programming 19-20, 321–350 (1994)

    Article  MathSciNet  Google Scholar 

  27. Felty, A., Miller, D.: Specifying theorem provers in a higher-order logic programming language. In: Lusk, E.‘., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 61–80. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  28. Flener, P.: Logic Program Synthesis from Incomplete Information. Kluwer Academic Publishers, Dordrecht (1995)

    Google Scholar 

  29. Flener, P.: Achievements and prospects of program synthesis. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2407, pp. 310–346. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Flener, P., Deville, Y.: Logic program synthesis from incomplete specifications. Journal of Symbolic Computation 15(5-6), 775–805 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  31. Flener, P., Lau, K.-K., Ornaghi, M.: Correct-schema-guided synthesis of steadfast programs. In: Proc. of ASE 1997, pp. 153–160. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  32. Flener, P., Lau, K.-K., Ornaghi, M.: On correct program schemas. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 124–143. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  33. Flener, P., Lau, K.-K., Ornaghi, M., Richardson, J.D.C.: An abstract formalisation of correct schemas for program synthesis. Journal of Symbolic Computation 30(1), 93–127 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  34. Flener, P., Partridge, D.: Inductive programming. Automated Software Engineering 8(2), 131–137 (2001)

    Article  Google Scholar 

  35. Flener, P., Richardson, J.D.C.: A unified view of programming schemas and proof methods. In: Bossi, A. (ed.) Proc. of LOPSTR 1999, pp. 75–82. Tech. rept. CS-99-16, Univ. of Venice, Italy (1999); Also see Technical Report 2003-008 at the Department of Information Technology, Uppsala University, Sweden (2003)

    Google Scholar 

  36. Flener, P., Yılmaz, S.: Inductive synthesis of recursive logic programs: Achievements and prospects. Journal of Logic Programming 41(2-3), 141–195 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  37. Flener, P., Zidoum, H., Hnich, B.: Schema-guided synthesis of CLP programs. In: Proc. of ASE 1998, pp. 168–176. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  38. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)

    Google Scholar 

  39. Gegg-Harrison, T.S.: Extensible logic program schemata. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 256–274. Springer, Heidelberg (1997)

    Google Scholar 

  40. Goldberg, A.T.: Knowledge-based programming: A survey of program design and construction techniques. IEEE Transactions on Software Engineering 12(7), 752–768 (1986)

    Google Scholar 

  41. Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanized Logic of Computation. In: Gordon, M., Wadsworth, C.P., Milner, R. (eds.) Edinburgh LCF. LNCS, vol. 78, Springer, Heidelberg (1979)

    Google Scholar 

  42. Green, C.: Application of theorem proving to problem solving. In: Proc. of IJCAI 1969, pp. 219–239. Morgan Kaufmann, San Francisco (1969)

    Google Scholar 

  43. Hamfelt, A., Fischer Nilsson, J.: Inductive metalogic programming. In: Jelitsch, R., Lange, O., Haupt, D., Juling, W., Händler, W. (eds.) CONPAR 1986. LNCS, vol. 237, pp. 85–96. Springer, Heidelberg (1986)

    Google Scholar 

  44. Hamfelt, A., Fischer Nilsson, J.: Declarative logic programming with primitive recursive relations on lists. In: Maher, M.J. (ed.) Proc. of JICSLP 1996, pp. 230–243. The MIT Press, Cambridge (1996)

    Google Scholar 

  45. Hamfelt, A., Fischer Nilsson, J.: Towards a logic programming methodology based on higher-order predicates. New Generation Computing 15(4), 421–448 (1997)

    Article  Google Scholar 

  46. Hamfelt, A., Fischer Nilsson, J., Oldager, N.: Logic program synthesis as problem reduction using combining forms. Automated Software Engineering 8(2), 167–193 (2001)

    Article  MATH  Google Scholar 

  47. Hill, P., Lloyd, J.W.: The Gödel Programming Language. MIT Press, Cambridge (1994)

    MATH  Google Scholar 

  48. Hindley, J.R., Seldin, J.P.: Introduction to Combinators and the λ-Calculus. Cambridge University Press, Cambridge (1986)

    Google Scholar 

  49. Howe, D.J.: On computational open-endedness in Martin-Löf’s type theory. In: Proc. of LICS 1991, pp. 162–172. IEEE Computer Society Press, Los Alamitos (1991)

    Google Scholar 

  50. Kraan, I., Basin, D., Bundy, A.: Logic program synthesis via proof planning. In: Lau, K.-K., Clement, T. (eds.) Proc. of LOPSTR 1992, Workshops in Computing Series, pp. 1–14. Springer, Heidelberg (1993)

    Google Scholar 

  51. Kraan, I., Basin, D., Bundy, A.: Middle-out reasoning for synthesis and induction. Journal of Automated Reasoning 16(1-2), 113–145 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  52. Lau, K.-K., Ornaghi, M.: On specification frameworks and deductive synthesis of logic programs. In: Fribourg, L., Turini, F. (eds.) LOPSTR 1994 and META 1994. LNCS, vol. 883, pp. 104–121. Springer, Heidelberg (1994)

    Google Scholar 

  53. Lau, K.-K., Ornaghi, M.: S.-˚A. Tärnlund. Steadfast logic programs. Journal of. Logic Programming 38(3), 259–294 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  54. Lisett, C.L., Rumelhart, D.E.: Facial recognition using a neural network. In: Proc. of the 11th International Florida AI Research Symposium FLAIRS 1998, pp. 328–332 (1998)

    Google Scholar 

  55. Maher, M.J.: Equivalences of logic programs. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, San Francisco (1987)

    Google Scholar 

  56. Martin-Löf, P.: Constructive mathematics and computer programming. In: Proc. of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pp. 153–175. North-Holland, Amsterdam (1982)

    Chapter  Google Scholar 

  57. Minton, S.: Automatically configuring constraint satisfaction programs: A case study. Constraints 1(1-2), 7–43 (1996)

    Article  MathSciNet  Google Scholar 

  58. Muggleton, S.: Inverse entailment and Progol. New Generation Computing 13(3-4), 245–286 (1995)

    Article  Google Scholar 

  59. Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)

    Book  MATH  Google Scholar 

  60. Pettorossi, A., Proietti, M.: Transformation of logic programs. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, Clarendon Press (1998)

    Google Scholar 

  61. Pfenning, F.: Logic programming in the LF logical framework. In: Logical Frameworks, pp. 149–181. Cambridge University Press, Cambridge (1991)

    Chapter  Google Scholar 

  62. Plotkin, G.D.: A note on inductive generalization. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 5, pp. 153–163. Edinburgh University Press (1970)

    Google Scholar 

  63. Reynolds, J.C.: Transformational systems and the algebraic structure of atomic formulas. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 5, pp. 135–151. Edinburgh University Press (1970)

    Google Scholar 

  64. Smith, D.R.: The structure of divide and conquer algorithms. Technical Report 52-83-002, Naval Postgraduate School, Monterey, California, USA (1983)

    Google Scholar 

  65. Smith, D.R.: Top-down synthesis of divide-and-conquer algorithms. Artificial Intelligence 27(1), 43–96 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  66. Smith, D.R.: KIDS: A semiautomatic program development system. IEEE Transactions. on Software Engineering 16(9), 1024–1043 (1990)

    Article  Google Scholar 

  67. Smith, D.R.: Toward a classification approach to design. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 62–84. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  68. Somogyi, Z., Henderson, F., Conway, T.: The execution algorithm of Mercury: An efficient purely declarative logic programming language. Journal of Logic Programming 29(1-3), 17–64 (1996)

    Article  MATH  Google Scholar 

  69. van Lamsweerde, A.: Formal specification: A roadmap. In: Finkelstein, A. (ed.) The Future of Software Engineering, pp. 147–159. ACM Press, New York (2000)

    Google Scholar 

  70. Vasconcelos, W.W., Fuchs, N.E.: An opportunistic approach for logic program analysis and optimisation using enhanced schema-based transformations. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 174–188. Springer, Heidelberg (1996)

    Google Scholar 

  71. Wiggins, G.A.: Synthesis and transformation of logic programs in the Whelk proof development system. In: Apt, K.R. (ed.) Proc. of JICSLP 1992, pp. 351–365. The MIT Press, Cambridge (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, ETH Zurich, Zürich, Switzerland

    David Basin

  2. Department of Computing Science and Engineering, Université catholique de Louvain, Pl. Ste Barbe 2, B-1348, Louvain-la-Neuve, Belgium

    Yves Deville

  3. Computing Science Division, Department of Information Technology, Uppsala University, Box 337, S-751 05, Uppsala, Sweden

    Pierre Flener

  4. Computer Science Division, Department of Information Science, Uppsala University, Box 513, S-751 20, Uppsala, Sweden

    Andreas Hamfelt

  5. Informatics and Mathematical Modelling, Technical University of Denmark, DK-2800, Lyngby, Denmark

    Jørgen Fischer Nilsson

Authors
  1. David Basin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yves Deville
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pierre Flener
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andreas Hamfelt
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Jørgen Fischer Nilsson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Katholieke Universiteit Leuven, Belgium

    Maurice Bruynooghe

  2. School of Computer Science, The University of Manchester, M13 9PL, Manchester, United Kingdom

    Kung-Kiu Lau

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Basin, D., Deville, Y., Flener, P., Hamfelt, A., Fischer Nilsson, J. (2004). Synthesis of Programs in Computational Logic. In: Bruynooghe, M., Lau, KK. (eds) Program Development in Computational Logic. Lecture Notes in Computer Science, vol 3049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25951-0_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-25951-0_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22152-4

  • Online ISBN: 978-3-540-25951-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation