**
The Power of Examples: sqrt(2)+sqrt(3) from Four Different Viewpoints **

Susan Landau University of Massachusetts Amherst `landau@cs.umass.edu`

Mathematics gives delightful interplay between the particular and the
abstract, between examples that guide and proofs that convince. Symbolic
computation can provide the computational power to discover and understand
deep and rich theorems. In this talk, I will discuss one example that
underlies four theorems in different, though related, areas: polynomial
factorization, subfield determination, polynomial decomposition, and
denesting of radicals.

**
Computing with large systems of linear Diophantine equations **

Mark Giesbrecht University of Manitoba `mwg@cs.umanitoba.ca`

`http://www.cs.umanitoba.ca/~mwg`

Finding exact integer solutions to linear systems of integer equations
is an intriguing and fundamental problem in computational mathematics.
Many applications arise in number theory, group theory and
combinatorics. In this talk we will survey a number of algorithms for
solving such Diophantine systems and for computing normal forms which
describe the structure of all solutions. Beginning with methods of
Hermite (1851) and Smith (1861), we trace the development of effective
algorithms for these problems and especially the rapid progress of the
past decade in both algorithms and motivating applications. The
emphasis here will be on provable efficiency, both in terms of time
and memory use. We will also discuss some important applications
which require the solution of systems which are extremely large but
sparse, i.e., many of the coefficients are zero. For these it becomes
essential to exploit this sparsity, and we will demonstrate how recent
algorithms for solving large sparse systems over finite fields can be
adapted to this case.

**
Theorem Prover Support for Computer Algebra Systems **

Robert L. Constable Cornell University `rc@CS.Cornell.EDU`

At first glance it seems that theorem provers could provide support for
computer algebra systems by verifying their algorithms. Although this
role might eventually become significant, it is not the main one that
we have pursued at Cornell. We have used the Nuprl proof development
system to provide a semantic basis for algebraic domains, as in Axiom,
to provide extended type checking capabilities, and to formalize
subtyping and inheritance relations found in algebra. Paul Jackson's
formalization of algebraic domains is available at the Nuprl home page
(follow links from www.cs.cornell.edu).

The design of a system to support both algebra and theorem proving has
led us to ideas for an architecture based around a "software bus" for
exchanging terms between systems. In an article entitled Collaborative
Mathematics Environments (see links from the home page), we describe
this architecure which is being used in Nuprl 5 and in a MathBus
project of R. Zippel which grew out of work in trying to link Nuprl and
the Weyl computer algebra system. Nuprl uses the MathBus terms to
communicate with other systems.

*Gene Cooperman*

*8/31/1997*