Lightweight Realms

Kohlhase M, Rabe F, Schütz M (2025)

Publication Type: Conference contribution

Publication year: 2025

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer Science and Business Media Deutschland GmbH

Book Volume: 16136 LNCS

Pages Range: 222-239

Conference Proceedings Title: Lecture Notes in Computer Science

Event location: Brasilia, BRA BR

ISBN: 9783032070203

DOI: 10.1007/978-3-032-07021-0_13

Abstract

During formalization – e.g. of Mathematics – we have to take many decisions that informal mathematics leaves (and can leave) open. In particular, often there are multiple isomorphic ways of formalizing a set of axioms between which mathematicians can switch seamlessly. But this can impede beginners from fully understanding a domain, and it has proved difficult to mimic the same seamlessness in formalized mathematics, hindering interoperability between systems and libraries. Realms have been proposed as an explicit representation of collections of isomorphic theories and conservative extensions, but have proven difficult to implement and manage. Therefore, here we introduce a more specialized definition that, in our experience, covers a large set of practically relevant examples. The central concept is that of a base of a theory: a subtheory that uniquely determines the entire theory. This allows us to represent an entire realm as a single theory with multiple bases. We show that many foundational concepts can be elegantly represented as such basic realms. The resulting formalism offers a good abstraction level to deal with (the consequences of) differing choices in the literature and in formal libraries, thus reducing interoperability problems, while keeping the formalizations simple.

Authors with CRIS profile

Michael Kohlhase Professur für Wissensrepräsentation und -verarbeitung Florian Rabe Professur für Wissensrepräsentation und -verarbeitung Marcel Schütz Professur für Wissensrepräsentation und -verarbeitung

How to cite

APA:

Kohlhase, M., Rabe, F., & Schütz, M. (2025). Lightweight Realms. In Valeria de Paiva, Peter Koepke (Eds.), Lecture Notes in Computer Science (pp. 222-239). Brasilia, BRA, BR: Springer Science and Business Media Deutschland GmbH.

MLA:

Kohlhase, Michael, Florian Rabe, and Marcel Schütz. "Lightweight Realms." Proceedings of the 18th International Conference on Intelligent Computer Mathematics, CICM 2025, Brasilia, BRA Ed. Valeria de Paiva, Peter Koepke, Springer Science and Business Media Deutschland GmbH, 2025. 222-239.

BibTeX: Download