FAIRsharing record for: The MMT Language and System

This FAIRsharing record describes: MMT is a framework for knowledge representation using formal languages such as logics, type theories, ontologies, set theories, etc.. It achieves a high level of generality by systematically avoiding a commitment to a representational paradigm, a particular concrete or abstract syntax, or a particular semantics. Instead, individual features of the abstract syntax (e.g., lambda-abstraction, conjunction), the concrete syntax (e.g. keywords, notations), or the semantics (e.g., excluded middle, set theoretical interpretation) are defined as separate, reusable modules, from which individual languages are assembled. Despite this high degree of abstraction, it is possible to implement advanced algorithms generically at the MMT level. The MMT system includes powerful generic solutions for knowledge management (e.g. IDE, change management) and verification (e.g., type reconstruction, module system). By designing knowledge representation languages inside MMT, we can obtain strong implementations at extremely low cost.