Biform Theories: Project Description

Jacques Carette, William M. Farmer, and Yasmine Sharoda

2018

Abstract

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.


Keywords: Axiomatic mathematics, algorithmic mathematics, biform
theories, symbolic computation, reasoning about syntax, meaning
formulas, theory graphs.