Abstract
In this paper we present our personal view of what should be the next step in the development of symbolic computation systems. The main point is that future systems should integrate the power of algebra and logic. We identify four gaps between the future ideal and the systems available at present: the logic, the syntax, the mathematics, and the prover gap, respectively. We discuss higher order logic without extensionality and with set theory as a subtheory as a logic frame for future systems and we propose to start from existing computer algebra systems and proceed by adding new facilities for closing the syntax, mathematics, and the prover gaps. Mathematica seems to be a particularly suitable candidate for such an approach. As the main technique for structuring mathematical knowledge, mathematical methods (including algorithms), and also mathematical proofs, we underline the practical importance of functors and show how they can be naturally embedded into Mathematica.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P.B. Andrews: An Introduction toMathematical Logic and Type Theory: To Truth Through Proof.Academic Press, London 1986.
B. Buchberger: Groebner Bases: An Algorithmic Method in Polynomial Ideal Theory. Chapter 6 in:Multidimensional Systems Theory, (N.K. Bose ed.). D. Reidel Publishing Company, Dordrecht, 1985.
B. Buchberger: Induction Proofs in Equational Logic: A Case Study Using Mathematica.Internal Technical Report, The RISC Institute, A4232 Schloss Hagenberg, Austria, 1995.
G.E. Collins: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. Proceedings of the Second GI Conference on Automata Theory and Formal Languages.Lecture Notes in Computer Science, 33, pp. 515–532, Springer, Heidelberg, 1975.
R. Constable:The Nuprl System.Lecture Notes of the Summer School on Logic of Computation, Marktoberndorf 1995. Edited by Institut für Informatik, Technische Universität München, 1995.
G. Huet: The CIC System. Lecture Notes of the Summer School onLogic of Computation, Maxktoberndorf 1995. Edited by Institut für Informatik, Technische Universität München, 1995.
D. Kapur, P. Narendran, H. Zhang: Automating Inductionless Induction using Test SetsJournal of Symbolic Computation, Vol. 11, No. 1&2, February 1991, pp. 83–111.
N. Soiffer:Mathematical Typesetting in Mathematica.Proceedings of the ISSAC 1995 Conference, pp. 140–149.
S. Wolfram: Mathematica:A System for Doing Mathematics by Computers.Addison- Wesley Publishing Company, Redwood, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 Springer Science+Business Media New York
About this chapter
Cite this chapter
Buchberger, B. (1996). Symbolic Computation: Computer Algebra and Logic. In: Baader, F., Schulz, K.U. (eds) Frontiers of Combining Systems. Applied Logic Series, vol 3. Springer, Dordrecht. https://doi.org/10.1007/978-94-009-0349-4_10
Download citation
DOI: https://doi.org/10.1007/978-94-009-0349-4_10
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-6643-3
Online ISBN: 978-94-009-0349-4
eBook Packages: Springer Book Archive