An Overview of a Formal Framework for Managing Mathematics

William M. Farmer, Martin v. Mohrenschild

2002

Abstract

Mathematics is a process of creating, exploring, and connecting
mathematical models.  This paper presents an overview of a formal
framework for managing the mathematics process as well as the
mathematical knowledge produced by the process.  The central idea of
the framework is the notion of a biform theory which is simultaneously
an axiomatic theory and an algorithmic theory.  Representing a
collection of mathematical models, a biform theory provides a formal
context for both deduction and computation.  The framework includes
facilities for deriving theorems via a mixture of deduction and
computation, constructing sound deduction and computation rules, and
developing networks of biform theories linked by interpretations.  The
framework is not tied to a specific underlying logic; indeed, it is
intended to be used with several background logics simultaneously.
Many of the ideas and mechanisms used in the framework are inspired by
the IMPS Interactive Mathematical Proof System and the Axiom computer
algebra system.

Keywords: Mechanized mathematics, theorem proving, computer algebra,
axiomatic method, little theories method.