Skip to main content
SpringerLink
Log in

Proof by pointing

  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 1994)

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

Included in the following conference series:

Abstract

This paper presents a principle for using locations in logical expressions to guide the process of building proofs. Using a sequent-style presentation of theorem provers, we annotate the inference rules to specify an algorithm that associates the construction of a proof tree to a location within a goal sequent. This principle provides a natural and effective use of the mouse in the user-interface of computer proof assistants. The implementation of the algorithm in a variety of theorem provers is discussed.

This work was supported in part by the “Types for Proofs and Programs” Esprit Basic Research Action, by SERC grant GR/G 33837 and a grant from DSTO Australia.

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

Access this chapter

Log in via an institution

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. A. Bonadio, E. Warren. Theorist Reference Manual, Prescience Corp. 814 Castro St. San Francisco, 1989

    Google Scholar 

  2. G. Boudol “Computational semantics of term rewriting systems”, in Algebraic Methods in Semantics, M. Nivat, J. C. Reynolds eds., Cambridge University Press, 1985.

    Google Scholar 

  3. “The Centaur 1.3 Manual”, I. Jacobs, ed., available from INRIA-Sophia-Antipolis, January 1993.

    Google Scholar 

  4. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin-Mohring, B. Werner, The Coq Proof Assistant User's Guide, INRIA Technical Report no. 134, December 1991.

    Google Scholar 

  5. A. Felty, Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language, PhD Thesis, University of Pennsylvania, August 1989.

    Google Scholar 

  6. J. Grundy, “Window Inference in the HOL System”, in Proceeding of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, M. Archer, J. J. Joyce, K. N. Levitt, P. J. Windley, eds., IEEE Computer Society Press, 1991.

    Google Scholar 

  7. M.J.C. Gordon, “HOL: A Proof Generating System for Higher-Order Logic”, in VLSI Specification, Verification and Synthesis, G. Birtwistle, P. A. Subrahmanyam, eds., Kluwer Academic Publishers, 1988.

    Google Scholar 

  8. L.C. Paulson, “Isabelle: The next 700 theorem provers”, in Logic and Computer Science, P. Odifreddi, ed., pp. 361–386, Academic Press, 1990.

    Google Scholar 

  9. B. W. Char et al., MAPLE: reference manual: 5th edition, Springer-Verlag, 1992.

    Google Scholar 

  10. R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, J.T.Smith, Implementing Mathematics with the Nuprl Proof Development System Prentice-Hall, 1986.

    Google Scholar 

  11. Paracomp Inc. Milo User's Guide, 123 Townsend St., Suite 310, San Francisco, 1988.

    Google Scholar 

  12. L. Paulson, Logic and computation: interactive proof with Cambridge LCF, Cambridge University Press, 1987.

    Google Scholar 

  13. G. Sundholm, “Systems of Deduction”, in Handbook of Philosophical Logic, Vol. I, D. Gabbay and F. Guenthner, eds., pp. 133–188, D. Reidel Publishing Company, 1983

    Google Scholar 

  14. B. Ritchie, The design and implementation of an interactive proof editor, PhD Thesis, University of Edinburgh, Nov. 1988. G. Sundholm, “Systems of Deduction”, in Handbook of Philosophical Logic,Vol. I, D. Gabbay, F. Guenthner, eds., D. Reidel Publishing Company, 1983.

    Google Scholar 

  15. M.E. Szabo, G. Gentzen, The Collected papers of Gerhard Gentzen, North-Holland, 1969.

    Google Scholar 

  16. L. Théry, Y. Bertot, G. Kahn, “Real Theorem Provers Deserve Real User-Interfaces”, in Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments, Tyson's Corner, Va, USA, Software Engineering Notes, Vol. 17, no. 5, ACM Press, 1992.

    Google Scholar 

  17. S. Wolfram, Mathematica: a system for doing mathematics by computer, Addison-Wesley, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia-Antipolis, B.P. 93, F-06902, Sophia Antipolis Cedex, France

    Yves Bertot & Gilles Kahn

  2. Computer Laboratory, University of Cambridge, New Museums Site, Pembroke Street, CB2 3QG, Cambridge, England

    Laurent Théry

Authors
  1. Yves Bertot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gilles Kahn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Masami Hagiya John C. Mitchell

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bertot, Y., Kahn, G., Théry, L. (1994). Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_94

Download citation

  • DOI: https://doi.org/10.1007/3-540-57887-0_94

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57887-1

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation