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

So, schon guten Morgen. Es ist immer noch leun. Ich vertrete heute Herr Professor

Schröder, der ist in der Konferenz. Und heute machen wir ein neues Thema.

Okay, das ist wahrscheinlich ein bisschen schwer.

Okay, was wir heute machen heißt...

Normalformen und Resolutionsverfahren. Also, früher haben wir ein bisschen von

natürlicher Schließen gemacht und das ist eine Art von logischer Kalkül, der...

Ja? Nicht anschalten? Ach so, wie denn? Recht? Ach so, okay.

Ja, okay. Also, natürlicher Schließen, wie gesagt, das ist eine Art von logischer

Kalkül, der entspricht zu der Art, die... Also, mehr oder weniger ist es formalisiert

logisches Denken. Da hat man die Regeln, die kann man verstehen und formalisieren

die normalen Beweise, die man in mathematischen Büchen findet. Und deswegen

heißt es natürliches Lesen. Da ist es mehr oder weniger natürliches. Und das ist

natürlich sehr bequem, wenn man einen Beweis selber schreibt. Dann kann man das

wieder lesen und verstehen, übergeben und die anderen Leute lesen das wieder und

auch verstehen, können das auch weiterentwickeln und so weiter.

Manchmal braucht man auch die Formeln automatisch beweisen. Und dafür,

dieser natürliche Schließenverfahren, ist nicht so effektiv. Das kann man auch

ausprogrammieren, aber wenn man das wirklich automatisch machen will, dann

kann man viel besser machen und dafür verwendet man normalerweise andere

Verfahren. Und dieser Resolutionsverfahren oder Resolutionsmethode ist eine andere

Art von Kalkül, wie ein natürliches Lesen, aber es ist mehr computerfreundlich, weil

natürliches Lesen mehr menschfreundlich ist, sozusagen. Ich kann das auch als eine

kleine Tabelle aufschreiben. So wir hatten früher...

und dann hier ist die Resolution.

Okay, das gehört alles zu diesen Teilen. Und wenn man

Effektivität von der Implementation, potenzielle Implementation, irgendwie

einschätzt, dann kann man grob gesagt, grob sagen, dass hier kriegt man mehr oder

weniger Minus, das ist natürlich ganz grob, und hier mehr oder weniger Plus, und

hier ist es Plus und hier ist es Minus. Das ist ganz grobe Einschätzung, natürlich

ist es nicht nicht so deutlich, aber ungefähr ist es so, damit ihr ein großes

Bild bekommt. Und ja, wie gesagt, eine Eigenschaft für natürliches Lesen ist,

dass man die Beweise mehr oder weniger gut versteht und dafür ändert man die

Formel ganz so auffällig. Und wenn man alles ausprogrammieren muss, damit der

automatische Beweis die Formel beweist, dann muss man nicht mehr anpassen, dass

die Formel so bleiben, wie sie ursprünglich waren. Dann die Formel können ganz

stark geändert werden, weil für Computer ist es egal, er versteht die Formel

sowieso nicht. Und für Resolution braucht man als erste Phase für das Verfahren,

die Normalformen finden. Und so eine Normalform hatten wir schon an die

Übungen, das heißt NNF, Negations-Normalform.

Die Übungen wurde jetzt schon ein bisschen unformal angeführt und

besprochen. Und jetzt machen wir das ganz formal. Definition. Also wir sprechen von

Negations-Normalformen von außerigenologischen Formeln. Wir haben eine

außerigenologische Formel Phi als Angabe. Und ja, erst mal sagen wir, dass Phi ist

in NNF.

Genau dann, wenn Phi mit der folgenden Grammatik

definierbar ist.

Okay, ich schreibe ein bisschen anders. Es ist entweder A oder nicht A oder

Phi und Psi oder Phi oder Psi. Und A ist von dieser Atommenge. Ist diese

Definition klar? Also eine Formel in NNF ist entweder ein Atom oder ein negierten