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.
The original LATIN project ran from 2009-2012.
The MMT Archive LATIN2 is a from-scratch revision of the original logic atlas.