Biform Theories: Project Description

TL;DR

This paper introduces a project to develop a methodology for formalizing and managing mathematical knowledge through interconnected biform theories, combining axiomatic reasoning with algorithmic computation.

Contribution

It proposes a novel framework for expressing and manipulating mathematical knowledge as a network of biform theories within the MathScheme project.

Findings

Initial methodology for biform theories development

Integration of reasoning and computation in mathematical knowledge

Framework supports managing complex mathematical algorithms

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.