Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS

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