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 46 articles , 1 standard article )
Showing results 1 to 20 of 46.
Sorted by year (- Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan: (\mathrmLF^+) in \textttCoqfor fast-and-loose reasoning (2019)
- Amann, Kai; Kohlhase, Michael; Rabe, Florian; Wiesing, Tom: Integrating semantic mathematical documents and dynamic notebooks (2019)
- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Guidi, Ferruccio; Sacerdoti Coen, Claudio; Tassi, Enrico: Implementing type theory in higher order constraint logic programming (2019)
- Kaliszyk, Cezary (ed.); Brady, Edwin (ed.); Kohlhase, Andrea (ed.); Sacerdoti Coen, Claudio (ed.): Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8--12, 2019. Proceedings (2019)
- Rabe, Florian; Sharoda, Yasmine: Diagram combinators in MMT (2019)
- Betzendahl, Jonas; Kohlhase, Michael: Translating the IMPS theory library to MMT/OMDoc (2018)
- Rabe, Florian: A modular type reconstruction algorithm (2018)
- Rabe, Florian (ed.); Farmer, William M. (ed.); Passmore, Grant O. (ed.); Youssef, Abdou (ed.): Intelligent computer mathematics. 11th international conference, CICM 2018, Hagenberg, Austria, August 13--17, 2018. Proceedings (2018)
- Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
- Kohlhase, Michael; De Feo, Luca; Müller, Dennis; Pfeiffer, Markus; Rabe, Florian; Thiéry, Nicolas M.; Vasilyev, Victor; Wiesing, Tom: Knowledge-based interoperability for mathematical software systems (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)
- Wiesing, Tom; Kohlhase, Michael; Rabe, Florian: Virtual theories -- a uniform interface to mathematical knowledge bases (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)
- Kohlhase, Michael; Rabe, Florian: QED reloaded: towards a pluralistic formal library of mathematical knowledge (2016)
- Rabe, Florian: The future of logic: foundation-independence (2016)