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.
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.
The following systems and technologies are employed, designed, and/or developed within LATIN:
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:
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.
LATIN final report, 2012.
M. Codescu, F. Horozal, T. Mossakowski, and F. Rabe. Compiling Logics, Abstract in WADT 2012.
F. Horozal and F. Rabe. Representing Categories of Theories in a Proof-Theoretical Framework, Abstract in WADT 2012.
M. Codescu, F. Horozal, I. Ignatov, and F. Rabe. Representing CASL in a Proof-Theoretical Framework, Abstract in WADT 2012.
F. Horozal, M. Kohlhase, and F. Rabe. Extending MKM Formats at the Statement Level, CICM 2012.
F. Horozal and F. Rabe. Representing Logics of Theorem Provers — TLTP: Tens of Logics for Theorem Provers, draft, 2012.
M. Iancu, M. Kohlhase, and F. Rabe. Translating the Mizar Mathematical Library into OMDoc format, KWARC-Report, 2011.
F. Horozal, A. Iacob, C. Jucovschi, M. Kohlhase, and F. Rabe. Combining Source, Content, Presentation, Narration and Relational Representation, CICM 2011.
M. Codescu and T. Mossakowski, Refinement trees: calculi, tools and applications, CALCO 2011, LNCS.
M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe, LATIN project abstract, CICM 2011.
M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe and K. Sojakova, Towards Logical Frameworks in the Heterogeneous Tool Set Hets, WADT 2010, to appear in LNCS.
M. Codescu and F. Horozal and M. Kohlhase and T. Mossakowski and F. Rabe, A Proof Theoretic Interpretation of Model Theoretic Hiding, WADT 2010, to appear in LNCS.
M. Codescu, Lambda Expressions in CASL Architectural Specifications, WADT 2010, to appear in LNCS.
M. Iancu and F. Rabe, Formalizing Foundations of Mathematics, Mathematical Structures in Computer Science, 2011.
Over the recent decades there has been a trend towards formalized mathematics, and a number of sophisticated systems have been developed to support the formalization process and mechanically verify its result. However, each tool is based on a specific foundation of mathematics, and formalizations in different systems are not necessarily compatible. Therefore, the integration of these foundations has received growing interest. We contribute to this goal by using LF as a foundational framework in which the mathematical foundations themselves can be formalized and therefore also the relations between them. We represent three of the most important foundations – Isabelle/HOL, Mizar, and ZFC set theory – as well as relations between them. The relations are formalized in such a way that the framework permits the extraction of translation functions, which are guaranteed to be well-defined and sound. Our work provides the starting point of a systematic study of formalized foundations in order to compare, relate, and integrate them.
Mihai Codescu, Till Mossakowski, Adrían Riesco, Christian Maeder, Integrating Maude into Hets, AMAST 2010, LNCS.
K. Sojakova, Mechanically Verifying Logic Translations, Master’s Thesis, Jacobs University, 2010.
F. Horozal, M. Kohlhase, F. Rabe, K. Sojakova, Towards an Atlas of Logics, the first paper about LATIN as a whole.
F. Rabe, Representing Isabelle in LF, LFMTP 2010.
F. Horozal and F. Rabe, Representing Model Theory in a Type-Theoretical Logical Framework, Special issue on “Logical and Semantic Frameworks with Applications 8+9”, Journal of Theoretical Computer Science, 2011.
F. Rabe and M. Iancu, A Formalized Set-Theoretical Semantics of Isabelle/HOL
F. Horozal and F. Rabe, Representing Model Theory in a Type-Theoretical Logical Framework, Fourth Workshop on Logical and Semantic Frameworks, with Applications, 2009.
F. Rabe and C. Schürmann, A Practical Module System for LF the Twelf instantiation of the MMT module system, LFMTP 2009.