Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case
Study
Jacques Carette and William M. Farmer
2017
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 formalizing algorithms that
manipulate mathematical expressions. A theory graph is a
network of theories connected by meaning-preserving
theory morphisms that map the formulas of one theory to the
formulas of another theory. Theory graphs are in turn well suited for
formalizing mathematical knowledge at the most convenient level of
abstraction using the most convenient vocabulary. We are interested
in the problem of whether a body of mathematical knowledge can be
effectively formalized as a theory graph of biform theories. As a
test case, we look at the graph of theories encoding natural number
arithmetic. We used two different formalisms to do this, which we
describe and compare. The first is realized in CTT_uqe, a
version of Church's type theory with quotation and evaluation, and the
second is realized in Agda, a dependently typed programming language.