Realms: A Structure for Consolidating Knowledge about Mathematical Theories
Jacques Carette, William M. Farmer, Michael Kohlhase

TL;DR
The paper introduces 'realms', a structured approach to consolidating and interconnecting various axiomatizations of mathematical theories within formalized libraries, enhancing accessibility and coherence.
Contribution
It proposes the concept of realms to unify multiple axiomatizations and provides mechanisms for creating and maintaining these structures.
Findings
Realms successfully integrate different axiomatizations.
Views establish interpretability between axiomatizations.
External interfaces improve user access to theories.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Semantic Web and Ontologies · Logic, Reasoning, and Knowledge
