Symbolic Computation Group
David R. Cheriton School of Computer Science


Friday, January 14, 2005, at U. of Western Ontario.
Abstract:
Mechanized mathematics is the use of computers to automate, manage,
and improve mathematical practice. Started in 2001 at McMaster
University, MathScheme is a project to develop a new approach to
mechanized mathematics in which computer theorem proving and computer
algebra are integrated and generalized. Three ideas are central to
the approach. (1) Context is represented by biform theories which can
include both formulas and algorithms as axioms. (2) Mathematical
knowledge and reasoning is distributed across a network of
interconnected biform theories. (3) Formal deduction and symbolic
computation are merged into a single activity called derivation. The
approach is strongly influenced by the IMPS theorem proving system and
the Axiom computer algebra system. This talk will give an overview of
MathScheme's goals, accomplishments, and challenges.

Last modified on Sunday, 04 November 2012, at 15:42 hours.