1. The LATIN Project: Logic Atlas and Integrator
    1. Institutions, Members, and Funding
    2. Main systems used in LATIN
    3. LATIN Atlas
    4. Papers (including drafts and preprints)
    5. Other Information

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 in a separate  SVN repository. In particular:

  •  Type theory: 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 theory: 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.

The browsable XHTML+MathML version of the atlas is available at  here. The web server uses a conversion of the Twelf sources into OMDoc/MMT and stores them in TNTBase. Then the MMT web server uses XQueries to retrieve the needed document fragments from TNTBase and assemble 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. However, when browsing it, keep in mind that both the formalizations themselves and the TNTBase-MMT-JOBAD infrastructure serving them are part of the LATIN project and thus subject to both constant improvement and temporary failures.

Papers (including drafts and preprints)

Other Information

The administrators of this Trac page are Fulya Horozal and Vyacheslav Zholudev.