MMT - Language and System for the Uniform Representation of Knowledge

Documentation Research Download Community
MMT integrates the 4 major paradigms for representing scientific knowledge. All aspects of MMT avoid a commitment to semantic foundation, representational paradigm, or application work flow.
Representation Languages
MMT represents all knowledge in one simple framework
  • Subsumes virtually any declarative language
  • Uniform treatment of virtually any formal object
  • Powerful module system
  • Highly extensible at all levels
Narration
MMT subsumes natural languages
  • Seamless mixing of formal/informal content
  • Arbitrary concrete syntax: presentation MathML, LaTeX, ...
  • Graceful degradation of formal algorithms to narrative content
  • Deep integration with LaTeX authoring workflow
Applications
MMT enables generic large-scale implementations
  • IDE for semantics editing support
  • Build Manager for incremental, parallel compilation
  • Semantics-aware content browser
  • Project hosting platform
  • Interoperability layer for semantics-preserving knowledge exchange
Deduction
MMT subsumes logical languages
  • Declarative definitions of logics including syntax, proof theory, model theory
  • Modular composition of logics from library of language features
  • Rapid prototyping of logical systems
  • No foundational commitment to a formal system or semantics
hover over a feature to see details
Theory morphisms uniformly represent
  • abstraction and refinement,
  • inclusion and inheritance,
  • functors and parametrization,
  • translations and interpretations.
MMT declarations uniformly represent
  • sort, type, universe symbols,
  • constant, function, predicate symbols,
  • connectives, binders, operators,
  • axioms, theorem, inference rules.
MMT declarations uniformly represent
  • types, kinds,
  • terms, function, formulas,
  • literals of any kind,
  • proofs, derivations.
MMT theories can introduce not only new symbols but also notations, implementation rules, and high-level language features.
MMT acts as a jEdit plugin to provide IDE functionality.
The MMT web browser provides numerous advanced features including interactive type inference or definition lookup.
The MMT build manager is designed for fast rebuilding of large projects including arbitrary importers and exporter for external formats.
MathHub builds on MMT and GitLab to provide a GitHub-style platform for mathematics.
MMT uses theories as interfaces to bridge between different languages.
MMT notations support mixfix syntax, precedences, implicit arguments, binding, sequence arguments/variables.
Reconstruction of omitted types and implicit arguments in the presence of dependent types, polymorphism, rewriting, ...
Arbitrary computation and rewrite rules.
MMT will allow interpretation of stateful programs.
Only 3 rules yield a basic theorem prover for forward- and backward chaining. No limitation with respect to advanced prover infrastructures.
Generation of arbitrary formats such as high-quality presentation MathML using only notations.
Differencing of concrete and abstract syntax for fast rechecking.
General query language and MathWebSearch allow fast search in large libraries.
MMT archives allow for collaboration, hosting, and distribution of projects.
Formal objects inside rigorous but informal documents.
Informal comments inside formal representations.
Escape back and forth between MMT and e.g., HTML and LaTeX.
Algorithms like type-checking of formulas perform as good as they can in the presence of narrative subformulas.
sTeX package for LaTeX allows semantic markup of narrative LaTeX documents.
mmt package for LaTeX allows type-checking and type-setting MMT formulas.
Logics are defined as theories in the logical framework.
The LATIN project has built a library of logic features, e.g.,
  • conjunction
  • lambda-abstraction
  • excluded middle
  • set theoretical models
MMT systematically avoids any commitment. All logical features are represented in the framework.
The logical framework is itself flexible, and different frameworks can be composed modularly.
Current work transfers the framework built for logics languages to programming languages.
Features of programming languages and their semantics and interrelations will be represented declaratively in MMT.
Type systems, computation features, and interpretation rules will be declared modularly and composed to form individual programming languages.
MMT will allow representing proofs and programs in the same formalism.
This avoids an ontological distinction between tactics (programs about proofs) and software verification (proofs about programs).
MMT supports finitary representations of complex mathematical objects that can be stored in standard databases and easily interchanged and queried.
Type-driven codecs are used to convert automatically between high-level mathematical representations and standard database languages for efficient low-level representation.
MMT allows using high-level languages to query the low-level representations.
Used in OpenDreamKit for LMFDB, OEIS, findstat.
Computation
MMT will subsume programming languages
  • Object-oriented, functional, and imperative features
  • Declarative definitions of programming languages
  • Modular composition of programming languages and their semantics
  • Seamlessly program about logics, reason about programs
Soundness-Critical Services
MMT allows generic solutions to deep problems
  • Parsing
  • Type Checking
  • Simplification
  • Computation (ongoing)
  • Theorem Proving (ongoing)
All algorithms are rule-based and rules can be combined modularly.
Thus, languages can be modified at minimal cost.
Tabulation
MMT subsumes data description languages
  • Concrete representation of abstract mathematical objects
  • Standardized codec language for interchanging data
  • Uniform query language across databases (ongoing)
  • Integrated with major databases of computational mathematics
Management Services
MMT allows generic knowledge management solutions
  • Rendering using MathML
  • Search and Querying
  • Change Management
  • Project Management