The MMT API: a generic MKM system
From MaRDI portal
Abstract: The MMT language has been developed as a scalable representation and interchange language for formal mathematical knowledge. It permits natural representations of the syntax and semantics of virtually all declarative languages while making MMT-based MKM services easy to implement. It is foundationally unconstrained and can be instantiated with specific formal languages. The MMT API implements the MMT language along with multiple backends for persistent storage and frontends for machine and user access. Moreover, it implements a wide variety of MMT-based knowledge management services. The API and all services are generic and can be applied to any language represented in MMT. A plugin interface permits injecting syntactic and semantic idiosyncrasies of individual formal languages.
Recommendations
Cited in
(27)- Aligning concepts across proof assistant libraries
- MathTools: an open API for convenient MathML handling
- MMT
- Experiences from exporting major proof assistant libraries
- Classification of alignments between concepts of formal mathematical systems
- Software citations, information systems, and beyond
- The future of logic: foundation-independence
- A bi-directional extensible interface between Lean and Mathematica
- Discourse-level parallel markup and meaning adoption in flexiformal theory graphs
- Extending MKM formats at the statement level
- A query language for formal mathematical libraries
- Generic literals
- A flexiformal model of knowledge dissemination and aggregation in mathematics
- Formal logic definitions for interchange languages
- Math Literate Knowledge Management via Induced Material
- Towards MKM in the large: modular representation and scalable software architecture
- A scalable module system
- Virtual theories -- a uniform interface to mathematical knowledge bases
- Implementing type theory in higher order constraint logic programming
- Lax theory morphisms
- A data model and encoding for a semantic, multilingual terminology of mathematics
- Matching concepts across HOL libraries
- Flexary operators for formalized mathematics
- Towards Knowledge Management for HOL Light
- Rapid prototyping formal systems in MMT: 5 case studies
- \(\mathsf{GF} + \mathsf{MMT} = \mathsf{GLF}\) -- from language to semantics through LF
- JEFL: joint embedding of formal proof libraries
This page was built for publication: The MMT API: a generic MKM system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843035)
