The MMT Language and System

The LATIN Project: Logic Atlas and Integrator

LATIN aims at developing methods, techniques, and tools for interfacing logics and proof systems. Logics allow making the mathematical knowledge at the core of science, engineering, and economics accessible to computational systems like (semi-)automated theorem provers, model checkers, computer algebra systems, constraint solvers, or concept classifiers. Unfortunately, these systems have differing foundational assumptions and input languages, which makes them non-interoperable and difficult to compare and evaluate in practice.

The LATIN project focuses on developing a foundationally unconstrained framework for knowledge representation that allows to represent the meta-theoretic foundations of the mathematical knowledge in the same format and to interlink the foundations at the meta-logical level. This approach of logics as theories leads to interoperability of both system behavior and represented knowledge.

To evaluate the developed framework and provide a service to the community, the project will build an atlas of logics used in automated reasoning, mathematics, and software engineering concentrating on paradigmatic logics from first-order logic (TPTP, CASL, and Mizar), higher-order logics (PVS, Isabelle/HOL, HasCASL), and logical frameworks (LF and Isabelle). For all of these we will build logic representations in our framework and (where possible) structure and relate them using logic morphisms.

Finally we will make the logic atlas sustainable and future-proof by developing a community portal, a tool suite, and a workflow that allow outside users to add their logics to the Logic Atlas by representing them in the LATIN framework and provide interoperability-inducing logic morphisms.

Institutions, Members, and Funding

LATIN is a joint research project between the KWARC research group at Jacobs University Bremen and the research department Safe and Secure Cognitive Systems at the German Research Center for Artificial Intelligence Bremen (DFKI-Bremen). It is funded 2010-2011 by the German Research Council (DFG) under grant KO-2428/9-1.

Members of LATIN are Michael Kohlhase, Till Mossakowski, Florian Rabe, Mihai Codescu and Fulya Horozal.

At Jacobs University, also involved are Christoph Lange and Vyacheslav Zholudev. Students involved in LATIN are Kristina Sojakova, Stefania Dumbrava, Catalin David, Alin Iacob, Mihnea Iancu, Iulia Ignatov, Corneliu-Claudiu Prodescu, Jonathan von Schroeder and Martha Rohte.

Main systems used in LATIN

The following systems and technologies are employed, designed, and/or developed within LATIN:

  • the HETS system (Heterogeneous Tool Set): a logical framework based on model theory and institutions that uses logic translations to mediate between languages and systems (developed at DFKI Bremen),
  • the Twelf system: a logical framework based on proof theory and dependent type theory (developed at Carnegie Mellon University), which we equipped with an MMT-based module system,
  • the OMDoc format: an XML-based document format for mathematical content developed at Jacobs University (developed at Jacobs University),
  • the MMT language and system: a fragment of OMDoc designed as a scalable, foundation-independent module system for mathematical theories (developed at Jacobs University),
  • the TNTBase system: a database combining SVN and XML functionalities (developed at Jacobs University with support from DFKI Bremen),
  • the JOBAD framework: a !JavaScript library for interactive mathematical documents (developed at Jacobs University).

LATIN Atlas

LATIN will provide both a logical framework with a strong theoretical foundation, a scalable infrastructure for this framework, and a library of formalizations in it. On the theoretical side, LATIN will extend and unify the languages of Twelf, MMT, and Hets in order to provide a comprehensive logical framework. Applying the infrastructure to the library, we obtain a more tangible deliverables of the project: the LATIN Atlas of logics.

The formalizations underlying the LATIN Atlas use the new Twelf module system and are available at [https://gl.mathhub.info/MMT/LATIN]. In particular, the folders contain:

  • Type theories: formal languages based on typed expressions including a modular development of the lambda cube, Martin-L&öunl; Type Theory, and the type theory of Isabelle,
  • Logics: formal languages using formulas and truth including first-order, higher-order, modal, and description logics, usually including both proof and model theory,
  • Set theories: formal languages based on sets, including Zermelo-Fraenkel and the Mizar variant of Tarski-Grothendieck set theory,
  • Mathematics: some case studies from mathematics leveraging modularity,
  • Logic translations: a growing number of logic translations including , e.g., the relativization translations from modal, description, and sorted first-order logics to unsorted first-order logics, the interpretation of type theory in set theory, the negative translation from classical to intuitionistic logic, and the translation from first to higher-order logic.

When the LATIN project finished, the atlas was taken over by the OAF project. That also maintains the browsable HTML+MathML version of the atlas. The web server uses a conversion of the Twelf sources into OMDoc/MMT and stores them in MathHub. Then the MMT web server retrieves the needed document fragments from MathHub and assembles the requested document on the fly. Then it uses notation definitions to render it into JOBAD-enabled XHTML+MathML. This already yields some useful non-trivial services such as folding and toggling the display of brackets, inferrable types, and implicit arguments.

A SVG image of the current snapshot of the LATIN graph is available here.

Papers (including drafts and preprints)