Abstract
An intelligent mathematical environment must enable symbolic mathematical computation and sophisticated reasoning techniques on the underlying mathematical laws. This paper disscusses different possible levels of interaction between a symbolic calculator based on algebraic algorithms and a theorem prover. A high level of interaction requires a common knowledge representation of the mathematical knowledge of the two systems. We describe a model for such a knowledge base mainly consisting of type and algorithm schemata, algebraic algorithms and theorems.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Bosma, J. Cannon, Handbook of MAGMA Functions, Sydney, 1994.
J. Calmet, K. Homann, I.A. Tjandra, Unified Domains and Abstract Computational Structures, in J. Calmet, J.A. Campbell (eds.), International Conference on Artificial Intelligence and Symbolic Mathematical Computing, Karlsruhe, August 3–6, 1992, LNCS 737, pp. 166–177, Springer, 1993.
J. Calmet, I.A. Tjandra, A Unified-Algebra-Based Specification Language for Symbolic Computing, in A. Miola (ed.), Design and Implementation of Symbolic Computation Systems, LNCS 722, pp. 122–133, Springer, 1993.
D. Geddis, The DTP Manual, Stanford University, 1994.
A. Heck, Introduction to MAPLE, Springer, 1993.
R.D. Jenks, R.S. Sutor, AXIOM, Springer, 1992.
D.B. Lenat, J.S. Brown, Why AM and EURISKO Appear to Work, Artificial Intelligence 23, pp. 269–294, Elsevier, 1984.
W.W. McCune, OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, 1994.
L.C. Paulson, ISABELLE: A Generic Theorem Prover, LNCS 828, Springer, 1994.
J.W. Shavlik, Extending Explanation-Based Learning by Generalizing the Structure of Explanations, Pitman, London, 1990.
A. Vella, C. Vella, Artificial Intelligence and the Mathcycle, in J.H. Johnson, S. McKee, A. Vella (eds.), Artificial Intelligence in Mathematics, Oxford University Press, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Homann, K., Calmet, J. (1995). Combining theorem proving and symbolic mathematical computing. In: Calmet, J., Campbell, J.A. (eds) Integrating Symbolic Mathematical Computation and Artificial Intelligence. AISMC 1994. Lecture Notes in Computer Science, vol 958. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60156-2_3
Download citation
DOI: https://doi.org/10.1007/3-540-60156-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60156-2
Online ISBN: 978-3-540-49533-8
eBook Packages: Springer Book Archive