Logic Atlas, Version 2

Core formalizations of (elementary) mathematics in MMT

The logical foundation(al theories) used by MitM projects

Metalogical frameworks that extend LF - the Edinburgh Logical Framework. These provide common features - e.g. record types, subtyping, or flexary functions - of logical languages at the meta-level for inheritance in LFX-specified logics.

The Formalizations for the UFrameIT-based serious game FrameWorld.

Paradigmatic examples of MMT content. They are used for development and regression testing.

This repository contains the MMT-translation of the SoftwareFoundations book.

Shabbar Raza's code for finding alignments based on matching names.

The Logic Atlas and Integrator project content (still in TWELF, not MMT syntax)