The MMT API: a generic MKM system

DOI10.1007/978-3-642-39320-4_25MaRDI QIDQ2843035zbMATH OpenOpenAlexFDO

Authors Florian Rabe

Publication date 9 August 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.3199

Mathematics Subject Classification ID

Knowledge representation (68T30)

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

• A scalable module system
• Towards MKM in the large: modular representation and scalable software architecture
• Virtual theories -- a uniform interface to mathematical knowledge bases
• A query language for formal mathematical libraries
• Generic literals

Cited in

(25)

• The future of logic: foundation-independence
• JEFL: joint embedding of formal proof libraries
• A scalable module system
• Software citations, information systems, and beyond
• Math Literate Knowledge Management via Induced Material
• Towards Knowledge Management for HOL Light
• Formal logic definitions for interchange languages
• Aligning concepts across proof assistant libraries
• Matching concepts across HOL libraries
• Towards MKM in the large: modular representation and scalable software architecture
• A data model and encoding for a semantic, multilingual terminology of mathematics
• Flexary operators for formalized mathematics
• Extending MKM formats at the statement level
• A query language for formal mathematical libraries
• Generic literals
• Classification of alignments between concepts of formal mathematical systems
• Lax theory morphisms
• MMT
• A bi-directional extensible interface between Lean and Mathematica
• Discourse-level parallel markup and meaning adoption in flexiformal theory graphs
• Experiences from exporting major proof assistant libraries
• A flexiformal model of knowledge dissemination and aggregation in mathematics
• Implementing type theory in higher order constraint logic programming
• MathTools: an open API for convenient MathML handling
• Virtual theories -- a uniform interface to mathematical knowledge bases

Describes a project that uses

Uses Software

• TNTBase
• QMT

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)