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.
Presenters
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