MMT
The MMT Language. We introduce the MMT language, which provides a simple and scalable Module system for the development of Mathematical Theories. MMT permits to encode mathematical knowledge in a logic-neutral representation format that can represent the meta-theoretic foundations of mathematical and logical systems together with the represented knowledge itself and interlink the foundations at the meta-logical level. This ”logics-as-theories” approach makes system behaviors as well as their represented knowledge interoperable and thus comparable. Furthermore, MMT defines logic-independent notions of well-formedness and equivalence of modular mathematical theories. Thus, it provides an interface layer between formally rigorous mathematical systems, and knowledge management services which are not aware of the semantics of the processed knowledge
Keywords for this software
References in zbMATH (referenced in 35 articles , 1 standard article )
Showing results 1 to 20 of 35.
Sorted by year (- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Betzendahl, Jonas; Kohlhase, Michael: Translating the IMPS theory library to MMT/OMDoc (2018)
- Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
- Kohlhase, Michael; Koprucki, Thomas; Müller, Dennis; Tabelow, Karsten: Mathematical models as research data via flexiformal theory graphs (2017)
- Kohlhase, Michael; Sperber, Wolfram: Software citations, information systems, and beyond (2017)
- Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
- Rabe, Florian: How to identify, translate and combine logics? (2017)
- Dehaye, Paul-Olivier; Iancu, Mihnea; Kohlhase, Michael; Konovalov, Alexander; Lelièvre, Samuel; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Wiesing, Tom: Interoperability in the OpenDreamKit project: the math-in-the-middle approach (2016)
- Ginev, Deyan; Iancu, Mihnea; Jucovshi, Constantin; Kohlhase, Andrea; Kohlhase, Michael; Oripov, Akbar; Schefter, Jürgen; Sperber, Wolfram; Teschke, Olaf; Wiesing, Tom: The SMGloM project and system: towards a terminology and ontology for mathematics (2016)
- Rabe, Florian: The future of logic: foundation-independence (2016)
- Horozal, Fulya; Rabe, Florian: Formal logic definitions for interchange languages (2015)
- Iancu, Mihnea; Kohlhase, Michael: Math literate knowledge management via induced material (2015)
- Iancu, Mihnea; Kohlhase, Michael: A flexiformal model of knowledge dissemination and aggregation in mathematics (2015)
- Rabe, Florian: Generic literals (2015)
- Rabe, Florian: Lax theory morphisms (2015)
- Carette, Jacques; Farmer, William M.; Kohlhase, Michael: Realms: a structure for consolidating knowledge about mathematical theories (2014)
- Gauthier, Thibault; Kaliszyk, Cezary: Matching concepts across HOL libraries (2014)
- Horozal, Fulya; Rabe, Florian; Kohlhase, Michael: Flexary operators for formalized mathematics (2014)
- Iancu, Mihnea; Jucovschi, Constantin; Kohlhase, Michael; Wiesing, Tom: System description: MathHub.info (2014)
- Kaliszyk, Cezary; Rabe, Florian: Towards knowledge management for HOL Light (2014)