A MMT counterpart to the elementary math in SMGloM

version 2 of the LATIN atlas

a research paper describing the export from Isabelle to OMDoc/MMT that is used to generate the MMT projects in this group

documentation for SMGloM project

The SMGloM contributions of Gabriel Cunningham.

The SMGloM contributions of Jukka Kohonen.

Examples for Grammatical Logical Framework (GLF)

Slides and notes for talks held by Michael Kohlhase

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

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

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 slides and course notes of the course Computational Logic at Jacobs University.

Elementary physics

The course materials for the Lecture Logic Based Language Processing at FAU

The course notes and slides of the course "Informatische Werkzeuge der Geistes- und Sozialwissenschaften" at FAU Elangen-Nürnberg