Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 2001: Theorem Proving in Higher Order Logics pp 27–42Cite as

Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

  • Conference paper
  • First Online:

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

Abstract

We describe an interface between version 6 of the Maple computer algebra system with the PVS automated theorem prover. The interface is designed to allow Maple users access to the robust and checkable proof environment of PVS. We also extend this environment by the provision of a library of proof strategies for use in real analysis. We demonstrate examples using the interface and the real analysis library. These examples provide proofs which are both illustrative and applicable to genuine symbolic computation problems.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abbott, J., Van Leeuwen, A., AND Strotman, A. Objectives of OpenMath. Available from, Jan. 1995, http://www.rrz.uni-koeln.de/themen/Computeralgebra/OpenMath/.

  2. Adams, A., Gottliebsen, H., Linton, S., AND Martin, U. Automated theorem proving in support of computer algebra: symbolic definite integration as a case study. In Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, Vancouver, Canada (1999), ACM Press.

    Google Scholar 

  3. Ballarin, C., Homann, K., AND Calmet, J. Theorems and algorithms: An interface between Isabelle and Maple. In Proceedings of the International Symposium on Symbolic and Algebraic Computation (1995), A. Levelt, Ed., ACM Press, pp. 150–157.

    Google Scholar 

  4. Bauer, A., Clarke, E., AND Zhao, X. Analytica-an experiment in combining theorem proving and symbolic computation. Journal of Automated Reasoning 21 (1998), 295–325.

    Article  MATH  MathSciNet  Google Scholar 

  5. Bertoli, P., Calmet, J., Guinchiglia, F., AND Homann, K. Specification and integration of theorem provers and computer algebra systems. In Artificial intelligence and symbolic computation (Plattsburgh, NY, 1998), no. 1476 in Lecture Notes in Computer Science. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  6. Buchberger, B. Symbolic computation: Computer algebra and logic. In Frontiers of Combining Systems (1996), F. Baader and K. Schultz, Eds., Applied Logic Series, Kluwer Academic Publishers, pp. 193–220.

    Google Scholar 

  7. Buchberger, B. Jebelean, T., Kriftner, F., Marin, M., Tomuta, E., AND Vasaru, D. A survey of the theorema project. In Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation (1997), W. Kuechlin, Ed., ACM Press, pp. 384–391.

    Google Scholar 

  8. Calmet, J., AND Homann, K. Classification of communication and cooperation mechanisms for logical and symbolic computation systems. In Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich (Germany) (1996), F. Baader and K. U. Schulz, Eds., Applied Logic, Kluwer, pp. 221–234.

    Google Scholar 

  9. Char, B. W.Maple V language Reference Manual. Springer-Verlag, 1991.

    Google Scholar 

  10. Dennis, L. A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., AND Melham, T. The PROSPER Toolkit. In Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2000), vol. 1785 of Lecture Notes in Computer Science, Springer-Verlag.

    Chapter  Google Scholar 

  11. Dewar, M. Special Issue on OPENMATH. ACM SIGSAM Bulletin 34, 2 (June 2000).

    Google Scholar 

  12. Dolzmann, A., AND Sturm, T. REDLOG: Computer algebra meets computer logic. A CM SIGSAM Bulletin 31, 2 (June 1997), 2–9.

    Article  MathSciNet  Google Scholar 

  13. Dutertre, B. Elements of mathematical analysis in PVS. In Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’ 96 (Turku, Finland, Aug. 1996), J. von Wright, J. Grundy, and J. Harrison, Eds., vol. 1125 of Lecture Notes in Computer Science, Springer-Verlag, pp. 141–156.

    Google Scholar 

  14. Gottliebsen, H. Transcendental Functions and Continuity Checking in PVS. In Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 (2000), J. Harrison and M. Aagaard, Eds., vol. 1869 of Lecture Notes in Computer Science, Springer-Verlag, pp. 198–215.

    Chapter  Google Scholar 

  15. Gray, S., Kajler, N., AND Wang, P. S. MP: A Protocol for Efficient Exchange of Mathematical Expressions. In Proc. of the International Symposium on Symbolic and Algebraic Computation (ISSAC’94), Oxford, GB (July 1994), M. Giesbrecht, Ed., ACM Press, pp. 330–335.

    Google Scholar 

  16. Harrison, J., AND Théry, L. Reasoning about the reals: the marriage of HOL and Maple. In Logic Programming and Automated Reasoning (1993), A. Voronkov, Ed., no. 698 in Lecture Notes in Artificial Intelligence, LPAR’93, Springer-Verlag, pp. 351–359.

    Google Scholar 

  17. Jackson, P.Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Apr. 1995.

    Google Scholar 

  18. Jenks, R. D., AND Sutor, R. S.AXIOM: the scientific computation system. Numerical Algorithms Group Ltd., 1992.

    Google Scholar 

  19. Monagan, M., Geddes, K., Heal, K., Labahn, G., Vorkoetter, S., AND McCarron, J.Maple6 Programming Guide. Waterloo Maple Inc., 2000.

    Google Scholar 

  20. Murphy, G. M.Ordinary differential equations and their solutions. D. van Nostrand Company, Inc., 1960.

    Google Scholar 

  21. Owre, S., Shankar, N., AND Rushby, J. M.User Guide for the PVS Specification and Verification System. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993.

    Google Scholar 

  22. Owre, S., Shankar, N., Rushby, J. M., AND Stringer-Calvert, D. W. J.PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA, Sept. 1999.

    Google Scholar 

  23. Owre, S., Shankar, N., Rushby, J. M., AND Stringer-Calvert, D. W. J.PVS System Guide. Computer Science Laboratory, SRI International, Menlo Park, CA, Sept. 1999.

    Google Scholar 

  24. Paulson, L. C.The Isabelle Reference Manual. Computer Laboratory, University of Cambridge, February 2001.

    Google Scholar 

  25. Poll, E., AND Thompson, S. Adding the axioms to AXIOM: Towards a system of automated reasoning in Aldor. Tech. Rep. 6-98, Computing Laboratory, University of Kent at Canterbury, May 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of CS, Cyb and University of Reading, Reading, RG6 6AY, UK

    Andrew Adams

  2. NAG LTD, Wilkinson House, Jordan Hill Road, Oxford, OX2 8DR, UK

    Martin Dunstan

  3. School of Computer Science, University of St. Andrews, St Andrews, KY16 9SS, UK

    Hanne Gottliebsen, Tom Kelsey & Ursula Martin

  4. Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA, 94025, USA

    Sam Owre

Authors
  1. Andrew Adams
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Dunstan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hanne Gottliebsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tom Kelsey
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ursula Martin
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Sam Owre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, Glasgow, G12 8QQ, Scotland, UK

    Richard J. Boulton

  2. Division of Informatics, University of Edinburgh, James Clerk Maxwell Building, King’s Buildings, Edinburgh, EH9 3JZ, Scotland, UK

    Paul B. Jackson

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., Owre, S. (2001). Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-44755-5_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42525-0

  • Online ISBN: 978-3-540-44755-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation