William M. Farmer
Department of Computer Science
McMaster University

"Biform Theories: A Basis for Integrating and Generalizing Computer Theorem Proving and Computer Algebra"

ABSTRACT: MathScheme is a project to develop a new approach to mechanized mathematics in which computer theorem proving and computer algebra are integrated and generalized. The immediate goals of the project are (1) to develop a *formal framework for managing mathematics* and (2) to design and implement a *microkernel* of a mechanized mathematics system based on the framework. The central idea of the framework is the notion of a *biform theory* which can include both formulas and algorithms as axioms. Simultaneously an *axiomatic theory* and an *algorithmic theory*, a biform theory provides a formal context for both deduction and computation. Indeed, a network of biform theories linked by interpretations is the basis for a mixture of deduction and computation called *derivation*. This talk will explain what biform theories are, how they support derivation, and how they are created and developed. (Joint work with Martin v. Mohrenschildt)

Back to Talks Page