Symbolic Computation Group

David R. Cheriton School of Computer Science
University of Waterloo, Waterloo, Ontario, Canada

MathScheme: A New Approach to Mechanized Mathematics
William M. Farmer, McMaster University
Friday, January 14, 2005, at U. of Western Ontario.


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.

This is joint work with Jacques Carette and Martin v. Mohrenschildt.


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