Nothing Special   »   [go: up one dir, main page]

Skip to main content

Generalization and reuse of tactic proofs

  • Conference paper
  • First Online:
Logic Programming and Automated Reasoning (LPAR 1994)

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

Abstract

A tactic proof is a tree-structured sequent proof where steps may be justified by tactic programs. We describe a prototype of a generic interactive theorem-proving system that supports the construction and manipulation of tactic proofs containing metavariables. The emphasis is on proof reuse. Examples of proof reuse are proof by analogy and reconstruction of partial proofs as part of recovering from errors in definitions or in proof strategies. Our reuse operations involve solving higherorder unification problems, and their effectiveness relies on a proof-generalization step that is done after a tactic is applied. The prototype is implemented in λProlog.

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

Access this chapter

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. R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

    Google Scholar 

  2. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The coq proof assistant user's guide. Technical Report 154, INRIA, 1993.

    Google Scholar 

  3. A. Felty. Implementing tactics and tacticals in a higher-order logic programming language, Journal of Automated Reasoning, 11(1):43–81, August 1993.

    Google Scholar 

  4. A. Felty and D. Howe. Tactic theorem proving with refinement-tree proofs and metavariables. In Twelfth International Conference on Automated Deduction. Springer-Verlag Lecture Notes in Computer Science, June 1994.

    Google Scholar 

  5. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, January 1993.

    Google Scholar 

  6. M. Heisel, W. Reif, and W. Stephan. Tactical theorem proving in program verification. In M. Stickel, editor, Tenth Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 117–131. Springer-Verlag, 1990.

    Google Scholar 

  7. C. Horn. The Oyster Proof Development System. University of Edinburgh, 1988.

    Google Scholar 

  8. L. Magnussan. Refinement and local undo in the interactive proof editor ALF. In Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, 1993.

    Google Scholar 

  9. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

    Google Scholar 

  10. L. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Frank Pfenning

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Felty, A., Howe, D. (1994). Generalization and reuse of tactic proofs. In: Pfenning, F. (eds) Logic Programming and Automated Reasoning. LPAR 1994. Lecture Notes in Computer Science, vol 822. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58216-9_25

Download citation

  • DOI: https://doi.org/10.1007/3-540-58216-9_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58216-8

  • Online ISBN: 978-3-540-48573-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics