Graphentheoretische Untersuchung von Beweisgraphen

Die Graphentheorie hat sich als günstiger Rahmen für zahlreiche Anwendungen erwiesen, da strukturelle Relationen zwischen einzelnen Objekten dargestellt und untersucht werden können (z.B. Gas- oder Elektrizitätsverteilungsnetze, Molekularstrukturen, Straßenpläne in der Transportlogistik, Soziogramme und Kommunikationsstrukturen). Im vorgeschlagenen Projekt sollen Graphen erforscht werden, die den strukturellen Aufbau von formalen Beweisen veranschaulichen. Die Entwicklung der Computertechnik hat dem formalen Beweis neue praktische Anwendungen gebracht, da mit ihm das automatisierte Auswerten einer Datenbasis beschrieben werden kann. Durch besseres Verstehen des strukturellen Aufbaus können automatische Auswertungen effizienter gestaltet und Wartezeiten verkürzt werden. Einzelne graphentheoretische Methoden sind bereits auf Beweise und deren Struktur angewandt worden, jedoch erschweren die syntaktischen Eigenheiten einzelner Beweissysteme die Anwendung von komplexen graphentheoretischen Methoden. Unter Mitwirkung des Antragstellers wurde ein neues abstraktes Graphenmodell (PROOF GRAPHS) entwickelt, das die Struktur von Beweisen, unabhängig von Eigenheiten einzelner Beweissysteme, darstellen kann. Das neue Modell ermöglicht eine klare und direkte Charakterisierung solcher Strukturen. Das geplante Forschungsprojekt ist in drei Phasen unterteilt. In der ersten Phase werden bestehende Beweissysteme betrachtet und die entsprechenden PROOF GRAPHS untersucht. Die zweiten Phase konzentriert sich auf die Anwendung spezieller graphentheoretischer Methoden (im besonderen Graphenhomomorphismen und die Abspaltung von Knoten) auf PROOF GRAPHS. Die letzte Phase ist der Analyse von Graphenklassen (wie ebene Graphen, n-reguläre Graphen, Eulersche Graphen, kritische Graphen) im Hinblick auf Ergebnisse der vorhergehenden Phasen gewidmet. Die theoretische Arbeit soll durch Computerexperimente, basierend auf dem Library of Efficient Data types and Algorithms (LEDA, Max-Planck-Institut Saarbrücken), begleitet werden.

Durch graphentheoretische Methoden können gewisse Erfüllbarkeitsprobleme effizient gelöst werden. Dies ist sowohl für die theoretische Informatik, als auch für praktische Anwendungen (z.B. der Verifikation von Computerchips) von Bedeutung. Die Frage, ob eine aussagenlogische Formel erfüllbar ist (kurz "SAT-Problem" genannt), ist von großer praktischer als auch theoretischer Bedeutung: Zum einen lassen sich viele Fragestellungen die sich in angewandter Technik ergeben, als SAT-Probleme formulieren (z.B. Verifikation von Computerchips, Sicherheitsüberprüfung von Signalanlagen, etc.) - zum anderen hält das SAT-Problem eine prominente Stelle innerhalb der Theoretischen Informatik und Komplexitätstheorie inne (das SAT-Problem war das erste als NP-vollständig identifizierte Problem). Im betrachteten Forschungsprojekt wurden kombinatorische Strukturen ("Beweisgraphen" oder "proof graphs") verwendet, um Instanzen des SAT-Problems zu modellieren. Durch diese Darstellung war es möglich, graphentheoretische Methoden auf das SAT-Problem anzuwenden. Es hat sich gezeigt, dass dies im Besonderen bei der Zuordnungstheorie (ein Teilgebiet der Graphentheorie) vorteilhaft ist: es konnten effiziente Algorithmen zur Erkennung gewisser Teilklassen von minimal unerfüllbaren Formeln entwickelt werden, womit eine Vermutung von Kleine Büning bewiesen wurde. Weiters konnte das Konzept der Graphen-Homomorphismen erfolgreich auf Beweisgraphen angewandt werden, woraus sich neue Resultate innerhalb der Theorie der aussagenlogischen Beweissysteme ergaben. Beispielsweise konnte eine neue Charakterisierung der sogenannten Baumresolution gefunden werden.