Skip to content
Snippets Groups Projects
Forked from KWARC / kwarc.info / www
782 commits behind the upstream repository.
latin.md 1.26 KiB
layout: project

title: "LATIN: Logic Atlas & Integrator"
teaser: Building a theory graph of logic represesentations. 

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

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.