Certified Computer Algebra on Top of an Interactive Theorem Prover

1. Armando, A., Zini, D.: Towards interoperable mechanized reasoning systems: the logic broker architecture. In: Corradi, A., Omicini, A., Poggi, A. (eds.) WOA, Pitagora Editrice Bologna, pp. 70–75 (2000)

   Google Scholar 

2. Aslaksen, H.: Multiple-valued complex functions and computer algebra. SIGSAM Bulletin (ACM Special Interest Group on Symbolic and Algebraic Manipulation) 30(2), 12–20 (1996)

   MATH  Google Scholar 

3. Ballarin, C., Paulson, L.C.: A pragmatic approach to extending provers by computer algebra - with applications to coding theory. Fundam. Inf. 39(1-2), 1–20 (1999)

   MATH  MathSciNet  Google Scholar 

4. Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: an interface between Isabelle and Maple. In: ISSAC 1995. Proceedings of the 1995 international symposium on Symbolic and algebraic computation, pp. 150–157. ACM Press, New York (1995)

   Chapter  Google Scholar 

5. Barendregt, H., Cohen, A.M.: Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants. J. Symb. Comput. 32(1/2), 3–22 (2001)

   Article  MATH  MathSciNet  Google Scholar 

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

   Article  MATH  MathSciNet  Google Scholar 

7. Bertoli, P., Calmet, J., Giunchiglia, F., Homann, K.: Specification and integration of theorem provers and computer algebra systems. Fundam. Inform. 39(1-2), 39–57 (1999)

   MATH  MathSciNet  Google Scholar 

8. Buchberger, B., et al.: The Theorema Project: A Progress Report. In: Kerber, M., Kohlhase, M. (eds.) Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS, Natick, Massachusetts, A.K. Peters (2000)

   Google Scholar 

9. Carette, J., Farmer, W., Wajs, J.: Trustable communication between mathematics systems. In: CALCULEMUS 2003, Rome, Italy, Aracne, pp. 55–68 (2003)

   Google Scholar 

10. Carlisle, D., Ion, P., Miner, R., Poppelier, N.: Mathematical Markup Language (MathML) Version 2.0, 2nd edn. (2003)

    Google Scholar 

11. Char, B.W., Geddes, K.O., Gentleman, W.M., Gonnet, G.H.: The design of Maple: A compact, portable and powerful computer algebra system. Springer, London (1983)

    Google Scholar 

12. Coq Development Team. The Coq Proof Assistant Reference Manual Version 8.0. INRIA-Rocquencourt (January 2005)

    Google Scholar 

13. Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9 (1997)

    Article  MathSciNet  Google Scholar 

14. Adams, A., et al.: Computer algebra meets automated theorem proving: Integrating Maple and PVS. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 27–42. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

15. Buswell, S., et al.: The OpenMath Standard, version 2.0 (2002)

    Google Scholar 

16. Harrison, J.: HOL light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

17. Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. Journal of Automated Reasoning 21, 279–294 (1998)

    Article  MATH  MathSciNet  Google Scholar 

18. Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, Ithaca, NY, USA (January 1995)

    Google Scholar 

19. Lester, D.R.: Effective continued fractions. In: Proceedings 15th IEEE Symposium on Computer Arithmetic, pp. 163–170. IEEE Computer Society Press, Washington (2001)

    Google Scholar 

20. Poll, E., Thompson, S.: Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor. In: Calculemus and Types 1998 (July 1998)

    Google Scholar 

21. Sorge, V.: Non-trivial symbolic computations in proof planning. In: Kirchner, H. (ed.) Frontiers of Combining Systems. LNCS, vol. 1794, pp. 121–135. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

22. Vuillemin, J.: Exact real computer arithmetic with continued fractions. In: LFP 1988. Proceedings of the 1988 ACM conference on LISP and functional programming, pp. 14–27. ACM Press, New York (1988)

    Chapter  Google Scholar 

23. Wester, M.J. (ed.): Contents of Computer Algebra Systems: A Practical Guide, chapter A Critique of the Mathematical Abilities of CA Systems. John Wiley & Sons, Chichester, United Kingdom (1999)

    Google Scholar 

Download references