Musik

Ja, guten Morgen.

Ich bin jetzt in der Arbeitszeit. Wir haben uns das letzte Mal mit Prolog beschäftigt

oder angefangen uns mit Prolog zu beschäftigen und waren letztlich von der Logik erster Stufe gekommen

und das Ganze ist sehr nahe aneinander. Die Idee von Prolog ist, dass man die Welt in einer Wissensbank beschreibt

und dann Anfragen an diese Wissensbank stellt. Und es gibt zwei Hauptmotoren von der ganzen Geschichte,

wie bei eigentlich allen First-Order-Sachen. Es gibt einmal Suche, Suche nach Antworten, Suche über den propositionalen Teil

und auf dem anderen Teil ist das Ganze Unifikation. Unifikation versucht, Terme gleich zu machen.

Und das ist auch wo wir im Prinzip gestartet waren. Wir hatten uns diesen Algorithmus angeguckt.

Es gibt drei Regeln. Das dadurch induzierte Inferenzsystem hat gute Eigenschaften. Das ist korrekt, vollständig, unitär, konfluent, terminierend.

Und das gibt uns dann letztlich einen Algorithmus und insbesondere eine Entscheidungsprozedur.

Und wir hatten uns Terminationen angeguckt und dann auf der Unifikation aufgebaut, angeguckt wie Resolutionen und Tableau funktionieren.

Das war es, was wir gemacht hatten. Und im Wesentlichen hatten wir uns Beispiele angeguckt.

Wir haben uns hier Colonel West angeguckt, was hier zu so einem Beweis führt in der Resolution.

Wir erinnern uns, wenn wir zwei Klauseln haben, also Disjunktionen, die komplementär machbare Literale haben,

dann können wir die wegschneiden, den Rest aufsammeln und mit der Substitution, die wir zum Gleichmachen der Literale benutzt haben,

können wir das Ganze solange machen, bis wir irgendwann mal zur leeren Klausel kommen.

Das ist Resolutionsbeweis, ist im automatischen Beweisen erster Stufe der Hauptmechanismus.

Und wir haben extrem leistungsstarke Implementationen und sie haben ja eine Hausaufgabe, in der sie die ausprobieren können.

Dann müssen sie nicht mehr so einen Krempel hier von Hand machen, sondern können das einfach an einen Beweiser verfüttern,

der dann relativ schnell einen Beweis findet oder auch nicht.

Und dann haben wir doch einen angeguckt, der so ein bisschen andere Charakteristika hat und da haben wir vor allem die Skolomisierung gesehen.

Genau. Dies hier ist jetzt in gewisser Weise allgemeines Beweisen.

Die nächsten beiden Dinge, also das, was wir den Rest des Semesters machen werden, ist, dass wir letztlich zwei Anwendungen dieser ganzen Sache angucken.

Einmal logisch programmieren. Wie kann man mit dem Zeugs programmieren? Und die andere wird sein Planung, da kommen wir dann heute zu.

Logisches Programmieren und im Prinzip sind die auch relativ nah verwandt. Prolog war der Versuch,

alle diese Techniken, die man in der KI entwickelt hat, irgendwie in einer Programmiersprache zur Verfügung stellen,

sodass man leichter mit experimentieren konnte. Und das ist auch zum guten Teil erfolgreich gewesen.

Was nie passiert ist, ist, dass irgendjemand gesagt hat, wir erweitern das um Techniken des Programmierens im Großen.

Es ist nie irgendwie sowas wie objektorientiertes Prolog oder getyptes Prolog wirklich populär geworden.

Und dadurch ist es als Programmiersprache heute nur noch in Ausnahmesituationen relevant.

Trotzdem als intellektuelles Modell ist es natürlich noch gut. Wir haben logisches Programmieren.

Die Idee ist, wie gesagt, wir schreiben in logischer Stufe eine Wissensbank auf und alles, was uns interessiert, stellen wir als Anfragen,

also als logische Atome mit Variablen da drin und wenn wir Glück haben, kommt die Antwort Ja zusammen mit einer Antwortsubstitution.

Wir haben uns das angeguckt, wir haben definiert, wie das mit dem Prolog ist.

Die Idee ist, dass die Wissensbank, eine endlich aufgeschriebene, repräsentierte Wissensbank,

ein unendlich großes Wissensraum generiert. Wir haben hier eine Situation, dass wir da das Programm haben.

Und der deduktive Abschluss, alles, was man daraus ableiten kann mittels dieser paar Regeln, die ich hier aufgeschrieben habe,

das ist irgendwie etwas Großes. Das ist so ein Wissensraum.

Und alle Dinge, die diese Wissensbank, das Programm, beantworten kann, liegen letztlich in diesem großen Raum.

Also virtuell, um die Bedeutung von Prolog zu verstehen, muss man sich über diesen Raum, den deduktiven Abschluss, Gedanken machen.

In der Praxis generieren wir den nicht, sondern durchsuchen den.

Das heißt, wenn wir irgendwo fragen wollen, hier ist ein induzierter Fakt F,

dann können wir durch eine Anfrage Q das Ganze nach diesem Fakt fragen und dann kann man zusammen letztlich einen Beweis finden,

für Q oder eben nicht finden. Das ist die Idee hier.

Wir machen sozusagen Proving on Demand, um Anfragen zu beantworten.

Und dann sind wir durch Beispiele gegangen. Und die Idee ist, dass diese Beweise werden in einer Art und Weise gesucht,

die so kontrolliert ist, dass wir als Programmierer sie voraussehen können.

Und dann benutzen wir eine sehr einfache Suchstrategie, nämlich Depth First Search. Was wir machen, ist immer,

wir haben eine Wissensbank, wir durchsuchen die von oben nach unten und benutzen die Prologregeln für Backchaining.