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 32 articles , 1 standard article )
Showing results 1 to 20 of 32.
Sorted by year (- 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)
- 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: A flexiformal model of knowledge dissemination and aggregation in mathematics (2015)
- Iancu, Mihnea; Kohlhase, Michael: Math literate knowledge management via induced material (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)
- Kohlhase, Michael: A data model and encoding for a semantic, multilingual terminology of mathematics (2014)
- Carette, Jacques (ed.); Aspinall, David (ed.); Lange, Christoph (ed.); Sojka, Petr (ed.); Windsteiger, Wolfgang (ed.): Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8--12, 2013. Proceedings (2013)
- Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef: The Mizar Mathematical Library in OMDoc: translation and applications (2013)