Beweisstrukturen: Beweise als formale Objekte und als Datenstrukturen

• Antragsteller: Dr. Christoph Wernhard
• Fachliche Zuordnung: Bild- und Sprachverarbeitung, Computergraphik und Visualisierung, Human Computer Interaction, Ubiquitous und Wearable Computing
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 457292495

Das geplante Projekt ist im Gebiet des Automated Reasoning angesiedelt, einem zentralen Teilgebiet der Künstlichen Intelligenz, das die Untersuchung des schließenden Denkens mit Hilfe des Computers zum Gegenstand hat. Typische Systeme des Automated Reasoning erstellen Beweisstrukturen: Repräsentationen von Beweisen, verknüpften Folgerungsschritten, durch Datenstrukturen. Beweisstrukturen lassen sich einerseits als formale Objekte betrachten, die in Beziehung zu logischen Formeln stehen, andererseits als Datenobjekte, die die formalen Objekte materialisieren und für praktische Anwendungen nutzbar sind. Ausgehend von der Untersuchung von Beweisstrukturen in diesem Sinn strebt das Projekt sowohl die Verbesserung der Leistungsfähigkeit von Systemen des Automated Reasoning beim Finden von Beweisen als auch die Erweiterung ihres Anwendungsspektrums über reine Beweisaufgaben hinaus an.Neben dem für das Gebiet des Automated Reasoning charakteristischen Zusammenspiel theoretischer und experimenteller Methoden ist die Analyse gegebener Beweise ein besonderer methodischer Aspekt des Projekts. Relevant ist dabei insbesondere ein umfangreicher Korpus komplexer formaler Beweise in der Literatur aus der Zeit vor der breiten Verfügbarkeit von Computern, die mit automatisierten Methoden immer noch nicht in zufriedenstellender Weise gefunden werden können.Konkrete Ziele des Projekts sind: (1) Die Verbesserung der Leistungsfähigkeit prädikatenlogischer Theorembeweiser beim Finden von Beweisen, insbesondere durch neuartige Kalküle, geleitet durch Abstraktionen, die sich aus der Orientierung an Beweisstrukturen ergeben und durch Beobachtungen bei der Analyse von Beweisen. (2) Theoretisch gut verstandene und implementierte Beweistransformation für verschiedene praktische Anwendungen wie etwa die Verkleinerung oder Vereinfachung von Beweisen, die Entdeckung und Abstraktion von Wiederholungen und Regelmäßigkeiten in Beweisen, oder die Abbildung zwischen Kalkülen, um die Kombination unterschiedlicher Systeme zu ermöglichen. (3) Anwendung von prädikatenlogischen Beweissystemen für die Umformulierung von Datenbankanfragen zur Integration von Datenbanken und Wissensbasen sowie zur Anfrageoptimierung. Geplant ist, einen Ansatz zur Umformulierung von Anfragen weiterzuentwickeln, der auf Craig-Interpolation beruht, einer grundlegenden Beziehung in Prädikatenlogik erster Stufe von Beweisstrukturen zu assoziierten Formeln. (4) Fortschritte bezüglich weiterführender Fragen von theoretischem und praktischem Interesse, die mit den im Projekt betrachteten Kerntechniken, Craig-Interpolation und Condensed Detachment, in Zusammenhang stehen. Condensed Detachment ist die primäre Beweisrepräsentation in der analysierten Literatur. Ziele sind dabei insbesondere die Überwindung bekannter Einschränkungen, Erkenntnisse über Bezüge zu weiteren Techniken sowie die Erschließung weiterer Anwendungsmöglichkeiten.

• DFG-Verfahren: Sachbeihilfen