Skip to main content
SpringerLink
Log in

The Theorema Environment for Interactive Proof Development

  • Conference paper
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005)

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

Abstract

We describe an environment that allows the users of the Theorema system to flexibly control aspects of computer-supported proof development. The environment supports the display and manipulation of proof trees and proof situations, logs the user activities (commands communicated with the system during the proving session), and presents (also unfinished) proofs in a human-oriented style. In particular, the user can navigate through the proof object, expand/remove proof branches, provide witness terms, develop several proofs concurrently, proceed step by step or automatically and so on. The environment enhances the effectiveness and flexibility of the reasoners of the Theorema system.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. Aitken, J.S., Gray, P.D., Melham, T.F., Thomas, M.: Interactive theorem proving: An empirical study of user activity. J. Symb. Comp. 25(2), 263–284 (1998)

    Article  Google Scholar 

  2. Aspinall, D.: Proof general: A generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 38–42. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. A database of mechanized reasoning systems, http://www-formal.stanford.edu/clt/ARS/systems.html .

  4. Benzmüller, C. (ed.): Mathematics Assistance Systems. Special Issue of J. Applied Logic. Elsevier (2005) (to appear)

    Google Scholar 

  5. Bertot, Y., Castèran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)

    Google Scholar 

  6. Bornat, R., Sufrin, B.: Jape’s quiet interface. In: Proc. Second Workshop on User Interfaces for Theorem Provers (UITP 1996) (1996)

    Google Scholar 

  7. Buchberger, B.: The PCS prover in Theorema. In: Moreno-Díaz Jr., R., Buchberger, B., Freire, J.-L. (eds.) EUROCAST 2001. LNCS, vol. 2178, pp. 469–478. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Buchberger, B., Crǎciun, A., Jebelean, T., Kovács, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. In: J. Applied Logic (2005) To appear in [4]

    Google Scholar 

  9. Buchberger, B., Jebelean, T., Văsaru, D.: Theorema: A system for formal scientific training in natural language presentation. In: Ottmann, T., Tomek, I. (eds.) Proc. ED–MEDIA/ED–TELECOM 1998, pp. 174–179 (1998)

    Google Scholar 

  10. Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  11. Constable, R.: Implementing Mathematics Using the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)

    Google Scholar 

  12. Eastaughffe, K.: Support for interactive theorem proving: Some design principles and their application. In: Proc. 4th Workshop on User Interfaces for Theorem Provers (UITP 1998) (1998)

    Google Scholar 

  13. Goguen, J.A.: Social and semiotic analyses for theorem prover user interface design. Formal Aspects of Computing 11(3), 272–301 (1999)

    Article  Google Scholar 

  14. Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  15. Hales, T.C.: A computer verification of the Kepler conjecture. In: Bai, F., Wegner, B. (eds.) ICM 2002. LNCS, vol. 2730. Springer, Heidelberg (2003)

    Google Scholar 

  16. Kossak, F.: An interface for interactive proving with the mathematical software system Theorema. Technical Report 99–19, RISC, University of Linz (1999)

    Google Scholar 

  17. Kossak, F., Nakagawa, K.: User–System Interaction within Theorema. Technical Report 99-37, RISC, University of Linz (1999)

    Google Scholar 

  18. Moten, R.: Just the facts, Jack: Truths and myths of automated theorem provers. Contemporary Mathematics 252, 31–48 (1999)

    MathSciNet  Google Scholar 

  19. Nipkow, T., Reif, W.: An introduction to interactive theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications. Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  20. Paulson, L.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press, London (1990)

    Google Scholar 

  21. Piroi, F.: Tools for Using Automated Provers in Mathematical Theory Exploration. PhD thesis, RISC, Johannes Kepler University, Linz, Austria (August 2004)

    Google Scholar 

  22. Rosenkranz, M.: A new symbolic method for solving linear two-point boundary value problems on the level of operators. J. Symb. Comp. 39(2), 171–199 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  23. Schubert, T., Biggs, J.: A tree-based, graphical interface for large proof development. In: 7th Int. Workshop, HOL Theorem Proving and Its Applications (1994)

    Google Scholar 

  24. Siekmann, J., Benzmüller, C., Autexier, S.: Computer Supported Mathematics with ΩMEGA. J. Applied Logic (2005) To appear in [4].

    Google Scholar 

  25. Siekmann, J., Hess, S., Benzmüller, C., Cheikhrouhou, L., Fiedler, A., Horacek, H., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Pollet, M., Sorge, V.: LΩUI: Lovely Ωmega User Interface. Formal Aspects of Computing 11(3), 326–342 (1999)

    Article  Google Scholar 

  26. Syme, D.: A new interface for HOL—ideas, issues and implementation. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 324–339. Springer, Heidelberg (1995)

    Google Scholar 

  27. Tomuţa, E.: An Architecture for Combining Provers and its Applications in the Theorema System. PhD thesis, Johannes Kepler University, Linz (July 1998)

    Google Scholar 

  28. Völker, N.: Thoughts on requirements and design issues of user interfaces for proof assistants. Electronic Notes in Theoretical Computer Science 103, 139–159 (2004)

    Article  Google Scholar 

  29. Wiedijk, F.: Comparing mathematical provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 188–202. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  30. Wolfram, S.: The Mathematica Book, 5th edn. Wolfram Media Inc. (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Johann Radon Institute for Computational and Applied Mathematics, Austrian Academy of Sciences, A-4040, Linz, Austria

    Florina Piroi

  2. Research Institute for Symbolic Computation, Johannes Kepler University, A-4040, Linz, Austria

    Temur Kutsia

Authors
  1. Florina Piroi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Temur Kutsia
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Miami, USA

    Geoff Sutcliffe

  2. University of Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Piroi, F., Kutsia, T. (2005). The Theorema Environment for Interactive Proof Development. In: Sutcliffe, G., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3835. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11591191_19

Download citation

  • DOI: https://doi.org/10.1007/11591191_19

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-31650-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation