Automated Reasoning, das automatische Schlussfolgern oder automatische Beweisen, ist eine relativ junge Disziplin. Sie kombiniert das bereits antike Wissen der Logik und der Philosophie mit moderner Mathematik und Technik. Ziel ist die Entwicklung von Computerprogrammen, die korrekt und vollkommen automatisch mathematische Sätze beweisen können. In meiner Arbeit verwende ich täglich solche Computerprogramme, was Automated Reasoning zu einem zentralem Konzept meiner Forschung macht.

Wozu automatisches Beweisen?

Wenn man nicht gerade Mathematiker*in ist, gibt es neben mehreren weniger bekannten, eine zentrale Motivation für automatisch generierte Beweise: Sie ermöglichen uns Programme zu verifizieren. Das heißt, durch Automated Reasoners (also diese Computerporgramme) können Software Entwickler prüfen, ob sich ihre Software so verhält wie sie das auch soll.

Sie denken jetzt womöglich: Moment - wird das nicht ohnehin kontrolliert? Jein. Es wird getestet, aber nicht verifiziert. Beim Testen probiert man, nach einem gewissen Schema, einzelne Fälle aus und überprüft dann das Ergebnis. Es kann nicht garantiert werden, dass man dadurch alle Fehler im Computerprogramm findet. Durch die Anwendung von Automated Reasoners allerdings, entsteht ein mathematischer Beweis, dass sich die entwickelte Software immer so verhält wie erwartet.

Wie funktioniert automatisches Beweisen?

Kommen wir noch einmal zu dem Beispiel im Titel zurück. Hoch mathematisch geben wir dem Inhalt Buchstaben: aus Bauer wird B, aus Zimmer wird Z, aus Schlafwandler wird W und aus schlafen wird S. Um zu sagen, dass der Bauer schläft, schreiben wir S(B). Wir wollen beweisen, dass die Aussage

•  "Wenn Bauer B kein Schlafwandler W ist

  nicht W(B)

• und wenn er im Zimmer Z steht,

  Z(B)

• dann schläft er nicht."

  nicht S(B)

immer gilt. Automated Reasoners können aber nur entscheiden ob etwas möglich oder unmöglich ist, nicht ob etwas korrekt ist. Das ist glücklicherweise kein Problem. Wir können unsere Frage nämlich verneint stellen und erhalten trotzdem den Beweis den wir suchen. Wir können fragen ob es möglich ist, dass B kein Schlafwandler ist, im Zimmer steht und schläft.

nicht W(B) und Z(B) und S(B)

Erhalten wir unmöglich (unsatisfiable) als Antwort, so ist unsere Aussage bewiesen.

Geben wir nun einem Automated Reasoner diese Information, beginnt er so lange Schlussfolgerungen zu ziehen bis entweder

1. ein Widerspruch entsteht - dann wäre das Resultat unmöglich. In diesem Fall kann man nicht alle Bedingungen gleichzeitig erfüllen,
2. oder es keine neuen Schlussfolgerungen mehr gibt. Dann wäre das Resultat möglich. Man kann alle Bedingungen gleichzeitig erfüllen.

[Anmerkung: Es gibt mehrere Herangehensweisen um zu solchen Antworten zu kommen. Hier habe ich exemplarisch Refutation und Saturation beschrieben.]

Um Schlussfolgerungen zu ziehen, hat der Automated Reasoner - zusätzlich zur von uns bereitgestellten Information - gewisse "Naturgesetze" die immer gelten und die angewendet werden. In unserem Beispiel kann man als solches annehmen:

Wenn eine Person x im Zimmer steht, ist sie entweder wach oder eine Schlafwandlerin:

wenn Z(x) dann nicht S(x) oder W(x)

Fassen wir nun das Wissen (Information + Naturgesetze) des Automated Reasoners zusammen:

• Der Bauer steht im Zimmer Z(B).
• Durch das Naturgesetz muss er also entweder wach sein (nicht S(B)) oder schlafwandeln W(B).
• Aber unsere Information sagt er schläft S(B) und ist kein Schlafwandler (nicht W(B)).
• Das ist ein Widerspruch!
• Die Information ist unmöglich.

Wie zuvor erklärt, beweist das unsere ursprüngliche Aussage.

In tatsächlichen Automated Reasonern sind die "Naturgesetze" natürlich andere. Es handelt sich um mathematische Grundannahmen, sogenannte Axiome, wie zum Beispiel x+y = y+x.

Verwendung und Relevanz

Heute ist Automated Reasoning ein sehr aktiver Forschungsbereich mit vielen Forschungsgruppen an top Universitäten weltweit. Doch nicht nur die Forschung sondern auch die Wirtschaft zeigt sich vermehrt interessiert an dieser und ähnlichen Methoden um die Korrektheit von Software zu garantieren. Amazon hat mittlerweile mehrere Automated Reasoning Teams, Microsoft hat sogar ein eigenes öffentlich zugängliches Programm zur Softwareverifikation entwickelt (Dafny) und auch Intel, Meta und Ethereum beschäftigen Automated Reasoning Experten um ihre Systeme sicherer zu machen.

Abschließend lässt sich sagen, dass Automated Reasoning noch in den Kinderschuhen steckt und laufend spannende neue Erkenntnisse veröffentlicht werden. Die beiden Netidee Stipendien Automated Software Verification with First-Order Theorem Provers und Automated Diagnosis of Heisenbugs sind tolle Beispiele dafür.

Nach drei Blogs, habe ich nun endlich alle Bausteine (Blockchain Technologie, Spieltheorie und Automated Reasoning) in der Hand um über meine eigentliche Forschung zu berichten. Im nächsten Blog werde ich erklären, wie ich die drei vorgestellten Bereiche zu einem innovativen Forschungsprojekt kombiniere.