Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Deductive Synthesis of Recursive Plans in Linear Logic

  • Conference paper
Recent Advances in AI Planning (ECP 1999)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1809))

Included in the following conference series:

Abstract

Linear logic has previously been shown to be suitable for describing and deductively solving planning problems involving conjunction and disjunction. We introduce a recursively defined datatype and a corresponding induction rule, thereby allowing recursive plans to be synthesised. In order to make explicit the relationship between proofs and plans, we enhance the linear logic deduction rules to handle plans as a form of proof term.

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

Access this chapter

Log in via an institution
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.

References

  1. Abramsky, S.: Computational interpretations of linear logic. Theoretical Computer Science 111, 3–57 (1993) (Revised version of Imperial College Technical Report DoC 90/20)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bibel, W.: A deductive solution for plan generation. New Generation Computing 4, 115–132 (1986)

    Article  MATH  Google Scholar 

  3. Brüning, S., Hölldobler, S., Schneeberger, J., Sigmund, U., Thielscher, M.: Disjunction in resource-oriented deductive planning. In: Proceedings of the International Symposium on Logic Programming, p. 670 (1993)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  5. Fikes, R.E., Nilsson, N.J.: STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence 2, 189–208 (1971)

    Article  MATH  Google Scholar 

  6. Ghassem-Sani, G.R., Steel, S.W.D.: Recursive plans. In: Hertzberg, J. (ed.) EWSP 1991. LNCS, vol. 522, pp. 53–63. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  7. Girard, J.-Y.: Linear logic: its syntax and semantics. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic. London Mathematical Society Lecture Notes Series, vol. 222, Cambridge University Press, Cambridge (1995)

    Chapter  Google Scholar 

  8. Große, G., Hölldobler, S., Schneeberger, J.: Linear deductive planning. Journal of Logic and Computation 6(2), 233–262 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  9. Hesketh, J., Bundy, A., Smaill, A.: Using middle-out reasoning to control the synthesis of tail-recursive programs. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 310–324. Springer, Heidelberg (1992)

    Google Scholar 

  10. Hodas, J.S., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation 110(2), 327–365 (1994); Extended abstract in the Proceedings of the Sixth Annual Symposium on Logic in Computer Science, Amsterdam, July 15-18 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  11. Ireland, A., Bundy, A.: Extensions to a Generalization Critic for Inductive Proof. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 47–61. Springer, Heidelberg (1996)

    Google Scholar 

  12. Jacopin, E.: Classical AI planning as theorem proving: The case of a fragment of linear logic. In: AAAI Fall Symposium on Automated Deduction in Nonstandard Logics, Technical Report FS-93-01, pp. 62-66. AAAI Press Publications, Palo Alto (1993)

    Google Scholar 

  13. Manna, Z., Waldinger, R.: How to clear a block: a theory of plans. Journal of Automated Reasoning 3(4), 343–377 (1986)

    MathSciNet  Google Scholar 

  14. Masseron, M.: Generating plans in linear logic II: A geometry of conjunctive actions. Theoretical Computer Science 113, 371–375 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  15. Masseron, M., Tollu, C., Vauzeilles, J.: Generating plans in linear logic I: Actions and proofs. Theoretical Computer Science 113(2), 349–371 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  16. Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf Type Theory. Oxford University Press, Oxford (1990)

    MATH  Google Scholar 

  17. Stephan, W., Biundo, S.: Deduction based refinement planning. In: Drabble, B. (ed.) Proceedings of the 3rd International Conference on Artificial Intelligence Planning Systems (AIPS 1996), pp. 213–220. AAAI Press, Menlo Park (1996)

    Google Scholar 

  18. Sterling, L., Shapiro, E.: The Art of Prolog, 2nd edn. MIT Press, Cambridge (1994)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Division of Informatics, University of Edinburgh, 80 South Bridge, Edinburgh, EH1 1HN, U.K.

    Stephen Cresswell, Alan Smaill & Julian Richardson

Authors
  1. Stephen Cresswell
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alan Smaill
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Julian Richardson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Artificial Intelligence, Ulm University, Germany

    Susanne Biundo

  2.  ,  

    Maria Fox

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cresswell, S., Smaill, A., Richardson, J. (2000). Deductive Synthesis of Recursive Plans in Linear Logic. In: Biundo, S., Fox, M. (eds) Recent Advances in AI Planning. ECP 1999. Lecture Notes in Computer Science(), vol 1809. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720246_20

Download citation

  • DOI: https://doi.org/10.1007/10720246_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67866-3

  • Online ISBN: 978-3-540-44657-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation