Realms: A Structure for Consolidating Knowledge about Mathematical
Theories
Jacques Carette, William M. Farmer, and Michael Kohlhase
2014
Abstract
Since there are different ways of axiomatizing and developing a
mathematical theory, knowledge about a such a theory may reside in
many places and in many forms within a library of formalized
mathematics. We introduce the notion of a realm as a structure
for consolidating knowledge about a mathematical theory. A realm
contains several axiomatizations of a theory that are separately
developed. Views interconnect these developments and establish that
the axiomatizations are equivalent in the sense of being mutually
interpretable. A realm also contains an external interface that is
convenient for users of the library who want to apply the concepts and
facts of the theory without delving into the details of how the
concepts and facts were developed. We illustrate the utility of
realms through a series of examples. We also give an outline of the
mechanisms that are needed to create and maintain realms.