Entwicklung von Methoden und Werkzeugen zur Vernetzung von Logiken/Beweissystemen aus autom. Beweisen, Mathematik und Softwareentwicklung

• Antragsteller: Professor Dr. Michael Kohlhase; Professor Dr. Till Mossakowski
• Fachliche Zuordnung: Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
• Förderung: Förderung von 2009 bis 2014
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 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-Verfahren: Sachbeihilfen