Abstracts of Invited Talks

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.