Rabe F, Weber F (2023)
Publication Type: Conference contribution
Publication year: 2023
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 14101 LNAI
Pages Range: 174-189
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Cambridge, GBR
ISBN: 9783031427527
DOI: 10.1007/978-3-031-42753-4_12
Theory graphs have theories as nodes and theory morphisms as edges. They can be seen as generators of categories with the nodes as the objects and the paths as the morphisms. But in contrast to generated categories, theory graphs do not allow for an equational theory on the morphisms. That blocks formalizing important aspects of theory graphs such as isomorphisms between theories. MMT is essentially a logic-independent language for theory graphs. It previously supported theories and morphisms, and we extend it with morphism equality as a third primitive. We show the importance of this feature in several elementary formalizations that critically require stating and proving certain non-trivial morphism equalities. The key difficulty of this approach is that important properties of theory graphs now become undecidable and require heuristic methods.
APA:
Rabe, F., & Weber, F. (2023). Morphism Equality in Theory Graphs. In Catherine Dubois, Manfred Kerber (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 174-189). Cambridge, GBR: Springer Science and Business Media Deutschland GmbH.
MLA:
Rabe, Florian, and Franziska Weber. "Morphism Equality in Theory Graphs." Proceedings of the Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023, Cambridge, GBR Ed. Catherine Dubois, Manfred Kerber, Springer Science and Business Media Deutschland GmbH, 2023. 174-189.
BibTeX: Download