Stärkere Beweisautomatisierung via nichtklausale Beweissuche

Automatische Theorembeweiser sind Computerprogramme, die mathematische Aussagen, wie z.B. den Satz von Pythagoras, ohne menschliche Unterstützung beweisen. Um dies zu bewerkstelligen, bringen die meisten Theorembeweiser die zu beweisende mathematische Aussage in eine für den Computer einfacher zu verarbeitende Form, nämlich in sogenannte Klauseln. Solche Beweiser nennt man klausal. Die Umwandlung in Klauseln kann jedoch den Beweis vieler Aussagen bedeutend erschweren. Für solche Fälle bieten sich nichtklausale Theorembeweiser an, die nicht auf die Umwandlung in Klauseln angewiesen sind. Obwohl nichtklausale Theorembeweiser attraktive theoretische Eigenschaften besitzen, sind sie derzeit noch wenig erforscht und können infolgedessen mit klausalen Theorembeweisern noch nicht mithalten. Wir möchten Methoden erforschen, um nichtklausale Theorembeweiser stärker zu machen. Unsere Hypothese ist, dass gut ausgeführte nichtklausale Theorembeweiser nicht nur in der Theorie, sondern auch in der Praxis ihre Vorteile gegenüber klausalen Theorembeweisern ausspielen können. Als erstes möchten wir theoretische Eigenschaften eines nichtklausalen Theorembeweisers mithilfe eines Computerprogramms überprüfen, um eine solide theoretische Basis für unsere weitere Forschung zu erhalten. Als nächstes möchten wir auf dieser Grundlage die Effizienz eines existierenden nichtklausalen Theorembeweisers steigern. Schlussendlich möchten wir die dabei gewonnenen Erkenntnisse nutzen, um eine nichtklausale Version eines der besten klausalen Theorembeweiser zu erstellen. Dies ermöglicht uns, einen direkten Vergleich zwischen klausalen und nichtklausalen Theorembeweisern anzustellen und somit unsere Hypothese zu überprüfen.

Der Einsatz kritischer Computerprogramme, wie z.B. zur Steuerung von Infrastruktur (Fahrzeuge, Kraftwerke, Dämme etc.), unterliegt strengen Sicherheitskriterien. Nehmen wir als Beispiel ein Programm zur Steuerung einer automatischen U-Bahn: Dieses Programm muss einige Eigenschaften (auch genannt *Aussagen*) erfüllen, z.B. dass Züge nur mit geschlossenen Türen fahren und niemals mit anderen Zügen kollidieren. Vor dem Einsatz eines solchen Programms müssen *Beweise* vorgelegt werden, dass das Programm tatsächlich die gewünschten Aussagen erfüllt. Die manuelle Überprüfung solcher Beweise ist jedoch fehleranfällig und kann Menschenleben kosten. Daher werden solche Beweise mithilfe von eigenen Programmen, nämlich sogenannten *Beweisprüfern*, überprüft. Dies setzt voraus, dass sowohl die Aussagen als auch deren Beweise in einer für den Beweisprüfer verständlichen Form vorliegen. Da die händische Erstellung solcher Beweise sehr zeitaufwändig ist, verwendet man andere Programme, nämlich sogenannte *(automatische) Theorembeweiser*, die viele solche Beweise ohne menschliche Unterstützung finden. Je mehr Beweise ein Theorembeweiser findet, umso weniger Beweise müssen händisch erstellt werden, was die Zeit und die Kosten zur Überprüfung kritischer Programme reduziert. Im Rahmen dieses Forschungsprojekts haben wir die Leistungsfähigkeit von Theorembeweisern und von Beweisprüfern verbessert. Zuerst haben wir untersucht, wie man die Menge der von einem *Theorembeweiser* in gegebener Zeit beweisbaren Aussagen vergrößern kann. Zu diesem Zweck haben wir einen existierenden Theorembeweiser modifiziert. Der Theorembeweiser verfügt über mehrere Heuristiken zur Beweissuche. Die besten Heuristiken schränken den Suchraum solchermaßen ein, dass sie zwar nicht alle theoretisch existierenden Beweise finden können, jedoch in der Praxis mehr Beweise in kurzer Zeit finden. Wir haben durch Zufall eine neue Heuristik namens REX entdeckt, die im Vergleich zur vorher besten Heuristik den Suchraum auf subtile Art weniger einschränkt. Wir haben für mehrere Datensätze von aus der Praxis stammenden Aussagen untersucht, wieviele Aussagen verschiedene Heuristiken beweisen können. Bei allen Datensätzen erhöhte sich die Anzahl der gefundenen Beweise, wenn REX statt der bisher besten Heuristik verwendet wurde, in einem Fall bis zu 19%. Als nächstes haben wir untersucht, wie man die Geschwindigkeit von *Beweisprüfern* erhöhen kann. Beweise, die automatisch (z.B. von Theorembeweisern) erzeugt werden, können oftmals sehr große Ausmaße annehmen. Die Verarbeitung solcher großen Beweise durch bisherige Beweisprüfer kann einige Zeit in Anspruch nehmen, was die Produktivität mindert. Bisherige Beweisprüfer haben Beweise sequentiell, also einen nach dem anderen, verarbeitet. In diesem Projekt haben wir ein neues Design für Beweisprüfer eingeführt, das die parallele, gleichzeitige Überprüfung mehrerer Beweise ermöglicht. Die besondere Herausforderung bestand darin, die Geschwindigkeit zu erhöhen, ohne jedoch die strengen Ansprüche an die Korrektheit von Beweisprüfern abzuschwächen. Der resultierende Beweisprüfer ist in der Lage, eine große Menge von Beweisen mehr als sieben Mal so schnell wie der bisher schnellste Beweisprüfer zu verarbeiten. Durch unsere Verbesserungen von automatischen Theorembeweisern und Beweisprüfern kann die Sicherheit von kritischen Programmen schneller und günstiger überprüft werden.