7 - Grundlagen der Logik in der Informatik [ID:4390]
50 von 399 angezeigt

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

Wir haben letztes Mal oder Sie mit Herrn Gotscharow gesprochen über Normalformen,

insbesondere die Negations-Normalform und die konjunktive Normalform. Zur Rekursivendefinition

der konjunktiven Normalform haben wir noch einen Nachtrag.

Dieser Nachtrag besteht darin, dass die Definitionen, die wir oder Herr Gotscharow letztes Mal gegeben

haben, noch keine Definition darstellt, indem sie keinen terminierenden Fall hat. Man muss

ja irgendwann auch mal feststellen, dass die Rekursion zu Ende ist. Das heißt, die vollständige

Definition lautet so. Also hier haben wir die erste Definition für eine Konjunktion.

Wenn ich also eine Konjunktion von zwei Formeln habe, dann kann ich einfach die CNF der beiden

Teilformeln bilden. Das sind jeweils Konjunktionen von Dissjunktionen und wenn ich das über eine

Konjunktion wieder zusammenfüge, habe ich wieder eine Konjunktion von Dissjunktionen. Das heißt,

wenn das rauskommt, ist wieder eine CNF. Wenn ich jetzt einen Fall habe, wo eine Dissjunktion

oben liegt und darunter eine Konjunktion kommt, dann mache ich jetzt nur einen Fall, weil wir

ab jetzt einen globalen Disklemmer einführen. Dissjunktion und Konjunktion gelten jetzt

mal als assoziativ und kommunitativ. Deshalb nehme ich jetzt mal nur den Fall, dass also

die Konjunktion hier auf der linken Seite kommt und wenn sie auf der rechten Seite kommt, dann

drehe ich das einfach um. Da verwenden wir dann das Distributivgesetz. Das heißt, wir

verteilen diese Dissjunktion über diese Konjunktion hier, haben also einmal hier Phi oder Chi und

andererseits Psi oder Chi. Hier bilden wir konjunktive Normalformen, verbinden die wieder

per Konjunktion, bekommen also wieder eine konjunktive Normalform. Warum terminiert das?

Nun, es terminiert deswegen, weil die rekursiven Aufrufe immer mit kleineren Formeln geschehen,

als ich hier reingegangen bin. Das heißt, die Größe der Argumentformel meiner Funktion

wird immer kleiner. Das muss irgendwann terminieren, nur, dass es hier eben bisher, das ist das,

was fehlt, der keinen terminierenden Fall gibt. Die Frage ist also, wann hören wir auf?

Nun, wir hören dann auf, wenn keiner dieser Fälle mehr matcht. Das heißt, wenn wir eine

Dissjunktion in der Hand haben, unter der keine weiteren Konjunktionen kommen. Wie drücken wir das aus?

Nun, wir sagen, die CNF von Phi ist gleich Phi selbst, wenn Phi schon eine CNF ist. So, gut.

Gut, und da muss man sich überlegen, dass das korrekt ist. Das heißt, man muss zeigen,

dass sobald keine dieser Klauseln der Vorderen mehr matcht, dass ich dann in dem letzten Fall bin.

Wenn jetzt keine dieser vorderen Klauseln mehr matcht, dann heißt das, ich habe oben keine Konjunktion.

Gut, ich könnte also oben noch eine Dissjunktion haben. Was passiert dann? Wohlgemerkt, jetzt kommt

noch weiter rein, das, was ich eben sagte, Dissjunktion ist konjunktiv und assoziativ.

Ich könnte natürlich eine Dissjunktion haben, unter der eine weitere Dissjunktion kommt.

Dann würde zunächst mal hier formal nichts matchen. Aber, da ich assoziativ rechne, wenn hier also

unter der obersten Dissjunktion eine weitere Dissjunktion kommt, dann kann ich also diese beiden Dissjunktionen,

die kann ich umklammern, per Assoziativität. Das ist also ein allgemeiner Disclaimer, der da drin steckt.

Und dann wäre, nachdem ich umgeklammert habe, die obersten paar Dissjunktionen, die ich finde,

landen die alle in dem Chi. Und werden dann also gemeinsam die gesamte oben liegende Dissjunktion

über die nächste drunter liegende Konjunktion verteilt. So, wir machen am besten mal ein Beispiel.

So, hier einen einfachen Fall, wo ich hier zwei Dissjunktionen oben liegen habe.

So, meinetwegen so geklammert. Das stelle ich mir zunächst mal vor.

So, wie gesagt, ich gönne mir implizit Assoziativität und Kommutativität.

So, das heißt, ich klammere das um. So, das mache ich alles implizit.

In Wirklichkeit schreibe ich sowieso keine Klammern hin, wenn ich Dissjunktionen schreibe.

Ich lasse die Klammern weg. So, wenn ich das jetzt umgeklammert habe, dann matcht diese Klausel hier.

Also, dann verteile ich also diese Dissjunktion hier, diese beiden Dissjunktionen gemeinsam hier über,

naja, falsch, gemeinsam über diese Konjunktion. Das heißt, einmal kriegt das A die ab, A und A oder diese beiden,

ne, nicht A oder, sondern A und A oder diese beiden hier. So, das ist das eine und CNF von nicht B oder diese beiden hier.

So, und jetzt bin ich im terminierenden Fall und zwar auf beiden Seiten, denn das hier sind jeweils beides schon CNFs, sogar Klauseln.

So, nicht damit haben wir also diese Formel in CNF transformiert.

Zugänglich über

Offener Zugang

Dauer

01:17:27 Min

Aufnahmedatum

2014-11-20

Hochgeladen am

2014-11-20 10:36:30

Sprache

de-DE

Aussagenlogik:

  • Syntax und Semantik
  • Automatisches Schließen: Resolution
  • Formale Deduktion: Korrektheit, Vollständigkeit


Prädikatenlogik erster Stufe:

  • Syntax und Semantik
  • Automatisches Schließen: Unifikation, Resolution
  • Quantorenelimination
  • Anwendung automatischer Beweiser
  • Formale Deduktion: Korrektheit, Vollständigkeit
Einbetten
Wordpress FAU Plugin
iFrame
Teilen