Developing methods and tools for interfacing logics and proof systems used in automated reasoning, mathematics and software engineering

• Applicants: Professor Dr. Michael Kohlhase; Professor Dr. Till Mossakowski
• Subject Area: Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
• Term: from 2009 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 153521782

„Das Projekt LATIN zielt ab auf die Entwicklung von Methodiken, Techniken und Werkzeugen für die Vernetzung von Logiken und Beweissystemen. Mit Logiken kann das mathematische Wissen in Wissenschaft, Entwicklung, und industriellen Kontexten für Theorembeweiser, Model-Checker, Computeralgebrasysteme, Constraintlöser oder deduktive Datenbanken zugänglich gemacht werden. Leider haben diese Systeme unterschiedliche Eingabesprachen und Grundannahmen und sind dadurch nur in seltensten Fällen interoperabel. LATIN soll die meta-theoretischen Grundlagen von Logiken mit dem mathematischen Wissen zusammen im selben System formalisieren, auf meta-logischer Ebene zu vernetzen und dadurch logikübergreifend einzusetzen. Dieser “Logiken-als-Theorien”-Ansatz macht sowohl Systemverhalten als auch representiertes Wissen interoperabel. Um das LATIN zu evaluieren und die Interoperabilität deduktiver Softwaresysteme zu unterstützen, wird das Projekt einen Atlas wichtiger Logiken erstellen. Wir werden uns auf paradigmatische Logiken erster (TPTP, CASL und Mizar), höherer Stufe (PVS, Isabelle/HOL, HasCASL) und metalogischer Frameworks (LF und Isabelle) konzentrieren. Alle diese Logiken werden wir im LATIN-Framework repräsentieren und durch Logikmorphismen verbinden. Schließlich werden wir versuchen, den Logikatlas dadurch nachhaltig verfügbar und zukunftssicher zu machen, dass wir ein Community-Portal, einen Werkzeugkasten und Arbeitsabläufe entwickeln, die es externen Entwicklern erlauben, ihre jeweiligen Logiken in den Logikatlas zu integrieren, indem sie diese im LATIN-Framework repräsentieren und mit Logikmorphismen einpassen.“

• DFG Programme: Research Grants