=ADD=
=author=
Buchberger; Bruno
=title=
Symbolic Computation: Computer Algebra and Logic
=number=
96-36
=month=
12
=year=
1996
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1996/96-36.ps.gz
=abstract=
In this paper we present our personal view of what should be the nextstep 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.
=howpublished=
F.  Baader, K.U.  Schulz (eds.) Frontiers of Combining Systems.
Applied Logic Series. Kluwer Academic Publishers, 1996.
=location=
2
=owner=
2
=source=
3
=reftype=
14