Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Wunderbar. Also, wir haben gestern logisch erste Stufe abgeschlossen, haben uns im Wesentlichen

den neuen Teil an First-Order-Inferenz angeguckt, nämlich in Unifikation. Unifikation ist ein

Algorithmus, der technisch gesehen erstmal einfach nur zwei Terme gleich macht und zwar

syntaktisch gleich unter einer Substitution, also eine Substitution findet, die das macht.

Und die wir, wir haben es in der Resolution gesehen, wir haben es im Tableau gesehen,

die einer der Basisfunktionalitäten ist, die es uns erlaubt, die Instanzen, also die Terme,

die wir für universell quantifizierte Variablen einsetzen wollen, spät zu finden. Nämlich

genau dann, wenn wir schon wissen, wo wir resolvieren wollen oder wo wir im Tableau

einen Ast schließen wollen. Da haben wir dann mehr Informationen, der es uns erlaubt,

die Substitutionen zu berechnen, statt sie einfach raten zu müssen. Und im Prinzip ist

Unifikation der Mechanismus, der in der Inferenz erster Stufe den Durchbruch gebracht hat.

Seitdem sind Theoremenbeweiser machbar. Stand der Kunst ist, dass, wie in allen diesen anderen

Sachen gibt es eine Theoremenbeweiser-Competition jedes Jahr, in dem die Beweiser gegeneinander

antreten und interessante Probleme, auch mathematische Probleme, lösen und zum Teil

auch offene mathematische Probleme tatsächlich beweisen. Theoremenbeweiser, wie alle diese

anderen Dinge, die wir haben, sind im Echteinsatz, werden benutzt, zum Beispiel in der Programmverifikation.

Intel zum Beispiel verifiziert alle seine Chips und verifiziert die Intel C-Library,

dass die auch tatsächlich richtig rechnet. Das hilft einem nicht vor Spectre und Merckdown,

weil das auf einer anderen Ebene ist. Man muss immer sagen, gegen was verifiziert man.

Also sowas wie Prefetch und Speculative Execution oder sowas. Auf der Ebene wird Intel vielleicht

bald verifiziert. Das könnte ich mir durchaus vorstellen. Aber es braucht ja immer erst

mal so eine Katastrophe, dass man dann die Deiche baut oder sowas. Und Programmverifikation

ist so ein Deich und ist ohne solche Rechnerunterstützung kaum noch möglich. Weil wir Menschen einfach

nicht so schnell und effizient relativ einfache Probleme lösen können. Typischer automatischer

Beweiser für Phasorologik kann die typischen Geschichten wie Colonel West mal 10, 20 in

der Größe in sowas wie 100 Millisekunden lösen. Und damit kann man dann schon was machen.

Also lösen auf einem Prozessor, das heißt man kann so was machen wie alle, also 10 Probleme

in so einem System pro Sekunde geben. Das heißt man kann ganz viele Dinge einfach, wo man

die Vorstellungen rauskompiliert, dann diesen System. Genau, Unifikation. Wir wollen alle

Unifikatoren für eine Termgleichung finden. Und wie machen wir das? Wir machen das per

Inferenz wieder. Wir suchen nach gelösten Formen, von denen man die Lösung ablesen kann.

Und wir machen das durch ein Inferenzsystem. Hier diese drei Regeln. Und die haben wir

uns sehr genau angeguckt, weil das eine andere Art und Weise ist, Algorithmen sich genau anzugucken.

Wir haben sonst immer sowas wie mit Pseudocode gemacht. Hier machen wir keinen Pseudocode.

Ich gehe davon aus, dass Sie das einfach im Pseudocode übersetzen können. Aber diese

Ebene, wenn man schon sehr gut strukturierte Objekte hat, in diesem Fall Terme und nicht

irgendwie Listen und Arrays oder so etwas, dann sollte man auch die Tools benutzen, die

man hat. Wir haben uns Beispiele angeguckt, wir haben uns Terminationen angeguckt, wo

man Terminationen, wie eigentlich immer, beweist, indem man irgendetwas zählt und das muss dann

kleiner werden. In diesem Fall und sehr häufig in Algorithmen ist es nicht ganz einfach,

rauszukriegen, was denn eigentlich kleiner wird und das Argument dann zu fabrizieren.

Und hier hatten wir uns so ein bisschen angeguckt, so Standard-Tools, dass man versucht, irgendwie

nötige Ordnungen zu finden und dafür gibt es so die Standard-Tools mit Multimengen zu

arbeiten oder mit kathärischen Produkten, wo man wiederum nötige Ordnungen hat. Terminationen

zu beweisen ist schwer, ist echte KI, das kann man damit nicht, wie Sie wissen, nach

dem Halteproblem kann man das nicht automatisieren vollständig. Es gibt Leute, die machen es

trotzdem, das Programm dazu schreiben, die Terminationen beweisen und kommen damit auch

relativ weit. Die benutzen diese Standard-Tools, aber man kann es natürlich nicht immer.

Genau, und das hat uns dann gezeigt, dass Unifikation ein Entscheidungsverfahren ist,