KnowledgeBase » SEMINAR » ID = 421

Computer Algebra, Theorem Proving, and Types

by Todd Wilson
1994-1995

Abstract

Many computations a mathematician performs can be described in "algebraic" terms, that is, as dealing with various symbolic entities that are combined in restricted ways and are subject to laws (e.g., equations) specifying which combinations are equivalent. The term "computer algebra", as it appears in my title, has this general sense (as opposed to the more restrictive sense of "computational commutative algebra"), and my talk will discuss this subject and its relation to automatic theorem proving and type theory.

In more detail, the talk will consist of the following:

• A survey of examples of computer algebra drawn from several areas of mathematics, including commutative algebra and algebraic geometry, invariant theory, (algebraic) number theory, group theory, Lie algebra, combinatorics, algebraic topology, and analysis (scientific computation).
  
• A discussion of the roles automatic theorem proving might have in these fields.
• A discussion of types, including
  • The purpose and advantages of using types in computer algebra,
  • An analysis, based on the examples before, of what type constructions are needed for computer algebra, and
  • A look at the type system of AXIOM and how it shapes up.

Concluding remarks on the relationship between types and theorem proving and a prospectus for what can (and should) be done in this area.