latin.md

---
layout: project

title: "LATIN: Logic Atlas & Integrator"

active: false
start_date: '2009'
end_date: '2012'

people: 
    - mkohlhase
    - frabe
    - fhorozal
    - miancu

collaborators:
    - Till Mossakowski, DFKI Bremen

funding: DFG
program: Normalverfahren
grantid: KO 2428/9-1
---

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.