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.

翻译：双形理论是一种不言而喻的理论和一种算法理论的结合,它支持了推理和计算的综合。它们是说明和推理操作数学表达的算法的理想。然而,正式化双形理论具有挑战性,因为它要求用各种手段来表达关于这些算法的相互作用及其行动在数学方面的含义。本文描述了一个开发一种表达、操纵、管理和生成数学知识的方法的项目,作为双形理论的网络。这是一个MathScheme的子项目,这是McMaster大学的一个长期项目,旨在形成一个将正式推算和符号计算结合起来的框架。