Connecting Proof Checkers and Computer Algebra Using OpenMath
Interactive mathematics over the Internet is particularly appealing in that it can take advantage of the wealth of resources available online. In particular, a problem-solving framework integrating computing and proving tools is of great interest. Several modes of advantageous cooperation can be envisioned. Proving is undoubtedly useful to computation for checking assertions and side conditions, whereas computation is useful for shortening the lengths of proofs. Both modes are definitely needed in interactive mathematics. In the interaction we do not want to waste resources by sending or receiving meaningless requests. There Strong OpenMath comes in, as it is possible to type-check the well-typedeness, hence the meaningfullness, of the mathematical objects it represents.
Unable to display preview. Download preview PDF.
- John A. Abbott, André van Leeuwen, and A. Strotmann. OpenMath: Communicating Mathematical Information between Co-operating Agents in a Knowledge Network. Journal of Intelligent Systems, 1998. Special Issue: “Improving the Design of Intelligent Systems: Outstanding Problems and Some Methods for their Solution.”.Google Scholar
- A. M. Cohen, H. Cuypers, and H. Sterk. Algebra Interactive, interactive course material. Number ISBN 3-540-65368-6. SV, 1999.Google Scholar
- S. Dalmas, M. Gaëtano, and S. Watt. An OpenMath 1.0 Implementation. pages 241–248. ACM Press, 1997.Google Scholar
- Z. Luo and R. Pollack. LEGO Proof Development System: User’s Manual. Department of Compter Science, University of Edinburgh, 1992.Google Scholar
- PolyMath OpenMath Development Team. Java openmath library, version 0.5. Available at http://pdg.cecm.sfu.ca/openmath/lib/, July 1998.
- Projet Coq. The Coq Proof Assistant: The standard library, version 6.1 edition. Available at http://www.ens-lyon.fr/LIP/groupes/coq.
- The OpenMath Consortium. The OpenMath Standard. OpenMath Deliverable 1.3.1a, September 1998. Public at http://www.nag.co.uk/projects/OpenMath.html.