Biform Theories in Chiron
William M. Farmer
2007
Abstract
An axiomatic theory represents mathematical knowledge declaratively as
a set of axioms. An algorithmic theory represents mathematical
knowledge procedurally as a set of algorithms. A biform theory is
simultaneously an axiomatic theory and an algorithmic theory. It
represents mathematical knowledge both declaratively and procedurally.
Since the algorithms of algorithmic theories manipulate the syntax of
expressions, biform theories -- as well as algorithmic theories -- are
difficult to formalize in a traditional logic without the means to
reason about syntax. Chiron is a derivative of
von-Neumann-Bernays-Goedel (NBG) set theory that is intended to be a
practical, general-purpose logic for mechanizing mathematics. It
includes elements of type theory, a scheme for handling undefinedness,
and a facility for reasoning about the syntax of expressions. It is
an exceptionally well-suited logic for formalizing biform theories.
This paper defines the notion of a biform theory, gives an overview of
Chiron, and illustrates how biform theories can be formalized in
Chiron.