Banner

Fachhochschule Wiesbaden
Fachbereich Informatik

KI


Sven Eric Panitz

Startseite zurück Inhaltsverzeichnis weiter


Kapitel 3 Logik

Hallo Bert. Was schauen sitzen Sie da so melancholisch wie ein Forsthaus im Walde? Ach, wissen Sie, es geht um meinen Freund Ernie. Ich dachte immer, Sie verstehen sich recht gut miteinander. Die Sache ist nur, daß Ernie angefangen hat, Gedichte zu schreiben. Nun, das ist doch ein recht leises und angenehmes Hobby. Nur Ernie hat mir seine Gedichte zum Lesen gegeben und nach meiner Meinung gefragt. Und. Naja, sie sind ziemlich langweilig aber das möchte ich nicht so direkt sagen, schließlich ist er ja mein Freund. Sind die wirklich so schlimm? Ja stellen Sie sich vor, alle seine Gedichte sind über Seifenblasen. Aber das kann doch ganz nett sein. Kann, muß aber nicht. Warten sie:
Oh Seifenblase, Oh Seifenblase,
In dir spiegelt sich ein kleiner Hase
Du leuchtest in allen Farben so bunt
In dir spiegelt sich auch ein kleiner Hund
Oh ja, das ist tatsächlich etwas langweilig. Aber, das muß man ihm ja nicht so direkt sagen. Dann drücken Sie das ihm gegenüber doch etwas verklausuliert aus, etwa so:

  • Wirklich interessante Gedichte sind nicht unbeliebt bei Leuten mit guten Geschmack.
  • Keine moderne Poesie ist frei von einer gewissen Schwülstigkeit.
  • Alle Deine Gedichte sind nun mal über Seifenblasen.
  • Schwülstige Poesie ist nicht beliebt bei Leuten mit einen gewissen Geschmack.
  • Kein älteres Gedicht beschäftigt sich mit Seifenblasen.
Das klingt alles sehr allgemein dahergesagt. Ich glaube, wenn ich Ernie es so sage, würde er nicht eingeschnappt sein. Hoffen wir nur das Ernie nicht zuviel Lewis Carrol liest. Eine der Kernaufgaben eines intelligenten Agenten besteht darin, aus vorhandenen Basiswissen neues Wissen abzuleiten; Charles Lutwidge Dodgson ($\ast$27. Januar 1832 in Daresbury; $\dagger$14. Januar 1898 in Guildford), besser bekannt unter seinem Künstlernamen Lewis Carroll, war ein britischer Schriftsteller, Mathematiker und Fotograf. Er ist der Autor von Alice im Wunderland, Alice hinter den Spiegeln (auch bekannt als Alice im Spiegelland) und Die Jagd nach dem Schnark. Mit seiner Befähigung für Wortspiel, Logik und Fantasie schaffte er es, weite Leserkreise -- von den Naivsten zu den Gebildetsten -- zu fesseln. Seine Werke sind bis heute populär geblieben und haben nicht nur die Kinderliteratur, sondern auch Schriftsteller wie James Joyce oder Douglas R. Hofstadter beeinflusst. \ aus bestehenden Fakten über die Umgebung, weitere Schlüsse zu ziehen oder Pläne zu kreieren. Die Frage, wie der Vorgang des folgerichtigen Schließens genauer präzisiert werden kann, stellte sich schon die alten Griechen. Aristoteles stellte hierzu ein formales System von Schlußregeln auf, die immer zu folgerichtigen Schlüssen führen. Damit begründete Aristoteles die formale Logik. Je nach den technischen Möglichkeiten, interessertierte die Frage, ob sich die formalen Schlußsysteme der Logik, maschinell zum logischen Schließen ausführen lassen. So verwundert es nicht, daß die KI sehr früh die formale Logik als eines der Hauptwerkzeuge anektierte und entscheidend für seine Zwecke weiterentwickelte. Ein Mathematiker, der sich recht unterhaltsam mit logischen Rätsel beschäftigte, war Lewis Carroll, der unzählige von logischen Spielereien und verklausulierten Rätsel aufgestellt hat.

3.1 Aussagenlogik

Das grundlegendste logischen System, von dem komplexere formale Systeme abgeleitet werden können, ist die Aussagenlogik, die einem Programmierer in jeder Programmiersprache als der Datentyp boolean begegnet.George Boole ($\ast$2. November 1815 in Lincoln, England; $\dagger$8. Dezember 1864 in Ballintemple, Irland) war ein englischer Mathematiker (Autodidakt) und Philosoph. Ursprünglich als Lehrer tätig, wurde er auf Grund seiner wissenschaftlichen Arbeiten 1848 Mathematikprofessor am Queens College in Cork (Irland). Boole entwickelte 1847 den ersten algebraischen Logikkalkül für Klassen und Aussagen im modernen Sinn. Damit begründete er die moderne mathematische Logik. Booles Kalkül wird gelegentlich noch im Rahmen der traditionellen Begriffslogik interpretiert, obwohl Boole bereits in The Mathematical Analysis of Logic ausschließlich von Klassen spricht. Boole arbeitete in einem kommutativen Ring mit Multiplikation und Addition, die den logischen Verknüpfungen und und entweder...oder entsprechen; in diesem booleschen Ring gilt zusätzlich zu den bekannten Rechenregeln die Regel aa=a, in Worten (a und a)=a. In der Boole-Schule wurde die zum booleschen Ring gleichwertige boolesche Algebra entwickelt, die mit und und oder arbeitet. Sie ist heute in der Aussagenlogik und Mengenlehre bekannter und verbreiteter als der originale, rechnerisch elegantere boolesche Ring. George Boole ist der Vater von Ethel Lilian Voynich. Auf George Boole sind die booleschen Variablen zurückzuführen, die zu den Grundlagen des Programmierens in der Informatik zählen. \ Wir werden in diesem Kapitel die Aussagenlogik auf unterschiedliche Weise betrachten. Dabei werden viele Aspekte eines formalen Systems exemplarisch vorgeführt. Ein formales System besteht in der Regel aus einer Sprache, in der bestimmtes Wissen ausgedrückt werden kann. Diese Sprache ermöglicht es syntaktische Sätze, oder Formeln aufzuschreiben. Zur Unterscheidung zu anderen Sprachen, insbesondere der Sprache, in der wir über die Formelsprache Beweise führen, bezeichnen wir die Formelsprache als Objektsprache. Wenn Beweise über Eigenschaften der Objektsprache geführt werden, so werden diese Beweise in einer Metasprache geführt. Für eine Objektsprache ist eine Semantik zu definieren. Die Semantik wird in der Regel eine mathematische Definition sein, in der jeder Satz der Objektsprache auf bestimmte Elemente mathematischer Mengen abgebildet wird. Die Semantik kann definieren, welche neuen Formeln aus einer Menge von Formeln folgt. Desweiteren ist für ein formales System ein Kalkül zu definieren. Ein Kalkül besteht aus Rechenregeln. Diese Regeln arbeiten auf den syntaktischen Objekten der Objektsprache und geben an, wie durch symbolisches Rechnen neue Formeln aus einer Menge von Formeln abzuleiten ist. Zwischen einem Kalkül und der Semantik einer Sprache sind zwei fundamentale Eigenschaften zu beweisen. Zum einem soll der Kalkül nur korrekte Ableitungen machen. Jeder Satz, der sich durch die Operationen eines Kalküls aus einer Formelmenge ableiten läßt, soll auch semantisch aus dieser Formelmenge folgern. Ist diese Eigenschaft erfüllt, so ist der Kalkül korrekt. Nun ist es natürlich recht leicht einen korrekten Kalkül für ein beliebiges formales System zu schreiben. Hierzu nehme man einfach den Kalkül, der überhaupt keine Sätze ableiten kann. Ein Kalkül sollte aber möglichst viele Schlußfolgerungen beweisen können, am besten sollte er alles, was semantisch aus einer Formelmenge folgt, aus dieser auch ableiten können. Wenn dieses der Fall ist, so bezeichnet man den Kalkül als vollständig. Abbildung gibt einen schematischen Überblick über die Bestandteile eines formales Systems.\setlength{\unitlength}{0.00087489in} % \begingroup\makeatletter\ifx\SetFigFont\undefined% \gdef\SetFigFont#1#2#3#4#5{% \reset@font\fontsize{#1}{#2pt}% \fontfamily{#3}\fontseries{#4}\fontshape{#5}% \selectfont}% \fi\endgroup% {\renewcommand{\dashlinestretch}{30} \begin{picture}(4075,3502)(0,-10) \drawline(360.000,1219.000)(397.779,1158.325)(437.664,1099.015) (479.608,1041.141)(523.558,984.776)(569.459,929.989) (617.257,876.847)(666.890,825.417)(718.299,775.761) (771.420,727.940)(826.187,682.014)(882.533,638.040) (940.388,596.071)(999.681,556.159)(1060.339,518.354) (1122.287,482.702)(1185.449,449.248)(1249.746,418.031) (1315.100,389.092)(1381.430,362.465)(1448.654,338.183) (1516.688,316.277)(1585.450,296.773)(1654.855,279.696) (1724.816,265.066)(1795.248,252.901)(1866.063,243.218) (1937.175,236.026)(2008.496,231.336)(2079.937,229.153) (2151.411,229.480)(2222.829,232.316)(2294.104,237.659) (2365.147,245.500)(2435.871,255.831)(2506.188,268.639) (2576.013,283.909)(2645.258,301.620)(2713.839,321.752) (2781.671,344.280)(2848.669,369.175)(2914.753,396.408) (2979.839,425.944)(3043.848,457.747)(3106.701,491.778) (3168.320,527.995)(3228.630,566.354)(3287.556,606.806) (3345.025,649.302)(3400.966,693.790)(3455.311,740.215) (3507.992,788.519)(3558.944,838.644)(3608.106,890.526) (3655.415,944.103)(3700.814,999.308)(3744.246,1056.072) (3785.658,1114.327)(3825.000,1174.000) \drawline(3782.875,1057.701)(3825.000,1174.000)(3733.102,1091.207) \drawline(3690.000,1534.000)(3651.262,1594.518)(3610.131,1653.437) (3566.674,1710.661)(3520.960,1766.099)(3473.063,1819.661) (3423.059,1871.263)(3371.029,1920.821)(3317.056,1968.256) (3261.227,2013.491)(3203.631,2056.454)(3144.361,2097.076) (3083.512,2135.293)(3021.181,2171.041)(2957.468,2204.265) (2892.477,2234.911)(2826.310,2262.930)(2759.074,2288.277) (2690.877,2310.911)(2621.828,2330.795)(2552.039,2347.899) (2481.620,2362.194)(2410.686,2373.658)(2339.349,2382.272) (2267.725,2388.022)(2195.927,2390.899)(2124.073,2390.899) (2052.275,2388.022)(1980.651,2382.272)(1909.314,2373.658) (1838.380,2362.194)(1767.961,2347.899)(1698.172,2330.795) (1629.123,2310.911)(1560.926,2288.277)(1493.690,2262.930) (1427.523,2234.911)(1362.532,2204.265)(1298.819,2171.041) (1236.488,2135.293)(1175.639,2097.076)(1116.369,2056.454) (1058.773,2013.491)(1002.944,1968.256)(948.971,1920.821) (896.941,1871.263)(846.937,1819.661)(799.040,1766.099) (753.326,1710.661)(709.869,1653.437)(668.738,1594.518) (630.000,1534.000) \drawline(670.901,1650.735)(630.000,1534.000)(721.023,1617.754) \drawline(2025,3334)(360,1534) \drawline(419.462,1642.463)(360.000,1534.000)(463.508,1601.721) \drawline(2205,3334)(3825,1624) \drawline(3720.692,1690.482)(3825.000,1624.000)(3764.249,1731.747) \put(1845,3379){\makebox(0,0)[lb]{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}Syntax}}} \put(0,1309){\makebox(0,0)[lb]{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}Semantik}}} \put(3645,1399){\makebox(0,0)[lb]{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}Kalkül}}} \put(1755,49){\makebox(0,0)[lb]{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}Vollständigkeit}}} \put(1710,2164){\makebox(0,0)[lb]{{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}Korrektheit}}} \end{picture} } In dieser Weise stellt auch jede Programmiersprache ein formales System dar. Der Kalkül einer Programmiersprache ist ihr Ausführungsmodell. Die Semantik einer Programmiersprache ist in den seltesten Fällen eigens definiert. Daher fällt es auch schwer Korrektheitsbeweise über Programme zu führen. Statt von Semantik und Kalkül spricht man bei Programmiersprachen auch von denotionaler und operationaler Semantik.

3.1.1 Syntax

Die Aussagenlogik ist eine Sprache in der aussagenlogische Formeln ausgedrückt werden können. Informatiker sind es gewohnt Sprachen über einer kontextfreie Grammatik auszudrücken. Wir werden im Folgenden eine eher mathematische Definition der Sprache der aussagenlogischen Formeln benutzen. Wir folgen dabei einem Vorlesungsskript der Universität Karlsruhe. Syntax der Aussagenlogik Die Menge $\{(,),\neg,\rightarrow\}$ sei die Menge der Sondersymbole.
Für eine abzählbare Menge $S=\{A,B,C\dots\}$ von Aussagenlogischen Variablen sei die Sprache $\mbox{For}_S$ definiert als die kleineste Menge mit:

  • $S\subset \mbox{For}_S$
  • wenn $x\in \mbox{For}_S$ dann auch $\neg x \in \mbox{For}_S$
  • wenn $x\in \mbox{For}_S$ und $x\in \mbox{For}_S$ dann auch $(x\rightarrow y)\in \mbox{For}_S$
Die Menge $S$ wird als Signatur bezeichnet. Formeln $x$ mit $x\in S$ werden als Atome bezeichnet. Die Menge $S\cup \{\neg x|x\in S\}$ wird als die Menge der Literale bezeichnet. Wie man sieht, halten wir unsere Sprache extrem klein. Wir verzichten auf die üblichen aussagenlogischen Junktoren für oder und und, $\vee$ und $\wedge$ und begnügen uns mit dem Symbol $\rightarrow$ für die logischen Implikation und $\neg$ für die Negation. $\vee$ und $\wedge$ werden wir lediglich als Abkürzungen für komplexere Ausdrücke benutzen: $\vee$ und $\wedge$ Ein Ausdruck der Form $(A\vee B)$, $A, B\in \mbox{For}_S$ stehe für: $(\neg A\rightarrow B)$.
Ein Ausdruck der Form $(A\wedge B)$, $A, B\in \mbox{For}_S$ stehe für: $\neg(\neg A\vee \neg B)$.
Ein Ausdruck der Form $(A\leftrightarrow B)$, $A, B\in \mbox{For}_S$ stehe für: $( (A\rightarrow B)\wedge(B \rightarrow A))$, Unsere aussagenlogischen Formeln sind mit obiger Definition vollständig geklammert. Wie wir es bei arithmetischen Ausdrücken gewohnt sind, bei denen die Punktrechnungsoperatoren stärker binden als Strichrechnungsoperatoren, und somit Klammern vermieden werden können, sei ein Operatorpriorität auf den aussagenlogischen Operatoren in folgender Reihenfolge gegeben: $\neg, \wedge, \vee, \rightarrow, \leftrightarrow$

3.1.2 Semantik

Wir haben im voherigen Abschnitt eine Sprache definiert. Die Ausdrücke der Sprache $\mbox{For}_S$ hat bisher noch keine Bedeutung für uns. Diese definieren wir nun. Hierzu werden Interpretationen für Ausdrücke der Sprache $\mbox{For}_S$ definiert. Interpretation Eine Abbildung $I: S\rightarrow \{W,F\}$ heißt Interpretation. Eine Interpretation wird auf die folgende Weise zu einer Abbildung $w_I: \mbox{For}_S\rightarrow \{W,F\}$ erweitert: \begin{eqnarray*} w_I(x) &=& I(x)\qquad \textrm{für $x\in S$}\\ w_I(\neg x) &=& \left\{\begin{array}{ll} W& \textrm{für $w_I(x)=F$}\\ F& \textrm{sonst} \end{array}\right.\\ w_I((x\rightarrow y)) &=& \left\{\begin{array}{ll} W& \textrm{für $w_I(y)=W$ oder $w_I(x)=F$}\\ F& \textrm{sonst} \end{array}\right. \end{eqnarray*} Eine Interpretation ist also eine Belegung der aussagenlogischen Variablen einer Formel mit den Werten $W$ und $F$. Für diese Belegung bekommt dann die gesammte Formel einen Wahrheitswert berechnet. Hierzu war es nur notwendig für die beiden Operatoren $\neg$ und $\rightarrow$ zu definieren, wie für sie den Wahrheitswert abhängig von der Teilformel lautet. Es schließen sich ein paar einfache Begriffe an: Sei $A\in\mbox{For}_S$.

  • $A$ ist eine Tautologie (allgemeingültig) gdw. für alle Interpretationen $I$ gilt: $w_I(A)=W$.
  • $A$ ist ein Widerspruch (widersprüchlich, unerfüllbar) gdw. für alle Interpretationen $I$ gilt: $w_I(A) = F$.
  • $A$ ist erfüllbar (konsistent) gdw. es eine Interpretationen $I$ gibt mit: $w_I(A)=W$.
  • ein Modell für eine Formel $A$ ist eine Interpretation $I$ mit $w_I(A) = W$.
In der Aussagenlogik sind wir in der glücklichen Lage, daß wir in einer Formel nur endlich aussagenlogische Variablen haben. Für $n$ aussagenlogische Variablen gibt es $2^n$ verschiedene Interpretationen. Somit können wir in Form von Wahrheitstafel alle Interpretaionen einer Formel hinschreiben und damit prüfen, ob es eine Tautologie ist. Allerdings ist das mit einem exponentiellen Aufwand verbunden.

Aufgabe 3

Zeigen Sie: $w_I((A\vee B)), w_I((A\wedge B)), w_I((A\rightarrow B)), w_I((A\rightarrow B))$ berechnen sich aus $w_I(A)$ und $w_I(B)$ wie folgt:
$w_I(A)$ $w_I(B)$ $w_I((A\vee B))$ $w_I((A\wedge B))$ $w_I((A\leftrightarrow B))$
W W W W W
W F W F F
F W W F F
F F F F W
Bauernregeln:

  • ``Abendrot Schlechtwetterbot'' kann man übersetzen in \\ $\mbox{Abendrot} \impl \mbox{Schlechtes\_Wetter}$. Diese Aussage ist weder Tautologie noch Widerspruch, aber erfüllbar.
  • ``Wenn der Hahn kräht auf dem Mist, ändert sich das Wetter oder es bleibt wie es ist.'' kann man übersetzen in \\ $\mbox{Hahn\_kraeht\_auf\_Mist} \impl (\mbox{Wetteraenderung} \vee \neg \mbox{Wetteraenderung})$. \\ Man sieht, dass das eine Tautologie ist.
Beispiele für ein paar allgemeingültige Formelschemata:

  • $A\wedge A\leftrightarrow A$ (Idemtpotenz)
  • $A\vee A\leftrightarrow A$ (Idemtpotenz)
  • $ (A\wedge B)\wedge C \leftrightarrow A\wedge (B\wedge C)$ (Assoziativität)
  • $ (A\vee B)\vee C \leftrightarrow A\vee (B\vee C)$ (Assoziativität)
  • $A\wedge B \leftrightarrow B\wedge A$ (Kommutativität)
  • $A\vee B \leftrightarrow B\vee A$ (Kommutativität)
  • $A\wedge (B\vee C)\leftrightarrow (A\wedge B)\vee (A\wedge C)$ (Distributivität)
  • $A\vee (B\wedge C)\leftrightarrow (A\vee B)\wedge (A\vee C)$ (Distributivität)
  • $A\wedge(A\vee B)\leftrightarrow A$ (Absorption)
  • $A\vee(A\wedge B)\leftrightarrow A$ (Absorption)
  • $\neg\neg A\leftrightarrow A$ (Doppelnegation)
  • $\neg(A\wedge B)\leftrightarrow \neg A\vee \neg B$ (de Morgan)
  • $\neg(A\vee B)\leftrightarrow \neg A\wedge \neg B$ (de Morgan)
Nachdem wir nun Formeln interpretiert haben, indem sie unter einer Interpretion euf einen der Werte $W$ und $F$ abgebildet werden, benutzen wir diese Interpretionen, um zu definieren, wann aus einer Formelmenge eine weitere Formel semantisch folgt. semantische Folgerbarkeit Sei $M\subset\mbox{For}_S$ und $A\in\mbox{For}_S$. Aus $M$ sei $A$ folgerbar im Zeichen $M\models_S A$ genau dann wenn: für jede Interpretion $I$, für die für jedes $B\in M$ gilt $w_I(B)=W$, gilt auch $w_I(A)=W$. logisch Äquivalent Für $A, B\in\mbox{For}_S$ sei $A$ logisch äquivalent zu $B$ genau dann wenn: $\{A\}\models_S B$ und $\{B\}\models_S A$. Es gilt das kleine praktische Lemma:$A$ ist logisch äquivalent zu $B$ genau dann wenn $\{\}\models A\leftrightarrow B$.

3.1.3 Kalküle

Wie werden zwei Beispiele für Kalküle der Aussagenlogik vorstellen. Zunächst einen Kalkül, der versucht ähnlich wie in Idealfall ein Mathematiker, den formalen Beweis einer Formel mit einer Kette kleiner aufeinanderfolgender Schritte zu führen; und ein zweiter Kalkül, der möglichst gut als einfacher Algorithmus umgesetzt werden kann.

Kalkül des natürlichen Schließens

Christoph Drösser, Die Zeit 27.4.2006 Mathematik, so lautet die gängige Meinung, beruht im Gegensatz zu den Naturwissenschaften nicht auf Erfahrung, sondern auf reiner Logik. Aus einer überschaubaren Menge von Grundannahmen, so genannten Axiomen, finden die Mathematiker durch die Anwendung logischer Schlussregeln zu immer neuen Erkenntnissen, dringen immer tiefer ins Reich der mathematischen Wahrheit vor. Die menschliche Subjektivität (der Geisteswissenschaft) und die schmutzige Realität (der Naturwissenschaft) bleiben außen vor. Es gibt nichts Wahreres als die Mathematik, und vermittelt wird uns diese Wahrheit durch den Beweis. So ein Beweis ist zwar von Menschen gemacht, und es erfordert Inspiration und Kreativität, ihn zu finden, aber wenn er einmal dasteht, ist er unumstößlich. Allenfalls kann er durch einen einfacheren oder eleganteren ersetzt werden. Obiges Zitat aus einem Wochenzeitungsartikel beschreibt, wie im Idealfall ein mathematischer Beweis aussieht. Der Kalkül, der in diesem Abschnitt vorgestellt wird, spiegelt genau diese Idee Beweise zu führen wieder. Daher definieren wir zunächst Axiome, die wir im Kalkül des natürlichen Schließens benutzen wollen: Axiome Die Menge $\cal{A}$ der Axiome über eine Signatur $S$ sei die Vereinigung der folgenden drei Mengen:

  • $A_1=\{(A\rightarrow(B\rightarrow A))|A,B \in \mbox{For}_S\}$
  • $A_2=\{(A\rightarrow(B\rightarrow C))\rightarrow((A\rightarrow B)\rightarrow(A \rightarrow C)))|A,B,C \in \mbox{For}_S\}$
  • $A_3=\{((A\rightarrow B )\rightarrow(\neg A\rightarrow \neg B))|A,B \in \mbox{For}_S\}$
Als kleine Übung läßt sich folgene Behauptung beweisen:Alle Axiome sind Tautologien. Man vergegenwätrige sich noch einmal, daß es nicht drei Axiome gibt, sondern unendlich viele Axiome, die alle nach einem der drei obigen Schemata gebildet sind. Im Kalkül des logischen Schließens wird eine Beweiskette aufgebaut: In dieser Kette dürfen Axiome auftauchen, Formeln des Basiswissens, aus dem neues Wissen abgeleitet werden soll, und über eine bestimmte Schlußregel erhaltene neue Schlüsse. syntaktische Ableitbarkeit Sei $M\subset\mbox{For}_S$ und $A\in\mbox{For}_S$. Aus $M$ sei $A$ ableitbar im Zeichen $M\vdash_S A$ genau dann wenn: es existiert eine Folge $(A_1,\dots, A_n)$ mit $A_i\in\mbox{For}_S$, so daß für jedes $A_i$ gilt:

  • $A_i\in M$
  • oder $A_i\in Ax$
  • oder es existieren $j,k<i$ mit $A_j=(A_k\rightarrow A_i)$
Der letzte Punkt in dieser Definition ist die eigentliche Schlußregel. Sie ist eine der Schlußregeln, die bereits Aristoteles aufgestellt hat, und wir seit der Antike als modus ponens bezeichnet. Sie hat die schematische Form:

\[\frac{A\quad A\rightarrow B}{A}\]

Diese Schreibweise von logischen Schlußregeln ist wie folgt zu lesen: wenn die Formeln oberhalb des Querstriches angenommen werden können, so darf die Formel unterhalb des Querstriches geschlossen werden. Für die erste unserer beiden Bauernregeln kommt der modus ponens zur Anwendung wenn Abendrot beobachtet wird, dann läßt sich aus den Faktum der Beobachtung und der Regel schließen, daß mit schlechten Wetter zu rechnen ist. \[\frac{\mbox{Abendrot}\quad \mbox{Abendrot}\rightarrow \mbox{Schlechtes\_Wetter}} {\mbox{Schlechtes\_Wetter}}\]

Da wir mit Syntax, Semantik und Kalkül alle drei Komponenten eines formalen Systems definiert haben, ist der fundamentale Zusammenhang zwischen diesen noch zu zeigenDer Kalkül des natürlichen Schließens ist korrekt und vollständig. Wir werden diesen Satz in diesem Skript nicht beweisen. Die Korrektheit ist leicht zu zeigen, hingegen die Vollständigkeit benötigt mehrere Seiten Beweis. Jetzt wollen wir aber endlich auch einen Beweis im Kalkül des natürlichen Schließens führen:Versuchen wir einmal eine Ableitung der sehr einfachen Formel $(A\rightarrow A)$ zu finden:\\ Ax1 $(A\rightarrow ((A\rightarrow A) \rightarrow A))$\\ Ax2 $((A\rightarrow ((A\rightarrow A) \rightarrow A)) \rightarrow ((A\rightarrow(A\rightarrow A)) \rightarrow(A\rightarrow A)) )$\\ MP $((A\rightarrow(A\rightarrow A)) \rightarrow(A\rightarrow A))$\\ Ax1 $((A\rightarrow(A\rightarrow A))$\\ MP $(A\rightarrow A)$ Wie man sieht, ist es eine mühsehlige Aufgabe, einen Beweis in diesem Kalkül zu finden. Es ist ein kreativer Anteil notwendig, in dem geschickte Instanziierungen der Axiomenschemata gefunden werden müssen. Algorithmisch ließe sich ein solcher Beweis tatsächlich nur über eine Suche realisieren, in der alle möglichen Ableitungsketten aufgezählt werden, um endlich eine Beweiskette zu finden, der zur zu beweisenden Formel führt.

Der Resolutionskalkül

Der Kalkül des natürlichen Schließens im letzten Abschnitt, war für algorithmische Zwecke und als Grundlage eines automatischen Beweissystems auf aussagenlogischen Formeln denkbar ungeeignet. Daher werden wir jetzt einen Kalkül vorstellen, der sich gut automatisieren läßt. Hierzu werden wir die Formeln zunächst in eine bestimmte Normalform umformen.konjunktive Normalform (CNF), Klauselnormalform Eine Formel, die eine Konjunktion von Disjunktionen von Literalen ist, ist in konjunktive Normalform oder auch Klauselnormalform. D.h. die Formel ist von der Form $$(L_{1,1} \vee \ldots \vee L_{1,n_1}) \wedge \ldots \wedge(L_{m,1} \vee \ldots \vee L_{m,n_m})$$ wobei $L_{i,j}$ Literale sind. Die Klauselnormalform wird oft als Menge von Mengen notiert und auch behandelt. Dies ist gerechtfertigt, da sowohl $\wedge$ als auch $\vee$ assoziativ, kommutativ und idempotent sind, so dass Vertauschungen und ein Weglassen der Klammern erlaubt ist. Wichtig ist die Idempotenz, die z.B. erlaubt, eine Klausel $\{A,B,A,C\}$ als unmittelbar äquivalent zur Klausel $\{A,B,C\}$ zu betrachten. Eine Klausel mit einem Literal bezeichnet man auch als {\em 1-Klausel}. Eine Klausel (in Mengenschreibweise) ohne Literale wird als {\em leere Klausel} bezeichnet. Diese ist äquivalent zu einem Widerspruch. Eine Klausel $C$ ist eine Tautologie genau dann wenn es eine Variable $A$ gibt, so dass sowohl $A$ als auch $\neg A$ in der Klausel vorkommenBeweis: Übungsaufgabe. Jede aussagenlogische Formel läßt sich mit folgendem Algorithmus in eine semantisch äquivalente Formel in Klauselnormalform umformen.

  • ersetze sukzessive Teilformeln der Gestalt $\neg\neg A$ durch $A$, $\neg(A\vee B)$ durch $(\neg A \wedge \neg B)$, $\neg(A\wedge B)$ durch $\neg A\vee \neg B$ bis keine der Umformungen mehr möglich ist.
  • dann ersetze Teilformeln der Gestalt $(A\vee(B\wedge C))$ durch $(A\vee B)\wedge(A\vee C)$ und $((B\wedge C)\vee A)$ durch $(B\vee A)\wedge(C\vee A)$ bis keine der Umformungen mehr möglich ist.

3.1.4 Implementierung

Formel.scala
package name.panitz.ki
case class Atom(name:String) extends Formel{
  override def toString()=name}
case class Not(e1:Formel) extends Formel{
  override def toString()="¬"+e1.toString}
case class Impl(e1:Formel,e2:Formel) extends Formel{
  override def toString()="("+e1.toString+" -> "+e2.toString+")"}
case class And(e1:Formel,e2:Formel) extends Formel{
  override def toString()="("+e1.toString+" /\\ "+e2.toString+")"}
case class Or(e1:Formel,e2:Formel) extends Formel{
  override def toString()="("+e1.toString+" \\/ "+e2.toString+")"}

abstract class Formel{
  def eliminateImpl():Formel={
   this match {
    case Atom(_)  => this
    case Not(x)   => Not(x.eliminateImpl)
    case And(x,y) => And(x.eliminateImpl,y.eliminateImpl)
    case Or(x,y)  => Or(x.eliminateImpl,y.eliminateImpl)
    case Impl(x,y)=> Or(Not(x.eliminateImpl),y.eliminateImpl)
   }
  }

  def negationToInner():Formel={
   this match {
    case Atom(_)       => this
    case Not(Atom(x))  => this
    case Not(Not(x))   => x.negationToInner
    case Not(And(x,y)) => Or(Not(x),Not(y)).negationToInner
    case Not(Or(x,y))  => And(Not(x),Not(y)).negationToInner
    case And(x,y)      => And(x.negationToInner,y.negationToInner)
    case Or(x,y)       => Or(x.negationToInner,y.negationToInner)
   }
  }

  def makeConjunctions():Formel={
   this match {
    case Atom(_)       => this
    case Not(x)        => this
    case Or(And(x,y),z)=> And(Or(x,z),Or(y,z)).makeConjunctions
    case Or(x,And(y,z))=> And(Or(x,y),Or(x,z)).makeConjunctions
    case Or(x,y) 
      => val x1 =x.makeConjunctions
         val y1 =y.makeConjunctions
         x1 match { 
           case And(_,_) => Or(x1,y1).makeConjunctions
           case _        => y1 match {
                           case And(_,_) => Or(x1,y1).makeConjunctions
                           case _        => Or(x1,y1)
	                 }
         }
    case And(x,y)      => And(x.makeConjunctions,y.makeConjunctions)
   }
  }

  def toCNF():Formel=eliminateImpl.negationToInner.makeConjunctions

  import scala.collection.mutable.HashSet
  import scala.collection.mutable.Set
  def conjunctionSet():Set[Formel]={
    val result=new HashSet[Formel]()
    this match {
      case And(e1,e2) => result++= e1.conjunctionSet;
                         result++= e2.conjunctionSet;
      case e => result+= e
    }
    result
  }

  type Klausel=Set[Formel]
  def disjunctionSet():Klausel={
    val result=new HashSet[Formel]()
    this match {
      case Or(e1,e2) => result++= e1.disjunctionSet;
                        result++= e2.disjunctionSet;
      case e => result+= e
    }
    result
  }

  def cnf():List[Klausel]=
    (for (val f<- toCNF.conjunctionSet.elements) 
       yield f.disjunctionSet).toList

  def negated()= this match { case Not(x) => x
                              case y      => Not(y)}

}

Resolution.scala
package name.panitz.ki
object Resolution{
  import scala.collection.mutable.Set
  import scala.collection.mutable.HashSet
  type Klausel=Set[Formel]

  def resolvable(xs:Klausel,ys:Klausel)=
    xs.exists((x)=>ys.exists((y)=>y.negated==x))

  def resolve(xs:Klausel,ys:Klausel)={
    val result=new HashSet[Formel]()
    for (val x<-xs.elements;!ys.exists((y)=>y==x.negated)) result+=x
    for (val y<-ys.elements;!xs.exists((x)=>y==x.negated)) result+=y
    result
  }

  def resolution(xsP:List[Klausel])={    
    var xs=xsP
    var zs=xsP
    while (!zs.isEmpty && !zs.exists((x)=>x.size==0)){
      val ks=
       for (val x<-xs;val y<-zs;resolvable(x,y)) yield resolve(x,y)
       
      zs=ks.toList
      xs= xs ::: zs
    }
    xs
  }

  def proof(a:Formel):List[Set[Formel]]=proof(List(),a)
  def proof(ms:List[Formel],a:Formel):List[Set[Formel]]={
    var clauses=List[Set[Formel]]()      
    for (val m<-ms) clauses = m.cnf ::: clauses
    clauses = Not(a).cnf ::: clauses
    resolution(clauses)
  }
}

TestFormel.scala
package name.panitz.ki
object TestFormel extends Application{
  val ax1:Formel = Impl(Atom("A"),Impl(Atom("B"),Atom("A")))
  Console println ax1
  Console println ax1.toCNF
  Console println Resolution.proof(ax1) 

  val ax2=Impl(Impl(Atom("A"),Impl(Atom("B"),Atom("C")))
              ,Impl(Impl(Atom("A"),Atom("B")),Impl(Atom("A"),Atom("C"))))
  Console println ax2
  Console println ax2.toCNF
  Console println Resolution.proof(ax2) 


  val ax3=Impl(Impl(Atom("A"),Atom("B")),Impl(Not(Atom("B")),Not(Atom("A"))))
  Console println ax3
  Console println ax3.toCNF
  Console println Resolution.proof(ax3) 
}