Skip to main content
SpringerLink
Log in

A Semantics for Proof Plans with Applications to Interactive Proof Planning

  • Conference paper
  • First Online:
Book cover Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002)

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

Abstract

Proof planning is an automated theorem proving technique which encodes meaningful blocks of proof as planning operators called methods. Methods often encode complex control strategies, and a language of methodicals, similar to tacticals, has been developed to allow methods to be expressed in a modular way.

Previous work has demonstrated that proof planning can be effective for interactive theorem proving, but it has not been clear how to reconcile the complex control encoded by methodicals with the needs of interactive theorem proving.

In this paper we develop an operational semantics for methodicals which allows reasoning about proof plans in the abstract, without generating object-level proofs, and facilitates interactive planning. The semantics is defined by a handful of deterministic transition rules, represents disjunction and backtracking in the planning process explicitly, and handles the cut methodical correctly.

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. Serge Autexier Axel Schairer and Dieter Hutter. A pragmatic approach to reuse in tactical theorem proving. In Maria Paola Bonacina and Bernhard Gramlich, editors, Electronic Notes in Theoretical Computer Science, volume 58. Elsevier Science Publishers, 2001.

    Google Scholar 

  2. C. Benzmüller, L. Cheikhrouhou, D Fehrer, A. Fiedler, X. Huang, M. Kerber, K. Kohlhase, A Meirer, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge. Ωmega: Towards a mathematical assistant. In W. McCune, editor, 14 th International Conference on Automated Deduction, pages 252–255. Springer-Verlag, 1997.

    Google Scholar 

  3. A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303–324, 1991. Earlier version available from Edinburgh as DAI Research Paper No 413.

    Article  MATH  MathSciNet  Google Scholar 

  4. Arie de Bruin and Erik P. de Vink. Continuation semantics for PROLOG with cut. In TAPSOFT, Vol.1, pages 178–192, 1989.

    Google Scholar 

  5. M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF-A mechanised logic of computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

    Google Scholar 

  6. A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1-2):79–111, 1996. Also available from Edinburgh as DAI Research Paper No 716.

    Article  MATH  MathSciNet  Google Scholar 

  7. M. Jamnik, M. Kerber, and M. Pollet. Automatic learning in proof planning. In F. van Harmelen, editor, Proceedings of 15th ECAI. European Conference on Artificial Intelligence. Springer Verlag, Forthcoming.

    Google Scholar 

  8. Richard B. Kieburtz. A logic for rewriting strategies. In Maria Paola Bonacina and Bernhard Gramlich, editors, Electronic Notes in Theoretical Computer Science, volume 58. Elsevier Science Publishers, 2001.

    Google Scholar 

  9. D. Lacey, J. D. C. Richardson, and A. Smaill. Logic program synthesis in a higher order setting. In Proceedings of the First International Conference on Computational Logic (CL2000), volume 1861 of Lecture Notes in AI, pages 912–925. Springer-Verlag, 2000.

    Google Scholar 

  10. H. Lowe and D. Duncan. XBarnacle: Making theorem provers more accessible. In William McCune, editor, 14th International Conference on Automated Deduction, pages 404–408. Springer-Verlag, 1997.

    Google Scholar 

  11. E. Melis and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 1999.

    Google Scholar 

  12. J. D. C. Richardson and A. Smaill. Continuations of proof strategies. In International Joint Conference on Automated Reasoning, IJCAR-2001-Short Papers, June 2001. Technical Report DII 11/01, Dipartimento di Ingegneria dell’Informazione, Università di Siena, Italy.

    Google Scholar 

  13. J. D. C Richardson, A. Smaill, and I. M. Green. System description: proof planning in higher-order logic with IClam. In Claude Kirchner and Hélène Kirchner, editors, 15th International Conference on Automated Deduction, volume 1421 of Lecture Notes in Artificial Intelligence, Lindau, Germany, July 1998.

    Google Scholar 

  14. J. Siekmann, S. Hess, C. Benzmueller, L. Cheikhrouhou, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, and V. Sorge. Loui: Lovely Omegauser interface. Formal Aspects of Computing, 3:1–18, 1999.

    Google Scholar 

  15. Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. Lecture Notes in Computer Science volume 2051, 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Mathematical and Computer Sciences, Heriot-Watt University, Riccarton, Edinburgh

    Julian Richardson

Authors
  1. Julian Richardson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria

    Matthias Baaz

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, M13, 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Richardson, J. (2002). A Semantics for Proof Plans with Applications to Interactive Proof Planning. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_23

Download citation

  • DOI: https://doi.org/10.1007/3-540-36078-6_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00010-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation