Okay, so wir sind in der Logik, logikbasierter Agenten und die Idee dabei als

Hintergrund ist, dass wir einen Agenten haben, der die Welt abbildet, der ein Weltmodell hat

und dieses Weltmodell ist in gewisser Weise sprachlicher Art. Wir haben also eine Wissensbank

aus Fakten bzw. Perzepten über die Welt und wir erschließen den Zustand der Welt, den wir

nicht sehen können oder den wir nicht direkt sehen können, erschließen wir aus dieser Wissensbank.

Diese Wissensbank ist natürlich unvollständig, potenziell unvollständig in mehreren Richtungen.

Einerseits sehen wir nicht alles über die Welt und zweitens können wir nicht alles über die

Welt schließen oder aber wir haben noch nicht dran gedacht, über gewisse Dinge nachzudenken.

Und wir hatten Verfahren gesehen, mit denen wir die Erfüllbarkeit eines Faktes aus einer

Wissensbank entscheiden können. Da hat Tableau und Resolution und im Prinzip kann man damit den

ganzen, ich will mal sagen, deduktiven Abschluss errechnen. Alles was aus dieser Wissensbank folgt,

weil jeder einzelne Folgerungsschritt ist natürlich entscheidbar und irgendwann hören

wir dann auf. In der Praxis wäre das so eine Art Anytime Prozess, in dem man den deduktiven

Abschluss bildet und der deduktive Abschluss ist natürlich unendlich groß. Es gibt unendlich viele

Formeln, die folgerbar sind aus einer beliebigen, konsistenten Wissensbank. Aus einer inkonsistenten

natürlich noch mehr, da ist alles folgerbar. Das war der Zustand im Wesentlichen beim letzten Mal

und wir haben das angewandt auf die Wumpus-Situation. Wir haben hier die Semantik, das ist wie die Welt

wirklich aussieht. Wir haben hier unsere Wissensbank, wo wir partiell wissen, was passiert ist. Wir haben

also gewisse Felder, in diesem Fall hier drei, exploriert, haben dann gewisses Wissen über die

Welt und die Wissensbank ist letztlich die Aussagen hier.

A für V für das ist, was war V nochmal, wer weiß es? Ne, das ist okay, das ist nämlich wo wir, ach doch ja. Ich weiß es nicht mehr.

Es ist schnitt für schnitt, das weiß ich noch. Das heißt wir wissen partiell, was es über dieses

Ding zu wissen gibt. Wir können das kodieren in Aussagenlogik, das gibt uns eine große Menge an

Formeln und aus dieser Formel können wir dann, in diesem Fall interessiert uns, wo ist der Wumpus,

nämlich in 1, 3, können wir dann ableiten. Wie machen wir das zum Beispiel? Indem wir das ganze

Klausel normalifizieren und dann die negierte Klausel dazu fügen und dann können wir einen

schönen kleinen Resolutionsbeweis machen und am Ende steht tatsächlich die leere Klausel.

Gut, warum ist das nicht alles, was wir wollen? Was wir wollen ist, dass wir die Welt ordentlich

beschreiben, so dass wir effizient Schlüsse ziehen können und in diesem Fall ist es so, dass wir sehr

viele Formeln haben, um eine sehr einfache Welt zu beschreiben. Und da hat man doch das Gefühl,

das geht besser. Also es ist nicht eine sehr schöne Beschreibungssprache und insbesondere ist es nicht

eine Beschreibungssprache, die Sie zum Beispiel verwenden würden, um mir zu erklären, was die

Wumpus-Situation ist. Beziehungsweise wenn Sie versuchen würden, das in Aussagenlogik zu sagen,

dann würde ich sehr schnell meuten. Erstens sagen Sie immer dasselbe, für jede Zelle sagt man

noch mal dasselbe und zweitens ist das ganze so groß, dass ich es mir kaum merken kann. Für

Maschinen mag das eine gute Sache sein, für Menschen ist das sicherlich keine und selbst

für Maschinen ist es nicht klar. In der Logik haben wir immer Sprachen, mit denen wir Welten

beschreiben und die Frage ist immer, ist das die beste Sprache, die ich im Moment benutzen kann und

wir werden uns relativ bald die Prädikatenlogik erster Stufe angucken als eine andere Beschreibungssprache.

Was wir aber vorher, also heute machen wollen, ist dass wir uns einen State of the Art

SAT Solver angucken. SAT Solver als eine Klasse von Programmen, den man eine aussagenlogische Formel

gibt und die dann sagen erfüllbar oder unerfüllbar. Das ist eine wichtige Klasse von Programmen,

die industriell relevant sind, weil man sehr, sehr viele Probleme in Aussagenlogik einfach

transformieren kann, sodass die Bedeutung erhalten bleibt, so wie wir es für den Wumpus gemacht

haben. Das ist der State of the Art in vielen Problemklassen, ist tatsächlich heutzutage

einfach kompilieren in Aussagenlogik einen SAT Solver, darauf anschmeißen und dann das Ergebnis,

also entweder unerfüllbar oder die Belegung zurückrechnen auf die Lösung des ursprünglichen

Problems. Eine interessante Sache ist, dass SAT Solving, diese Programmklasse, ist noch ziemlich

stark in akademischer Hand. Bei vielen Problemen ist es so, dass irgendwann mal die Industrie

davon Wind kriegt und sagt, das ist eine interessante Klasse von Problemen, da können wir Geld verdienen,