Angles of MMT, each one sentence

Guidelines: every item should be at most 2 sentences long; items should be comprehensible independently from each other; link to relevant papers or theses of appropriate (mention the paper name in case the site ever goes down; except for arxiv, that probably never goes down)

Angles of MMT

• MMT is a scalable module system for formalizing knowledge.
• MMT/LF induces a module system over LF.
• MMT is a foundation-independent framework for representing declarative languages such as logics, type theories, set theories.
• The MMT API implements complex algorithms generically for any language in the framework.
• MMT allows rapid prototyping of formal systems
• MMT allows formalizing knowledge declaratively and modularly with an open-world assumption in mind.
• MMT theories represent knowledge... (in parentheses: inductive datatypes as found e.g. in Coq represent knowledge...)
  • declaratively (inductively)
  • modularly (monolithicially)
  • with an open-world assumption (closed-world assumption)
• MMT views represent knowledge
  • declaratively
  • modularly
  • with a somewhat closed-world assumption (due to compositionality)
• MMT views v: S -> T may represent
  • compositional language translations from S-terms to T-terms
  • special cases of meta theorems (e.g. soundness)
  • S being a generalization of T (compositionally so, see Navid Roux's B.Sc. thesis "Refactoring of Theory Graphs in Knowledge Representation Systems", Sects. 2 and 3)
  • T implementing S via v
• MMT theories, views, and pushouts allow storing, relating, and combining knowledge. (source: "FrameIT: Detangling Knowledge Management from Game Design in Serious Games", Sect. 2)