A biform theory is a combination of an axiomatic theory and an algorithmic
theory that supports the integration of reasoning and computation. These are
ideal for specifying and reasoning about algorithms that manipulate
mathematical expressions. However, formalizing biform theories is challenging
since it requires the means to express statements about the interplay of what
these algorithms do and what their actions mean mathematically. This paper
describes a project to develop a methodology for expressing, manipulating,
managing, and generating mathematical knowledge as a network of biform
theories. It is a subproject of MathScheme, a long-term project at McMaster
University to produce a framework for integrating formal deduction and symbolic
computation.