kapitel 3: aussagenlogik - hu-berlin.dekossahl/uni/thi1/vorlesung/kap3.pdfkapitel 3: aussagenlogik...
TRANSCRIPT
Kapitel 3: Aussagenlogik
§ 3.1 Grundbegriffe§ 3.2 Anwendung: Data Mining§ 3.3 Erfullbarkeit§ 3.4 Folgerungen und formale Argumente§ 3.5 Anwendung: Planungsprobleme in der
kunstlichen Intelligenz§ 3.6 Anwendung: Schaltkreisverifikation§ 3.7 Aquivalenz§ 3.8 Boolesche Algebra§ 3.9 Die Adaquatheit der Junktoren§ 3.10 Normalformen§ 3.11 Anwendung: Schaltkreisentwurf
123
§ 3.1 Grundbegriffe
124
Aussagen
Die Frage ”Was ist eigentlich ein Wort?“ ist analog der ”Was ist eineSchachfigur?“ Ludwig Wittgenstein, Philosophische Untersuchungen
I Aussagen (im Sinne der Aussagenlogik) sind sprachlicheGebilde, die entweder wahr oder falsch sind.
I Aussagen konnen mit Junktoren wie nicht, und, oder oder wenn. . . dann zu komplexeren Aussagen verknupft werden.
I Aussagenlogik beschaftigt sich mit allgemeinen Prinzipien deskorrekten Argumentierens und Schließens mit Aussagen undKombinationen von Aussagen.
125
Ludwig Wittgenstein (1889 – 1951)
126
Beispiele
Aussagen sind etwaI α: Die Sonne scheint.I β: Die Vorlesung ist langweilig.I γ: Die Vorlesung ist unverstandlich.
Diese “atomaren” Aussagen konnen wir mit Hilfe von Junktoren zuneuen Aussagen verknupfen, etwa:
I β und γDie Vorlesung ist langweilig und unverstandlich.
I Wenn nicht α dann γWenn die Sonne nicht scheint, dann ist die Vorlesungunverstandlich.
127
Syntax der Aussagenlogik
Definition 3.1 (Variablen)Eine Aussagenvariable, oder einfach Variable, hat die Form Vi , furi ∈ N. Die Menge aller Variablen bezeichnen wir mit AVAR.
Definition 3.2 (Alphabet)Das Alphabet der Aussagenlogik ist
AAL := AVAR ∪{111,000,¬,∧,∨,→,↔, (, )}.
128
Definition 3.3 (Sprache der Aussagenlogik)Die Menge AL der (aussagenlogischen) Formeln ist rekursiv wie folgtdefiniert:
Basisregeln:I 000 und 111 sind Formeln.I Jede Variable ist eine Formel.
000, 111 und die Variablen bezeichnen wir als atomare Formeln oderAtome.
Rekursive Regeln:I Wenn ϕ eine Formel ist, dann ist auch ¬ϕ eine Formel.I Wenn ϕ,ψ Formeln sind, dann sind auch (ϕ∧ψ), (ϕ∨ψ),
(ϕ → ψ), (ϕ ↔ ψ) Formeln.¬,∧,∨,→,↔ heißen Junktoren.
129
Syntaxbaume
Die Struktur einer Formel lasst sich bequem in einem Syntaxbaum(oder Ableitungsbaum, auf Englisch parse tree) darstellen.Fur die Formel (((V0 ∧ 111) ∨ V2) ↔ (V0 ∧ ¬V1)) sieht der Syntaxbaumwie folgt aus:
↔
∨
∧
V0 111
V2
∧
V0 ¬
V1
130
ASCII-Syntax fur die Aussagenlogik
Alternativ zur ”abstrakten“ Syntax der Aussagenlogik uber demAlphabet AAL konnen wir auch eine ”konkrete“ computerlesbareSyntax uber dem ASCII-Alphabet angeben.
Definition 3.4Die Menge AVAR ⊆ ASCII∗ sei definiert durch:
AVAR := {Vn | n ∈ NAT}
(wobei NAT wie in Kapitel 2 definiert ist).
131
Definition 3.5Die Menge AL ⊆ ASCII∗ sei rekursiv wie folgt definiert:
Basisregeln:I 0,1 ∈ AL,I Fur alle X ∈ AVAR: X ∈ AL.
Rekursive Regeln:I Wenn ϕ ∈ AL, dann !ϕ ∈ AL.I Wenn ϕ,ψ ∈ AL, dann (ϕ/\ψ), (ϕ\/ψ),(ϕ->ψ), (ϕ<->ψ) ∈ AL.
Bemerkung 3.6Es ist offensichtlich, wie man Formeln von der abstrakten in dieASCII-Syntax ubersetzt und umgekehrt. Wir werden im Folgendennur mit der abstrakten Syntax arbeiten.Um aber etwa die Algorithmen, die wir in der Vorlesung kennenlernenwerden, zu implementieren, kann man die obige ASCII-Syntaxverwenden.
132
Subformeln
Definition 3.7Die Menge sub(ϕ) der Subformeln einer Formel ϕ ist rekursiv wiefolgt definiert:
I Fur atomare Formeln ϕ ist sub(ϕ) := {ϕ}.I Ist ϕ = ¬ψ, so ist sub(ϕ) := {ϕ} ∪ sub(ψ)
I Fur alle ∗ ∈ {∧,∨,→,↔}:Ist ϕ = (ψ1 ∗ψ2), so ist
sub(ϕ) := {ϕ} ∪ sub(ψ1) ∪ sub(ψ2).
Bemerkung 3.8Formal ist also
sub : AL → ℘(AL).
133
Beispiel 3.1
Sei ϕ = (((V0 ∧ 111) ∨ V2) ↔ (V0 ∧ ¬V1)).Dann ist
sub(ϕ) ={(((V0 ∧ 111) ∨ V2) ↔ (V0 ∧ ¬V1)),
((V0 ∧ 111) ∨ V2),
(V0 ∧ ¬V1),
(V0 ∧ 111),
V2,
V0,
¬V1,
111,
V1}
134
Rekursive Definitionen uber Formeln
Eine Funktion f : AL → M, fur eine beliebige Menge M, lasst sich wiefolgt definieren:Rekursionsanfang:
I Definiere f (111) und f (000).I Definiere f (X ) fur alle X ∈ AVAR.
Rekursionsschritt:I Definiere f (¬ϕ) aus f (ϕ).I Fur ∗ ∈ {∧,∨,→,↔}, definiere f (ϕ ∗ψ) aus f (ϕ) und f (ψ).
135
Notation
I Statt V0,V1,V2 . . . bezeichnen wir Variablen auch mit X ,Y ,Z , . . .oder Varianten wie X ′,Y1.
I Wir schreiben∧n
i=1ϕi oder (ϕ1 ∧ . . .∧ϕn) statt(· · · ((ϕ1 ∧ϕ2) ∧ϕ3) ∧ . . .∧ϕn).Analog fur ∨.
I Die außeren Klammern einer Formel lassen wir normalerweiseweg. Also (X ∧ Y ) → Z statt ((X ∧ Y ) → Z ).
I Bezuglich Klammerung verwenden wir folgende Bindungsregeln:1. ¬ bindet starker als alle anderen Junktoren.2. ∧ und ∨ binden starker als → und ↔.
Wir konnen also X ∧ ¬Y → Z ∨ X schreiben, aber nichtX ∧ Y ∨ Z .
136
Wahrheitsbelegungen
Definition 3.9Die Variablenmenge einer Formel ϕ ist die Menge
var(ϕ) := AVAR ∩ sub(ϕ).
Definition 3.101. Eine Wahrheitsbelegung (oder einfach Belegung) ist eine
partielle Funktion B von AVAR nach {0,1}.2. Eine Belegung B ist eine Belegung fur eine Formel ϕ, oder
passend zu ϕ, wenn var(ϕ) ⊆ def(B).
Intuitive Bedeutung1 steht fur wahr, 0 steht fur falsch.
137
Semantik der Aussagenlogik
Definition 3.11Rekursiv uber den Aufbau von AL definieren wir eine Funktion J · K·,die jeder Formel ϕ ∈ AL und jeder Belegung B fur ϕ einen WertJϕKB ∈ {0,1} zuordnet:Rekursionsanfang:
I J000KB:= 0, J111KB
:= 1I Fur alle X ∈ VAR: JX KB
:= B(X ).
Rekursionsschritt: Fur nichtatomare ϕ sei JϕKB durch folgendeVerknupfungstafeln definiert:
JϕKB J¬ϕKB
0 11 0
(Fortsetzung auf der nachsten Folie)
138
JϕKB JψKB Jϕ∧ψKB
0 0 00 1 01 0 01 1 1
JϕKB JψKB Jϕ∨ψKB
0 0 00 1 11 0 11 1 1
JϕKB JψKB Jϕ → ψKB
0 0 10 1 11 0 01 1 1
JϕKB JψKB Jϕ ↔ ψKB
0 0 10 1 01 0 01 1 1
139
Intuitive Bedeutung der SemantikAtome
111 und 000 bedeuten einfach “wahr“ und ”falsch“.Die Variablen stehen fur irgendwelche Aussagen. Unsinteressiert aber nur, ob diese wahr oder falsch sind.Das wird durch die Belegung angegeben.
Negation¬ϕ wahr ⇐⇒ ϕ falsch.¬ϕ bedeutet also ”nicht ϕ“.
Konjunktionϕ∧ψ wahr ⇐⇒ ϕ wahr und ψ wahr.ϕ∧ψ bedeutet also ”ϕ und ψ“.
Disjunktionϕ∨ψ bedeutet ”ϕ oder ψ“.
Implikationϕ → ψ bedeutet ”ϕ impliziert ψ“ (oder ”wenn ϕ dannψ“).
Biimplikationϕ ↔ ψ bedeutet ”ϕ genau dann wenn ψ“.
140
Andere Junktoren
Die Auswahl der Junktoren ¬,∧,∨,→,↔ fur ”unsere“aussagenlogische Sprache richtet sich nach demumgangssprachlichen Gebrauch und den Erfordernissen desformalen Schließens, ist aber in gewisser Weise willkurlich.Durch Festlegung ihrer Verknupfungstafel konnen wir auch andereJunktoren definieren (und damit andere aussagenlogischeSprachen).
141
Beispiele
Exklusives Oder: Der 2-stellige Junktor ⊕ sei definiert durch
JϕKB JψKB Jϕ⊕ψKB
0 0 00 1 11 0 11 1 0
Intuitiv bedeutet ϕ⊕ψ ”Entweder ϕ oder ψ“. Man nennt ⊕ auchexklusives Oder.
142
Mehrheitsjunktor: Der 3-stellige Junktor M sei definiert durch
JϕKB JψKB JχKB JM(ϕ,ψ, χ)KB
0 0 0 00 0 1 00 1 0 01 0 0 00 1 1 11 0 1 11 1 0 11 1 1 1
Intuitiv ist M(ϕ,ψ, χ) also dann wahr, wenn mindestens zwei(also die Mehrheit) der Formeln ϕ,ψ, χ wahr sind. Man nennt Mden (3-stelligen) Mehrheitsjunktor.
AchtungDie Junktoren ⊕ und M sind nicht Teil unserer aussagenlogischenSprache und durfen deswegen in Formeln auch nicht verwendetwerden.
143
Formalisierung umgangssprachlicher Aussagen
Beispiel 3.12
”Wenn es regnet und kalt ist, gehe ich nicht spazieren.“
Atomare Aussagen:I XR : Es regnet.I XK : Es ist kalt.I XS: Ich gehe spazieren.
Obige Aussage ist dann
XR ∧ XK → ¬XS.
144
Beispiel 3.13
”Das Fluchtauto war rot oder grun und hatte weder vornenoch hinten ein Nummernschild“
Atomare Aussagen:I XR : Das Fluchtauto war rot.I XG: Das Fluchtauto war grun.I XV : Das Fluchtauto hatte vorne ein Nummernschild.I XH : Das Fluchtauto hatte hinten ein Nummernschild.
Obige Aussage ist dann
(XR ∨ XG) ∧ (¬XV ∧ ¬XH).
145
Beispiel 3.14
”Alle Menschen sind sterblich. Sokrates ist ein Mensch. Alsoist Sokrates sterblich.“
Nicht unmittelbar aussagenlogisch. Trotzdem ist eineaussagenlogische Formalisierung nutzlich, die eine
”Individuenvariable“ x verwendet.Atomare Aussagen:
I XM : x ist ein MenschI X†: x ist sterblich.I XS: x ist Sokrates.
Dann ergibt sich
(XM → X†) ∧ (XS → XM) → (XS → X†).
Diese Formalisierung vernachlassigt allerdings den Aspekt, dass dieobige Aussage fur alle x gelten soll.
146
Beispiel 3.15
”Jede Primzahl großer als zwei ist ungerade.“
Atomare Aussagen:I XP : x ist Primzahl.I X>2: x ist großer als 2.I XU : x ist ungerade
Dann ergibt sich(XP ∧ X>2) → XU .
147
Wahrheitstafeln
Fur jede Formel ϕ kann man die Werte unter allen moglichenBelegungen in einer Wahrheitstafel darstellen. Fur jede BelegungB : var(ϕ) → {0,1} hat die Tafel eine Zeile, die die Werte B(X ), furX ∈ var(ϕ), und den Wert JϕKB enthalt.
Beispiel 3.16Sei ϕ = V0 ∨ V1 → V0 ∧ V2. Die Wahrheitstafel fur ϕ ist
V0 V1 V2 V0 ∨ V1 → V0 ∧ V20 0 0 10 0 1 10 1 0 00 1 1 01 0 0 01 0 1 11 1 0 01 1 1 1
148
Um die Wahrheitstafel fur ϕ zu berechnen, ist es bequem, auchSpalten fur alle Subformeln von ϕ einzufugen. In unserem Beispielsieht die so erweiterte Wahrheitstafel wie folgt aus:
V0 V1 V2 V0 ∨ V1 V0 ∧ V2 V0 ∨ V1 → V0 ∧ V20 0 0 0 0 10 0 1 0 0 10 1 0 1 0 00 1 1 1 0 01 0 0 1 0 01 0 1 1 1 11 1 0 1 0 01 1 1 1 1 1
149
Bemerkung 3.17Fur eine Formel ϕ ohne Variablen besteht die Wahrheitstafel nur auseiner einzigen Spalte (weil ϕ keine Variablen enthalt) und, neben derKopfzeile, einer einzigen Zeile (weil es genau eine BelegungB : ∅ → {0,1} gibt – die leere Menge) und hat damit genau einenEintrag (den ”Wert“ der Formel). Die erweiterte Wahrheitstafel hateine Zeile, die die Werte aller Subformeln der Formel enthalt.
Beispiel 3.18Sei ϕ = (111 → 000) → 000. Die Wahrheitstafel von ϕ ist
(111 → 000) → 0001
Die erweiterte Wahrheitstafel ist
111 000 111 → 000 (111 → 000) → 0001 0 0 1
150
Das Koinzidenzlemma
Beim Arbeiten mit Wahrheitstafeln setzen wir stillschweigend voraus,dass der Wert JϕKB einer Formel ϕ unter einer Belegung B nur vonden Werten B(X ) fur die Variablen X ∈ var(ϕ) abhangt.Die Rechtfertigung dafur liefert folgendes Koinzidenzlemma.
Lemma 3.19Seien ϕ eine Formel und B eine Belegung fur ϕ. Dann gilt fur dieRestriktion B|var(ϕ) von B auf var(ϕ):
JϕKB= JϕKB|var(ϕ) .
Intuitiv ist das Lemma ”offensichtlich“, denn in der Definition von JϕKB
werden ja nur die Variablen von ϕ verwendet.Formal kann man es per Induktion uber den Aufbau von AL beweisen.
151
Ein Ratsel
Auf der Insel Wafa leben zwei Stamme: Die Was, die immer dieWahrheit sagen, und die Fas, die immer lugen. Ein Reisenderbesucht die Insel und trifft auf drei Einwohner A, B, C, die ihmfolgendes sagen:
I A sagt: ”B und C sagen genau dann die Wahrheit, wenn C dieWahrheit sagt.“
I B sagt: ”Wenn A und C die Wahrheit sagen, dann ist es nicht derFall, daß A die Wahrheit sagt, wenn B und C die Wahrheitsagen.“
I C sagt: ”B lugt genau dann, wenn A oder B die Wahrheit sagen.“Welchem der beiden Stamme gehoren A, B und C an?
152
Formalisierung
Atomare Aussagen:I XA: A sagt die Wahrheit.I XB: B sagt die Wahrheit.I XC : C sagt die Wahrheit.
Kombinierte Aussagen:I ϕA := XA ↔ ((XB ∧ XC) ↔ XC)
I ϕB := XB ↔ ((XA ∧ XC) → ¬((XB ∧ XC) → XA))
I ϕC := XC ↔ (¬XB ↔ (XA ∨ XB))
Wir suchen nach Belegungen fur XA,XB,XC , die ϕA, ϕB und ϕC wahrmachen.
153
Losung mit Wahrheitstafel
XA XB XC ϕA ϕB ϕC
0 0 0 0 0 10 0 1 1 0 00 1 0 0 1 10 1 1 0 1 01 0 0 1 0 01 0 1 0 1 11 1 0 1 1 11 1 1 1 0 0
Die Belegung XA 7→ 1, XB 7→ 1, XC 7→ 0 in Zeile 7 ist die einzige, dieϕA, ϕB und ϕC wahr macht. Also mussen XA und XB wahr sein undXC falsch, das heißt, A und B sind Was und C ist ein Fa.
154
§ 3.2 Anwendung: Data Mining
155
ProblemstellungEine sehr große Datenmenge soll analysiert werden, um in denDaten verborgene Regelmaßigkeiten zu erkennen.Ganz verschiedene Arten von Regelmaßigkeiten sind denkbar:
1. Qualitative Zusammenhange, die sich etwa durch so genannteAssoziationsregeln (Implikationen von Eigenschaften derDatensatze) beschreiben lassen.Beispiel: Wenn es regnet, tragen die Leute Jacken mit Kapuzenoder Regenschirme.
2. Quantitative Zusammenhange.Beispiel: Wenn die Blute (einer Blume) mehr als 10g wiegt, dannhat der Stiel eine Durchmesser von mindestens 3mm.
3. Clustering, d.h., das Zusammenfassen von Datensatzen zuGruppen einander ahnlicher Datensatze.Beispiel: Es gibt (unter den in den Daten erfassten Viren)mehrere große Gruppen, die jeweils ahnlich Krankheitsbilderverursachen.
Wir betrachten im Folgenden ein aussagenlogisches Modell, in demsich qualitative Regelmaßigkeiten beschreiben lassen.
156
Beispiel: Supermarktdaten
SzenarioDie vollstandigen Kassendaten aller Kassen in den Supermarkteneiner großen Kette sind in einer Datenbank erfasst.Die Datensatze fur unser Datamining-Problem sind die Einkaufslistender Kunden.
ZielDas Aufspuren von Regelmaßigkeiten im Einkausverhalten, um etwadie Anordnung der Produkte in den Regalen zu optimieren.Beispiel: Kunden, die Windeln und Chips kaufen, kaufen auch Bier.
157
Aussagenlogische ModellierungI Fur jedes Produkt fuhren wir eine Aussagenvariable ein.I Die Datensatze lassen sich dann als Belegungen fur die
Variablen beschreiben.I Assoziationsregeln lassen sich als aussagenlogische Formeln
der Gestalt ϕ → ψ beschreiben.
Beispiel 3.20Produkte: Milch, Windeln, Bier, Chips, GummibarchenVariablen: XM , XW , XB, XC , XGDaten:
XM XW XB XC XGKunde 1 0 0 1 0 1Kunde 2 0 1 1 0 1Kunde 3 0 1 1 1 1Kunde 4 0 0 1 1 1Kunde 5 0 1 1 1 0Kunde 6 1 1 1 1 0Kunde 7 0 1 0 1 1Kunde 8 0 0 1 1 1
Regeln:
ρ1 := XW ∧ XC → XB
ρ2 := ¬XB → XG
ρ3 := ¬(XM ∧ XB)
158
Bewertung von AssoziationsregelnZwei wichtige KriterienRegel ρ := ϕ → ψ.Abdeckung:
Zahl der Datensatze, in denen ϕ giltGesamtzahl der Datensatze
.
Genauigkeit:Zahl der Datensatze, in denen ψ giltZahl der Datensatze, in denen ϕ gilt
(falls Abdeckung > 0).
Beispiel 3.20 (Fortsetzung)
Abdeckung Genauigkeitρ1 50% 75%ρ2 12,5% 100%ρ3 100% 87,5%.
159
Bemerkungen
I Das aussagenlogische Modell hat den Vorteil, dass es sehreinfach ist und deswegen auch effizient algorithmisch bearbeitetwerden kann.
I Komplexere qualitative Zusammenhange und quantitatitveZusammenhange konnen darin allerdings nur sehr umstandlichoder gar nicht beschrieben werden.
160
§ 3.3 Erfullbarkeit
161
Erfullbarkeit
Definition 3.21Sei ϕ eine Formel.
1. Eine Belegung B erfullt ϕ (oder ist Modell von ϕ, wir schreibenB|=ϕ), wenn B passend zu ϕ ist und JϕKB
= 1.2. ϕ ist erfullbar, wenn es eine Belegung gibt, die ϕ erfullt. Sonst istϕ unerfullbar.
3. ϕ ist allgemeingultig (oder eine Tautologie), wenn jede zu ϕpassende Belegung ϕ erfullt.
162
Beobachtung 3.22Sei ϕ eine Formel
1. ϕ ist genau dann erfullbar, wenn in der letzten Spalte derWahrheitstafel von ϕ mindestens eine Eins steht.
2. ϕ ist genau dann unerfullbar, wenn in der letzten Spalte derWahrheitstafel von ϕ nur Nullen stehen.
3. ϕ ist genau dann allgemeingultig, wenn in der letzten Spalte derWahrheitstafel von ϕ nur Einsen stehen.
Korollar 3.23Fur alle Formeln ϕ gilt:
ϕ ist allgemeingultig ⇐⇒ ¬ϕ ist unerfullbar.
163
Das Wahrheitstafelverfahren
Eingabe: Formel ϕ.Ziel: Entscheide ob ϕ erfullbar ist.
Verfahren:
1. Berechne die Wahrheitstafel von ϕ.2. Prufe, ob in der letzten Spalte eine Eins steht.
Wenn ja, dann ist ϕ erfullbar, sonst nicht.
Bemerkung 3.24Um zu testen, ob ϕ allgemeingultig ist, pruft man, ob in der letztenSpalte der Wahrheitstafel nur Einsen stehen.
164
Die Ineffizienz des Wahrheitstafelverfahrens
Außer fur Formeln mit sehr wenigen Variablen ist dasWahrheitstafelverfahrens extrem ineffizient, weil eine Formel mit nVariablen eine Wahrheitstafel mit 2n Zeilen hat. Folgende Tabellezeigt die Anzahl der Zeilen der Wahrheitstafel in Abhangigkeit von derVariablenzahl:
Variablen Zeilen10 1.024 ≈ 103
20 1.048.576 ≈ 106
30 1.073.741.824 ≈ 109
40 1.099.511.627.776 ≈ 1012
50 1.125.899.906.842.624 ≈ 1015
60 1.152.921.504.606.846.976 ≈ 1018
165
Erfullbarkeit von Formelmengen
Definition 3.25Sei Φ eine Menge von Formeln.
1. Eine Belegung B ist passend zu Φ, wenn B passend zu allenϕ ∈ Φ ist.
2. Eine Belegung B erfullt Φ (oder ist Modell von Φ, wir schreibenB |= Φ), wenn B passend zu Φ ist und B |= ϕ fur alle ϕ ∈ Φ.
3. Φ ist erfullbar, wenn es eine Belegung gibt, die Φ erfullt. Sonstist Φ unerfullbar.
166
§ 3.4 Folgerungen und formale Argumente
167
Folgerungen
Definition 3.26Seien Φ eine Formelmenge und ψ eine Formel. ψ folgt aus Φ, wennfur jede zu Φ und ψ passende Belegung B gilt:
B |= Φ =⇒ B |= ψ.
Satz 3.27Sei Φ eine Formelmenge und ψ eine Formel. Dann folgt ψ genaudann aus Φ, wenn Φ ∪ {¬ψ} unerfullbar ist.
168
Satz 3.28Sei Φ = {ϕ1, . . . , ϕn} eine endliche Formelmenge und ψ eine Formel.Dann folgt ψ genau dann aus Φ, wenn
ϕ1 ∧ . . .∧ϕn → ψ
allgemeingultig ist.
169
Formale Argumente
Definition 3.29Ein formales Argument, oder eine Ableitungsregel, besteht aus einerReihe von Hypothesen, oder Voraussetzungen, ϕ1, . . . , ϕn und einerFolgerung ψ. Das Argument ist korrekt, wenn ψ aus ϕ1, . . . , ϕn folgt.
Bemerkung 3.30Um zu uberprufen, ob das Argument korrekt ist, konnen wir mittelsder Wahrheitstafelmethode testen, ob ϕ1 ∧ . . .∧ϕn → ψ
allgemeingultig ist.
NotationEine formales Argument mit Hypothesen ϕ1, . . . , ϕn und Folgerung ψschreiben wir oft in der Form
ϕ1 ϕ2 · · · ϕn
ψoder
ϕ1...ϕn
ψ
170
Beispiel
Wenn ThI-1 Vorlesung ist, dann schlafe ich. Abends schlafeich nie. Also ist abends keine ThI-1 Vorlesung.
FormalisierungAussagen:
X: Es ist ThI-1 Vorlesung.Y : Ich schlafe.Z : Es ist Abend.
Das Argument:
Hypothese 1: X → YHypothese 2: Z → ¬Y
Folgerung: Z → ¬X
171
Korrektheitsbeweis mit Wahrheitstafel
X Y Z X → Y ¬Y Z → ¬Y (X → Y )∧(Z → ¬Y )
¬X Z → ¬X(X → Y )
∧(Z → ¬Y )→(Z → ¬X )0 0 0 1 1 1 1 1 1 10 0 1 1 1 1 1 1 1 10 1 0 1 0 1 1 1 1 10 1 1 1 0 0 0 1 1 11 0 0 0 1 1 0 0 1 11 0 1 0 1 1 0 0 0 11 1 0 1 0 1 1 0 1 11 1 1 1 0 0 0 0 0 1
172
Chrisippus JagdhundAls er ein Kaninchen jagte, kam der Hund an eine Kreuzung.Er schnuffelte am Weg links und fand keinenKaninchengeruch. Dann schnuffelte er am Weg geradeausund fand keinen Kaninchengeruch. Daraufhin rannte er,ohne dort zu schnuffeln, nach rechts.
FormalisierungAussagen:
X: Das Kaninchen ist links abgebogen.Y : Das Kaninchen ist geradeaus gelaufen.Z : Das Kaninchen ist rechts abgebogen.
Das Argument:
Hypothese 1: X ∨ Y ∨ ZHypothese 2: ¬XHypothese 3: ¬Y
Folgerung: Z
173
Syllogismen
”Alle Menschen sind sterblich. Sokrates ist ein Mensch. Alsoist Sokrates sterblich.“
FormalisierungAussagen:
I X : x ist ein MenschI Y : x ist sterblich.I Z : x ist Sokrates.
Das Argument:
Hypothese 1: (X → Y )Hypothese 2: (Z → X )
Folgerung: (Z → Y )
174
§ 3.5 Anwendung: Planungsprobleme inder kunstlichen Intelligenz
175
Allgemeines Problem
ProblemWir wollen aufgrund unseres Wissens uber eine gewisse Situation
”richtige“ Entscheidungen uber unser weiteres Vorgehen treffen.
MethodeWir formalisieren das Problem und unser Wissen daruber in derAussagenlogik. Dann versuchen wir, aus unserem bisherigen Wissendie fur unsere Entscheidung notwendige Information zu folgern.Dieses Folgerungsproblem konnen wir als Erfullbarkeitsproblem fureine gewisse Formel formulieren.
WerkzeugEin Programm zur Losung des Erfullbarkeitsproblems.
Wir illustrieren das Verfahren anhand des Minesweeper Spiels.176
Erinnerung: Minesweeper
Regeln:I Anfangs sind alle Felder verdeckt. Einige der Felder enthalten eine
Mine, alle anderen sind leer.I Durch Anklicken mit der linken Maustaste kann man ein Feld
aufdecken.2
Klickt man auf eine Mine, so hat man verloren.Klickt man auf ein leeres Feld, so wird die Anzahl der Minen aufbenachbarten Feldern angezeigt.
I Ziel des Spiels ist es, alle Felder aufzudecken, die keine Mine enthalten.
2Außerdem kann man ein Feld durch anklicken mit der rechten Maustaste mit einemFahnchen markieren.
177
FormalisierungSeien m und n die Zahl der Zeilen bzw. Spalten des gesamtenSpielfeldes. Sei
A := {1, . . . ,m}× {1, . . . ,n}.
Jedes einzelne Feld hat damit Koordinaten (i , j) ∈ A.Fur ein Feld (i , j) ∈ A definieren wir die Menge der Nachbarn von (i , j)wie folgt:
N((i , j)) := A ∩ {(i − 1, j), (i − 1, j + 1), (i , j + 1), (i + 1, j + 1), (i + 1, j),(i + 1, j − 1), (i , j − 1), (i − 1, j − 1)}.
Fur alle q ∈ A fuhren wir 10 Aussagenvariablen ein:
X •q ,X
0q ,X
1q , . . . ,X
8q .
Intuitive BedeutungI X •
q : “Feld q ist vermint.”I X s
q : “Feld q hat s verminte Nachbarfelder.”
(Fortsetzung auf der nachsten Folie)178
Wir definieren eine Formelmenge Φ, die die Regeln des Spielsformalisiert. Φ besteht aus folgenden Formeln:
I Fur alle q ∈ A,
α(q) :=
8∨s=0
X sq .
I Fur alle q ∈ A und 0 ≤ s < t ≤ 8,
β(q, s, t) := ¬(X sq ∧ X t
q).
I Fur alle q ∈ A und R ⊆ N(q),
γ(q,R) :=∧r∈R
X •r → X |R|
q ∨ X |R|+1q ∨ . . .∨ X 8
q
I Fur alle q ∈ A und 1 ≤ s ≤ 8,
δ(q, s) := X sq → ∨
R⊆N(q)|R|=s
∧r∈R
X •r .
(Fortsetzung auf der nachsten Folie)179
Zusatzlich zu den Regeln haben wir zu jedem Zeitpunkt noch Wissenuber die aktuelle Spielsituation, das wir durch eine Formelmenge Ψbeschreiben.Anfangs ist Ψ = ∅.
Beispiel 3.31Wir klicken im ersten Zug auf (3,2); die Zahl 3 wird aufgedeckt. Dannwissen wir ¬X •
(3,2) und X 3(3,2).
Daruber hinaus wissen wir (im Prinzip) auch noch alles, was ausΦ ∪ {¬X •
(3,2),X3(3,2)} folgt, etwa
∨R⊆N((3,2))
|R|=3
∧r∈R X •
r .
Um den nachsten Zug zu finden, konnen wir fur alle q, die noch nichtaufgedeckt sind, prufen, ob ¬X •
q aus Φ ∪ Ψ folgt. Wenn wir ein qfinden, fur das das der Fall ist, so konnen wir gefahrlos im nachstenZug auf q klicken.
AufgabeFinde effiziente Methoden, um Folgerungen aus Formelmengen zuziehen.
180
§ 3.6 Anwendung: Schaltkreisverifikation
181
Digitale Schaltkreise
I Digitale Signale, beschrieben durch 0 (“aus”) und 1 (“ein”).I Schaltelemente berechnen ein oder mehrere Ausgangsignale
aus einem oder mehreren Eingangssignalen.Das Ein-/Ausgabeverhalten eines Schaltelements laßt sich durchWahrheitstafeln beschreiben.
I Schaltkreise sind Kombinationen solcher Schaltelemente.
182
Beispiel
Schaltelement
E1 E2 A1 A20 0 1 00 1 1 01 0 1 01 1 0 1
Schaltkreis
E1 E2 A1 A2 A3 A40 0 1 0 0 00 1 0 1 0 01 0 1 0 1 01 1 0 1 0 1
183
Formalisierung in der Aussagenlogik
SchaltelementI Fur jeden Ein- und Ausgang eine Variable.I Fur jeden Ausgang eine Formel, die den Wert der
Ausgangsvariablen in Abhangigkeit von den Eingangsvariablenbeschreibt.
SchaltkreisI Fur jeden Ein- und Ausgang eine Variable sowie ein Sortiment
Variablen fur jedes Schaltelement.I Formeln fur die Schaltelemente und Formeln fur die
”Verdrahtung“.
184
Beispiel
Schaltelement
Variablen: X1,X2,Y1,Y2
Formeln:Y1 ↔ ¬(X1 ∧ X2)
Y2 ↔ (X1 ∧ X2)
185
Beispiel (cont.)
Schaltkreis
Variablen:X1,X2,Y1,Y2,Y3,Y4,X u
1 ,Xu2 ,Y
u1 ,Y
u2 ,
X m1 ,X
m2 ,Y
m1 ,Y
m2 ,
X o1 ,X
o2 ,Y
o1 ,Y
o2 .
Formeln:Y u
1 ↔ ¬(X u1 ∧ X u
2 ), Y u2 ↔ (X u
1 ∧ X u2 ),
Y m1 ↔ ¬(X m
1 ∧X m2 ), Y m
2 ↔ (X m1 ∧X m
2 ),Y o
1 ↔ ¬(X o1 ∧ X o
2 ), Y o2 ↔ (X o
1 ∧ X o2 ),
X u1 ↔ X1, X u
2 ↔ X2,X m
1 ↔ X1, X m2 ↔ Y u
1 ,X o
1 ↔ X2, X o2 ↔ Y m
1 ,Y1 ↔ Y o
1 , Y2 ↔ Y o2 , Y3 ↔ Y m
2 , Y4 ↔Y u
2 .
186
Verifikation
ZielNachweis, dass der Schaltkreis eine gewisse Korrektheitsbedingungerfullt.
Methode
1. Beschreibe den Schaltkreis durch eine Menge Φ von Formeln.2. Formuliere die Korrektheitsbedingung als Formel ϕ.3. Weise nach, dass ϕ aus Φ folgt.
Bemerkung 3.32Die Korrektheitsbedingung kann insbesondere das gewunschteEin-/Ausgabeverhalten des Schaltkreises vollstandig spezifizieren.
187
Beispiel
Schaltkreis
Einige KorrektheitsbedingungenI Bei jeder Eingabe ist mindestens eine Ausgabe 1.
Y1 ∨ Y2 ∨ Y3 ∨ Y4.
I Bei keiner Eingabe sind zwei Ausgaben 1.
¬“(Y1 ∧ Y2) ∨ (Y1 ∧ Y3) ∨ . . .∨ (Y3 ∧ Y4)
”.
188
Beispiel (cont.)
Vollstandige Spezifikation des Ein-/Ausgabeverhaltens`¬X1 ∧ ¬X2 → Y1 ∧ ¬Y2 ∧ ¬Y3 ∧ ¬Y4
´∧
`¬X1 ∧ X2 → ¬Y1 ∧ Y2 ∧ ¬Y3 ∧ ¬Y4
´∧
`X1 ∧ ¬X2 → Y1 ∧ ¬Y2 ∧ Y3 ∧ ¬Y4
´∧
`X1 ∧ X2 → ¬Y1 ∧ Y2 ∧ ¬Y3 ∧ Y4
´
189
Schaltkreisentwurf durch schrittweiseVerfeinerung
Oft entwirft man zunachst eine “Rohversion” eines Schaltkreises undverbessert diese dann in mehreren Schritten.
ProblemEin bestehender Schaltkreis S1 mit korrektem Ein-/Ausgabeverhaltensoll durch einen neuen Schaltkreis S2 ersetzt werden. Wir wollennachweisen, dass S2 dasselbe Ein-/Ausgabeverhalten hat wie S1.
LosungsverfahrenI Beschreibe das Verhalten von S1 und S2 durch FormelmengenΦ1 und Φ2 (mit disjunkten Variablenmengen). Fur j = 1,2 seienX j
1, . . . ,Xjm bzw. Y j
1, . . . ,Yjn die Variablen, die die Ein- bzw.
Ausgange von Sj beschreiben.I Weise nach, dass aus Φ1 ∪Φ2 folgt:
m∧i=1
(X 1i ↔ X 2
i ) → n∧i=1
(Y 1i ↔ Y 2
i ).
190
§ 3.7 Aquivalenz
191
Aquivalenz
Definition 3.33Zwei Formeln ϕ und ψ sind aquivalent (wir schreiben ϕ ≡ ψ), wennfur alle Belegungen B fur ϕ und ψ gilt:
B |= ϕ ⇐⇒ B |= ψ.
Beobachtung 3.34
1. Fur alle Formeln ϕ,ψ gilt:
ϕ ≡ ψ ⇐⇒ ϕ ↔ ψ ist allgemeingultig
2. Fur alle Formeln ϕ gilt
ϕ ist allgemeingultig ⇐⇒ ϕ ≡ 111.
192
Korollar 3.35Um festzustellen, ob zwei Formeln ϕ,ψ aquivalent sind, kann mandie Wahrheitstafel fur ϕ ↔ ψ berechnen und nachsehen, ob in derletzten Spalte nur Einsen stehen.
Beispiel 3.36Fur alle X ,Y ∈ AVAR gilt:
(X → Y ) ≡(¬X ∨ Y )
(X ↔ Y ) ≡(X → Y ) ∧ (Y → X ).
193
Fragen
1. Kann man aus (X → Y ) ≡ (¬X ∨ Y ) fur alle X ,Y ∈ AVARschließen, dass
(ϕ → ψ) ≡ (¬ϕ∨ψ)
fur alle Formeln ϕ,ψ ∈ AL ?
2. Kann man aus
(X → Y ) ≡(¬X ∨ Y )
(X ↔ Y ) ≡(X → Y ) ∧ (Y → X ).
schließen, dass
(X ↔ Y ) ≡ (¬X ∨ Y ) ∧ (¬Y ∨ X ) ?
194
Das Substitutionslemma (intuitiv)
Lemma 3.37Ersetzt man in einer Aquivalenz uberall die Variablen X1, . . . ,Xndurch Formeln ψ1, . . . , ψn, so bleibt die Aquivalenz erhalten.
Korollar 3.38Fur alle Formeln ϕ,ψ gilt:
ϕ → ψ ≡ ¬ϕ∨ψ.
195
Substitutionen
Definition 3.39Eine Substitution ist eine partielle Abbildung S von AVAR nach AL mitendlichem Definitionsbereich.
196
Die Anwendung von SubstitutionenFur eine Formel ϕ ∈ AL und eine Substitution S bezeichnet ϕS dieFormel, die aus ϕ entsteht, indem man fur alle X ∈ def(S) jedes X inϕ durch die Formel S(X ) ersetzt. Formal definieren wir:
Definition 3.40Fur jede Formel ϕ ∈ AL und jede Substitution definieren wir eineFormel ϕS ∈ AL rekursiv uber den Aufbau von AL:Rekursionsanfang:
I 000S := 000, 111S := 111
I Fur X ∈ AVAR sei XS :=
{S(X ) falls X ∈ def(S),
X sonst.
Rekursionsschritt:I Fur alle ϕ ∈ AL sei
(¬ϕ)S := ¬ϕS.
I Fur ∗ ∈ {∧,∨,→,↔} und ϕ,ψ ∈ AL sei
(ϕ ∗ψ)S := (ϕS ∗ψS) .
197
Beispiel
Sei ϕ := V1 ∧ V2 → V1 ∨ V3, und sei die Substitution
S : {V1,V2} → AL
definiert durch:X V1 V2
S(X ) V2 V0 ∨ V1.
Dann gilt:
ϕS = (V1 ∧ V2)S → (V1 ∨ V3)S= V1S ∧ V2S → V1S ∨ V3S= V2 ∧ (V0 ∨ V1) → V2 ∨ V3.
198
Das Substitutionslemma (formal)
Lemma 3.41Seien S eine Substitution und ϕ,ϕ ′ ∈ AL. Dann gilt
ϕ ≡ ϕ ′ =⇒ ϕS ≡ ϕ ′S.
199
Induktionsprinzip fur aussagenlogischeFormeln
Fur jede Formel ϕ sei A(ϕ) eine Aussage.
Es gelte:Induktionsanfang:
I A(111), A(000)
I Fur alle X ∈ AVAR: A(X ).
Induktionsschritt:I Fur alle Formeln ϕ: Wenn A(ϕ), dann A(¬ϕ).I Fur alle ∗ ∈ {∧,∨,→,↔} und alle Formeln ϕ,ψ:
Wenn A(ϕ) und A(ψ), dann A(ϕ ∗ψ).
Dann gilt A(ϕ) fur alle Formeln ϕ.
200
Induktionsbeweise uber den Aufbauvon Formeln
Fur jede Formel ϕ sei A(ϕ) eine Aussage.
BehauptungA(ϕ) gilt fur alle Formeln ϕ.
Beweis durch Induktion uber den Aufbau von ϕ:
Induktionsanfang:I Beweise A(111) und A(000).I Beweise A(X ) fur X ∈ AVAR.
201
Induktionsschritt:I Negation: Beweise A(¬ϕ) unter Verwendung der
Induktionsannahme (IA) A(ϕ).I Konjunktion: Beweise A(ϕ1 ∧ϕ2) unter Verwendung der
Induktionsannahme A(ϕ1) und A(ϕ2).I Disjunktion: Beweise A(ϕ1 ∨ϕ2) unter Verwendung der
Induktionsannahme A(ϕ1) und A(ϕ2).I Implikation: Beweise A(ϕ1 → ϕ2) unter Verwendung der
Induktionsannahme A(ϕ1) und A(ϕ2).I Biimplikation: Beweise A(ϕ1 ↔ ϕ2) unter Verwendung der
Induktionsannahme A(ϕ1) und A(ϕ2).
202
Bemerkungen
I Oft lassen sich die Schritte fur die zweistelligen Junktoren zueinem einzigen Schritt zusammenfassen:
Fur ∗ ∈ {∧,∨,→,↔}, beweise A(ϕ1 ∗ϕ2) unter Verwendung derInduktionsannahmen A(ϕ1) und A(ϕ2).
I Gelegentlich beweisen wir eine Aussage nur fur Formeln, indenen nur bestimmte Junktoren (etwa ¬,∧,∨) vorkommen.Dann konnen wir im Induktionsbeweis naturlich die Schritte furalle anderen Junktoren weglassen.
203
Beweis des Substitutionslemmas
Eine Belegung ist passend zu S, wenn sie passend zu allen Formeln S(X )
fur X ∈ def(S) ist. Fur jede zu S passende Belegung B sei BS diefolgendermaßen definierte Belegung
BS(X ) :=
{JS(X )KB falls X ∈ def(S),
B(X ) falls X ∈ def(B) \ def(S).
LemmaFur jede Formel ϕ und jede Belegung B, die passend zu ϕ und S ist, gilt:
B |= ϕS ⇐⇒ BS |= ϕ.
Beweis: Wir zeigen die Behauptung des Lemmas durch Induktion uber denAufbau von ϕ:
Induktionsanfang:I Fur ϕ ∈ {000,111} ∪ AVAR \ def(S) gilt ϕS = ϕ und JϕKBS = JϕKB.I Fur ϕ = X ∈ def(S) gilt ϕS = S(ϕ) und JϕKBS = JS(ϕ)KB. Also
BS |= ϕ ⇐⇒ B |= ϕS.
204
Beweis des Substitutionslemmas (cont.)
Induktionsschritt:
I Negation:
B |= (¬ϕ)S ⇐⇒ B |= ¬ (ϕS)⇐⇒ B 6|= ϕS⇐⇒(IA)
BS 6|= ϕ
⇐⇒ BS |= ¬ϕ.
I Konjunktion:
B |= (ϕ∧ψ)S ⇐⇒ B |= (ϕS ∧ψS)⇐⇒ B |= ϕS und B |= ψS⇐⇒(IA)
BS |= ϕ und BS |= ψ
⇐⇒ BS |= ϕ∧ψ.
205
Beweis des Substitutionslemmas (cont.)
I Disjunktion, Implikation, und Biimplikation analog zur Konjunktionunter Verwendung der Semantik des jeweiligen Junktors.
Damit ist das Lemma bewiesen.
Der Beweis des Substitutionslemmas laßt sich jetzt leicht zu Ende fuhren.Seien ϕ,ϕ ′ zwei aquivalente Formeln. Wir wollen zeigen, dass ϕS ≡ ϕ ′S,dass also fur jede passende Belegung B gilt:
B |= ϕS ⇐⇒ B |= ϕ′S.
Sei also B eine zu ϕS und ϕ ′S passende Belegung. Wegen desKoinzidenzlemmas konnen wir annehmen, dass B sogar zu ϕ, S, und ϕ ′
passend ist. Dann gilt:
B |= ϕS ⇐⇒Lemma
BS |= ϕ
⇐⇒ϕ≡ϕ ′
BS |= ϕ′
⇐⇒Lemma
B |= ϕ′S.
Damit ist das Substitutionslemma bewiesen.206
Das Ersetzungslemma (intuitiv)
Lemma 3.42Ersetzt man in einer Formel ϕ eine Subformel ψ durch eine zu ψaquivalente Formel, so erhalt man eine zu ϕ aquivalente Formel.
Korollar 3.43Fur alle Formeln ϕ,ψ gilt:
ϕ ↔ ψ ≡ (¬ϕ∨ψ) ∧ (¬ψ∨ϕ).
Korollar 3.44Jede Formel ist aquivalent zu einer Formel, in der nur die Junktoren¬,∧,∨ vorkommen.
207
Das Ersetzungslemma (formal)
DefinitionSeien ψ,ψ ′ Formeln. Rekursiv definieren wir fur jede Formel ϕ eine Mengeersψ ψ ′(ϕ) von Ersetzungsinstanzen von ψ durch ψ ′ in ϕ:
I Fur atomare ϕ sei
ersψ ψ ′(ϕ) :=
{{ψ ′} falls ϕ = ψ,
∅ sonst.
I Fur ϕ ∈ AL sei
ersψ ψ ′(¬ϕ) :=
{{ψ ′} falls ¬ϕ = ψ,
{¬ϕ ′ | ϕ ′ ∈ ersψ ψ ′(ϕ)} sonst.
208
Das Ersetzungslemma (formal) (cont.)
I Fur ∗ ∈ {∧,∨,→,↔} und ϕ1, ϕ2 ∈ AL sei
ersψ ψ ′(ϕ1∗ϕ2) :=
{ψ ′} falls ϕ1 ∗ϕ2 = ψ,
{ϕ1 ∗ϕ ′2 | ϕ ′
2 ∈ ersψ ψ ′(ϕ2)}
∪ {ϕ ′1 ∗ϕ2 | ϕ ′
1 ∈ ersψ ψ ′(ϕ1)}
sonst.
BeispielSeien ψ := (X1 → X2), ψ ′ := ¬X3, und ϕ := ((X1 → X2) ∨ X3) ∧ ¬(X1 → X2).
Dann ist
ersψ ψ ′(ϕ) = { (¬X3 ∨ X3) ∧ ¬(X1 → X2),
((X1 → X2) ∨ X3) ∧ ¬¬X3}
209
Das Ersetzungslemma (formal) (cont.)
ErsetzungslemmaSeien ϕ,ψ,ψ ′ Formeln mit ψ ≡ ψ ′. Dann gilt fur alle ϕ ′ ∈ ersψ ψ ′(ϕ):
ϕ ≡ ϕ ′.
Beweis: Durch Induktion uber den Aufbau beweisen wir fur alle Formeln ϕ:
S(ϕ): Fur alle ϕ ′ ∈ ersψ ψ ′(ϕ) gilt ϕ ′ ≡ ϕ.
Induktionsanfang:I Behauptung: S(ϕ) fur alle atomaren ϕ.
Beweis:
1. Fall: ϕ = ψ.Dann ist ersψ ψ ′(ϕ) := {ψ ′}, und S(ϕ) gilt, da ϕ = ψ ≡ ψ ′.
2. Fall: ψ 6= ϕ.Dann ist ersψ ψ ′(ϕ) := ∅ und S(ϕ) gilt trivialerweise.
210
Das Ersetzungslemma (formal) (cont.)
Induktionsschritt:I Negation
Induktionsannahme: S(ϕ)
Behauptung: S(¬ϕ)
Beweis:
1. Fall: ¬ϕ = ψ. Wie im atomaren Fall.2. Fall: ¬ϕ 6= ψ.
Sei ϕ ′′ ∈ ersψ ψ ′(¬ϕ). Dann ist ϕ ′′ = ¬ϕ ′ fur einϕ ′ ∈ ersψ ψ ′(ϕ). Nach (IA) gilt ϕ ′ ≡ ϕ. Fur jede BelegungB gilt also B |= ϕ ⇐⇒ B |= ϕ ′ und damit
B |= ϕ′′ ⇐⇒ B |= ¬ϕ
′ ⇐⇒ B |= ¬ϕ
(weil J¬ϕKB nur von JϕKB abhangt). Also ist ϕ ′′ ≡ ¬ϕ.
211
Das Ersetzungslemma (formal) (cont.)
I Sei ∗ ∈ {∧,∨,→,↔}.
Induktionsannahme: S(ϕ1),S(ϕ2)
Behauptung: S(ϕ1 ∗ϕ2)
Beweis:
1. Fall: ϕ1 ∗ϕ2 = ψ. Wie im atomaren Fall.2. Fall: ϕ1 ∗ϕ2 6= ψ.
Sei ϕ ′ ∈ ersψ ψ ′(ϕ1 ∗ϕ2). Dann gilt ϕ ′ = ϕ ′1 ∗ϕ ′
2 fur einϕ ′
1 ∈ ersψ ψ ′(ϕ1) ∪ {ϕ1} und ein ϕ ′2 ∈ ersψ ψ ′(ϕ2) ∪ {ϕ2}.
Nach (IA) gilt ϕ ′1 ≡ ϕ1 und ϕ ′
2 ≡ ϕ2. Damit gilt fur jedeBelegung B
B |= ϕ′ ⇐⇒ B |= ϕ
′1 ∗ϕ ′
2 ⇐⇒ B |= ϕ1 ∗ϕ2.
(weil Jϕ1 ∗ϕ2KB nur von Jϕ1KB und Jϕ2KB abhangt). Also istϕ ′ ≡ ϕ1 ∗ϕ2.
212
§ 3.8 Boolesche Algebra
213
George Boole (1815 – 1864)
214
Fundamentale AquivalenzenSatz 3.45Fur alle Formeln ϕ,ψ, χ gelten die folgenden Aquivalenzen:
1. Idempotenzϕ∧ϕ ≡ ϕ, ϕ∨ϕ ≡ ϕ.
2. Kommutativitat
ϕ∧ψ ≡ ψ∧ϕ, ϕ∨ψ ≡ ψ∨ϕ.
3. Assoziativitat
(ϕ∧ψ) ∧ χ ≡ ϕ∧ (ψ∧ χ), (ϕ∨ψ) ∨ χ ≡ ϕ∨ (ψ∨ χ).
4. Absorption
ϕ∧ (ϕ∨ψ) ≡ ϕ, ϕ∨ (ϕ∧ψ) ≡ ϕ.
5. Distributivitat
ϕ∧(ψ∨χ) ≡ (ϕ∧ψ)∨(ϕ∧χ), ϕ∨(ψ∧χ) ≡ (ϕ∨ψ)∧(ϕ∨χ).
(Fortsetzung nachste Folie) 215
6. Doppelte Negation¬¬ϕ ≡ ϕ.
7. De Morgansche Regeln
¬(ϕ∧ψ) ≡ ¬ϕ∨ ¬ψ, ¬(ϕ∨ψ) ≡ ¬ϕ∧ ¬ψ.
8. Tertium Non Datur
ϕ∧ ¬ϕ ≡ 000, ϕ∨ ¬ϕ ≡ 111.
9.
ϕ∧ 111 ≡ ϕ, ϕ∨ 000 ≡ ϕ,ϕ∧ 000 ≡ 000, ϕ∨ 111 ≡ 111.
10.111 ≡ ¬000, 000 ≡ ¬111.
(Fortsetzung nachste Folie)
216
11. Elimination der Implikation
ϕ → ψ ≡ ¬ϕ∨ψ.
12. Elimination der Biimplikation
ϕ ↔ ψ ≡ (ϕ → ψ) ∧ (ψ → ϕ).
217
Das Dualitatsprinzip
Definition 3.461. Sei ϕ eine Formel, in der keine Implikationen und
Biimplikationen vorkommen. Die zu ϕ duale Formel ist dieFormel ϕ, die aus ϕ entsteht, indem man uberall 111 durch 000, 000durch 111, ∧ durch ∨ und ∨ durch ∧ ersetzt.
2. Sei B eine Belegung. Die zu B duale Belegung ist die BelegungB mit def(B) := def(B) und
B(X ) := 1 − B(X ) fur alle X ∈ def(B).
Beobachtung 3.47In Satz 3.45 stehen auf der linken Seite jeweils die dualen Formeln zudenen auf der rechten Seite.
218
Satz 3.48Fur alle Formeln ϕ, in denen keine Implikationen und Biimplikationenvorkommen, und alle Belegungen B fur ϕ gilt:
JϕKB= 1 − JϕK
eB.
Korollar 3.49Fur alle Formeln ϕ,ψ, in denen keine Implikationen undBiimplikationen vorkommen, gilt:
ϕ ≡ ψ ⇐⇒ ϕ ≡ ψ.
219
Beweis des Dualitatssatzes
Induktion uber den Aufbau von ϕ.Induktionsanfang:
I Behauptung:re111zB
= 1 − J111KeB und
re000zB
= 1 − J000KeB.
Beweis: Es gilt e111 = 000 und e000 = 111. Damitre111zB
= J000KB = 0 = 1 − J111KeB,
re000zB
= J111KB = 1 = 1 − J000KeB.
I Behauptung:reXzB
= 1 − JXKeB fur alle X ∈ AVAR.
Beweis: Fur X ∈ AVAR ist eX = X . Damit giltreXzB
= B(X ) = 1 − eB(X ) = 1 − JXKeB.
Induktionsschritt:I Negation
Induktionsannahme: JeϕKB = 1 − JϕKeB
220
Beweis des Dualitatssatzes (cont.)
Behauptung: Jg¬ϕKB= 1 − J¬ϕK
eB.Beweis: Es gilt g¬ϕ = ¬eϕ. Damit
Jg¬ϕKB= J¬eϕKB = 1 − JeϕKB =
(IA)1 − (1 − JϕK
eB) = 1 − J¬ϕKeB.
I Konjunktion
Induktionsannahme: JeϕKB = 1 − JϕKeB und
reψzB
= 1 − JψKeB
Behauptung:rϕ∧ψ
zB
= 1 − Jϕ∧ψKeB.
Beweis: Es gilt ϕ∧ψ = eϕ∨ eψ. Den Beweis liefert folgendeWahrheitstafel; die beiden letzten Spalten beruhen auf der IA.
JeϕKBreψzB reϕ∨ eψzB
Jϕ∧ψKeB JϕK
eB JψKeB
0 0 0 1 1 10 1 1 0 1 01 0 1 0 0 11 1 1 0 0 0
221
Beweis des Dualitatssatzes (cont.)
I Disjunktion
Induktionsannahme: JeϕKB = 1 − JϕKeB und
reψzB
= 1 − JψKeB
Behauptung:rϕ∨ψ
zB
= 1 − Jϕ∨ψKeB.
Beweis: Es gilt ϕ∨ψ = eϕ∧ eψ. Den Beweis liefert folgendeWahrheitstafel:
JeϕKBreψzB reϕ∧ eψzB
Jϕ∨ψKeB JϕK
eB JψKeB
0 0 0 1 1 10 1 0 1 1 01 0 0 1 0 11 1 1 0 0 0
222
Anwendung in der Mengenlehre
Die Mengengleichungen der Satze 2.10 und 2.12 entsprechen imWesentlichen den Aquivalenzen in Satz 3.45. Tatsachlich kann man dieSatze 2.10 und 2.12 leicht mit Hilfe von Satz 3.45 beweisen, wie folgendesBeispiel illustriert:Beweis von Satz 2.10(5).
Behauptung: Fur alle Mengen M,N,P gilt
M ∩ (N ∪ P) = (M ∩ N) ∪ (M ∩ P).
Beweis: Seien M,N,P MengenSei zunachst m ∈ M ∩ (N ∪ P), wir zeigen m ∈ (M ∩ N) ∪ (M ∩ P).Seien XM ,XN ,XP Aussagenvariablen und B die Belegung mit
B(XQ) :=
{1 falls m ∈ Q0 sonst
(fur Q ∈ {M,N,P}).
223
Anwendung in der Mengenlehre (cont.)
Dann gilt
m ∈ M ∩ (N ∪ P) ⇐⇒ B |= XM ∧ (XN ∨ XP)⇐⇒Satz 3.45(5)
B |= (XM ∧ XN) ∨ (XM ∧ XP)
⇐⇒ m ∈ (M ∩ N) ∪ (M ∩ P)
Dieselbe Aquivalenzkette ruckwarts gelesen zeigt, daß fur allem ∈ (M ∩ N) ∪ (M ∩ P) auch m ∈ M ∩ (N ∪ P) gilt.
Ahnlich folgt auch das Dualitatsprinzip der Mengenlehre (Satz 2.11) ausKorollar 3.49.
224
Das algebraische Verfahren
Eingabe: Formeln ϕ und ψ.Ziel: Entscheide, ob ϕ ≡ ψ.
Verfahren:
1. Wiederhole folgende Schritte:2. Sei ϕ ′ eine Formel, die aus ϕ ensteht, indem
man eine der Aquivalenzen in (1)–(12) auf ei-ne Subformel von ϕ anwendet.
3. Falls ϕ ′ = ψ, so halte an mit der Antwort:“ϕ ≡ ψ”.
Sonst setze ϕ := ϕ ′.
Bemerkung 3.50Um mit dem algebraischen Verfahren zu testen, ob eine Formel ϕallgemeingultig (bzw. unerfullbar) ist, testet man, ob ϕ ≡ 111(bzw. ϕ ≡ 000).
225
Beispiele
1. Die Formeln ¬(¬ϕ∨ ¬ψ) und ϕ∧ψ sind aquivalent:
¬(¬ϕ∨ ¬ψ) ≡ ¬¬ϕ∧ ¬¬ψ (Satz 3.45(7))
≡ ϕ∧ ¬¬ψ (Satz 3.45(6))
≡ ϕ∧ψ (Satz 3.45(6)).
2. Die Formeln
(X1 → (X2 → ((X3 ∨ X4) ∧ ¬X5))) ∨ (X1 → X2)
und 111 sind aquivalent(d.h., die Formel (X1 → (X2 → ((X3 ∨ X4) ∧ ¬X5))) ∨ (X1 → X2) istallgemeingultig):
(X1 → (X2 → ((X3 ∨ X4) ∧ ¬X5))) ∨ (X1 → X2)
≡ (X1 → (X2 → ((X3 ∨ X4) ∧ ¬X5))) ∨ (¬X1 ∨ X2) (Satz 3.45(11))
226
Beispiele (cont.)
≡ (X1 → (¬X2 ∨ ((X3 ∨ X4) ∧ ¬X5))) ∨ (¬X1 ∨ X2) (Satz 3.45(11))
≡ (¬X1 ∨ (¬X2 ∨ ((X3 ∨ X4) ∧ ¬X5))) ∨ (¬X1 ∨ X2) (Satz 3.45(11))
≡ ¬X1 ∨ ((¬X2 ∨ ((X3 ∨ X4) ∧ ¬X5)) ∨ (¬X1 ∨ X2)) (Satz 3.45(3))
≡ ¬X1 ∨ ((¬X1 ∨ X2) ∨ (¬X2 ∨ ((X3 ∨ X4) ∧ ¬X5))) (Satz 3.45(2))
≡ ¬X1 ∨ (¬X1 ∨ (X2 ∨ (¬X2 ∨ ((X3 ∨ X4) ∧ ¬X5)))) (Satz 3.45(3))
≡ ¬X1 ∨ (¬X1 ∨ ((X2 ∨ ¬X2) ∨ ((X3 ∨ X4) ∧ ¬X5))) (Satz 3.45(3))
≡ ¬X1 ∨ (¬X1 ∨ (111 ∨ ((X3 ∨ X4) ∧ ¬X5))) (Satz 3.45(8))
≡ ¬X1 ∨ (¬X1 ∨ (((X3 ∨ X4) ∧ ¬X5)) ∨ 111) (Satz 3.45(2))
≡ ¬X1 ∨ (¬X1 ∨ 111) (Satz 3.45(9))
≡ ¬X1 ∨ 111 (Satz 3.45(9))
≡ 111 (Satz 3.45(9)).
227
Bemerkungen
I Wenn die beiden Eingabeformeln nicht aquivalent sind, halt dasalgebraische Verfahren niemals an.Ein solches Verfahren, daß nur im Falle einer positiven Antworttatsachlich antwortet, nennt man einSemi-Entscheidungsverfahren.
I Selbst wenn die Eingabeformeln aquivalent sind, halt dasVerfahren nicht unbedingt an. Zum Beispiel kann es passieren,dass die Regeln ”zirkular“ angewendet werden.
I Selbst wenn die Eingabeformeln aquivalent sind und alle Regeln
”optimal“ angewendet werden, ist es nicht klar, ob das Verfahrenimmer halt. Denn wir wissen (noch) nicht, ob zwei aquivalenteFormeln auch tatsachlich immer durch die Umformungen(1)–(12) ineinander uberfuhrt werden konnen.
228
Vollstandigkeit des algebraischen Verfahrens
Satz 3.51Seien ϕ,ϕ ′ aquivalente Formeln. Dann gibt es ein n ≥ 1 undFormeln ϕ1 := ϕ,ϕ2, . . . , ϕn := ϕ ′, so dass fur 1 ≤ i ≤ n − 1 gilt:
ϕi+1 entsteht aus ϕi , indem man eine der Aquivalenzen ausSatz 3.45 auf eine Subformel von ϕi anwendet.
(ohne Beweis)
229
§ 3.9 Die Adaquatheit der Junktoren
230
Boolesche Funktionen
Definition 3.52Eine boolesche Funktion ist eine Funktion f : {0,1}n → {0,1} fur einn ≥ 1.
NotationI Wir schreiben ϕ(X1, . . . ,Xn), um auszudrucken, dass
var(ϕ) ⊆ {X1, . . . ,Xn}.I Ist ϕ(X1, . . . ,Xn) eine Formel und B : {X1, . . . ,Xn} → {0,1} eine
Belegung mit bi := B(Xi) fur 1 ≤ i ≤ n, so schreiben wir auchϕ[b1, . . . ,bn] anstatt JϕKB.
Diese Notation zeigt, dass Formeln boolesche Funktionen berechnen.
231
Beschreibbarkeit boolescher Funktionen
Satz 3.53Fur jede boolesche Funktion f : {0,1}n → {0,1} gibt es eine Formelϕ(V1, . . . ,Vn), so dass fur alle b1, . . . ,bn ∈ {0,1}:
f (b1, . . . ,bn) = ϕ[b1, . . . ,bn].
232
Beweis des Satzes
Sei f : {0, 1}n → {0, 1}. Falls f (b) = 0 fur alle b ∈ {0, 1}n, so setzen wirϕ(V1, . . . ,Vn) := 000. Im folgenden nehmen wir an, dass f (b) = 1 furmindestens ein b ∈ {0, 1}n.Fur 1 ≤ i ≤ n und b ∈ {0, 1} sei
λi,b :=
{Vi falls b = 1,¬Vi falls b = 0.
Dann gilt fur alle Belegungen B mit Vi ∈ def(B):
B |= λi,b ⇐⇒ B(Vi) = b.
Fur b = (b1, . . . , bn) ∈ {0, 1}n sei
ψb(V1, . . . ,Vn) := (λ1,b1 ∧ . . .∧ λn,bn ).
Dann gilt fur alle Belegungen B : {V1, . . . ,Vn} → {0, 1}:
B |= ψb(V1, . . . ,Vn) ⇐⇒ Fur alle i , 1 ≤ i ≤ n : B(Vi) = bi .
233
Beweis des Satzes (cont.)
Anders ausgedruckt: Fur alle c ∈ {0, 1}n gilt:
ψb[c1, . . . , cn] = 1 ⇐⇒ c = b.
Nun seiϕ(V1, . . . ,Vn) :=
_b∈{0,1}n
f(b)=1
ψb(V1, . . . ,Vn).
Dann gilt fur alle Belegungen c ∈ {0, 1}n:
ϕ(c) = 1⇐⇒ Es gibt ein b ∈ {0, 1}n mit f (b) = 1 : ψb[c] = 1⇐⇒ Es gibt ein b ∈ {0, 1}n mit f (b) = 1 : c = b⇐⇒ f (c) = 1.
234
Adaquatheit
Definition 3.54Sei τ ⊆ {111,000,¬,∧,∨,→,↔}.
1. AL(τ) ist die Menge aller Formeln, die nur aus Variablen,Klammern, und den Symbolen in τ aufgebaut sind.
2. τ ist adaquat, wenn jede Formel in AL aquivalent zu einer Formelin AL(τ) ist.
Beispiel 3.55{111,000,¬,∨,∧} ist adaquat (vgl. Folgerung 3.44).
235
Adaquate Mengen
Lemma 3.56Fur alle Formeln ϕ,ψ gelten folgende Aquivalenzen:
1. ϕ∧ψ ≡ ¬(¬ϕ∨ ¬ψ), ϕ∨ψ ≡ ¬(¬ϕ∧ ¬ψ).
2. 111 ≡ ϕ∨ ¬ϕ, 000 ≡ ϕ∧ ¬ϕ.
Satz 3.57{∧,¬} und {∨,¬} sind adaquat.
Lemma 3.58Fur alle Formeln ϕ,ψ gelten folgende Aquivalenzen:
1. ϕ∨ψ ≡ ¬ϕ → ψ.2. ¬ϕ ≡ ϕ → 000.
Satz 3.59{→,¬} und {→,000} sind adaquat.
236
Eine nicht adaquate Menge
Satz 3.60{111,000,∨,∧} ist nicht adaquat.
237
Beweis von Satz 3.60
Wir zeigen fur alle Formeln ϕ(X ) ∈ AL({111,000,∨,∧}):
ϕ[0] = 0 oder ϕ[1] = 1. (?)
Damit ϕ(X ) 6≡ ¬X .Beweis von (?) per Induktion uber den Aufbau von ϕ:Induktionsanfang:
I Fur ϕ = 000 ist ϕ[0] = 0.I Fur ϕ = 111 und ϕ = X ist ϕ[1] = 1.
Induktionsschritt:I Sei ϕ(X ) = ψ1(X ) ∧ψ2(X ).
Falls ψ1[0] = 0 oder ψ2[0] = 0, so ϕ[0] = 0.Sonst nach (IA) ψ1[1] = ψ2[1] = 1 und damit ϕ[1] = 1.
I Sei ϕ(X ) = ψ1(X ) ∨ψ2(X ).Falls ψ1[0] = 0 und ψ2[0] = 0, so ϕ[0] = 0.Sonst nach (IA) ψ1[1] = 1 oder ψ2[1] = 1 und damit ϕ[1] = 1.
238
§ 3.10 Normalformen
239
Vereinfachende Annahme
In diesem Paragraphen betrachten wir nur Formeln in AL({¬,∨,∧}).
RechtfertigungDie Annahme bedeutet keine wesentliche Einschrankung, weil dieMenge {¬,∨,∧} adaquat ist.
240
NNF
Definition 3.61Eine Formel ist in Negationsnormalform (NNF), wenn sie nur dieJunktoren ¬,∧,∨ enthalt und wenn Negationszeichen nur unmittelbarvor Variablen auftreten.
Satz 3.62Jede Formel ist aquivalent zu einer Formel in NNF.
241
Ein NNF-Algorithmus
Eingabe: Formel ϕ ∈ AL({¬,∧,∨}).Ausgabe: Formel ϕ ′ in NNF
Verfahren:
1. Wiederhole folgende Schritte:2. Wenn ϕ in NNF ist, dann halte mit Ausgabe ϕ.3. Ersetze eine Subformel von ϕ der Gestalt
¬(ψ1 ∧ψ2) durch ¬ψ1 ∨ ¬ψ2oder eine Subformel der Gestalt
¬(ψ1 ∨ψ2) durch ¬ψ1 ∧ ¬ψ2oder eine Subformel der Gestalt
¬¬ψ durch ψ.Sei ϕ ′ die resultierende Formel.
4. ϕ := ϕ ′.
242
Satz 3.63Fur jede Eingabeformel ϕ ∈ AL({¬,∧,∨}) gibt der NNF-Algorithmusnach endlich vielen Schritten eine zu ϕ aquivalente Formel ϕ ′ in NNFaus.
243
Klammern bei Konjunktionen und Disjunktionen
Weil ∧ assoziativ ist, konnen wir Formeln der Gestalt∧n
i=1ϕi etwasgroßzugiger interpretieren. Von nun an stehe
∧ni=1ϕi fur
ϕ1 ∧ . . .∧ϕn mit irgendeiner Klammerung.
Entsprechend verfahren wir mit Disjunktionen.
Beispiel 3.64Die Formel
∧4i=1ϕi kann fur jede der folgenden Formeln stehen:
((ϕ1 ∧ϕ2) ∧ϕ3) ∧ϕ4,
(ϕ1 ∧ (ϕ2 ∧ϕ3)) ∧ϕ4,
(ϕ1 ∧ϕ2) ∧ (ϕ3 ∧ϕ4),
ϕ1 ∧ ((ϕ2 ∧ϕ3) ∧ϕ4),
ϕ1 ∧ (ϕ2 ∧ (ϕ3 ∧ϕ4)).
244
DNF und KNF
Definition 3.651. Ein Literal ist eine Formel der Gestalt X oder ¬X , wobei
X ∈ AVAR. (Im ersten Fall sprechen wir von einem positiven, imzweiten Fall von einem negativen Literal.)
2. Eine Formel ist in disjunktiver Normalform (DNF), wenn sie eineDisjunktion von Konjunktionen von Literalen ist, d.h., wenn siedie Gestalt
n∨i=1
mi∧j=1
λij
hat, wobei n,m1, . . . ,mn ≥ 1 und die λij , fur 1 ≤ i ≤ n,1 ≤ j ≤ mi ,Literale sind.Die Subformeln
∧mij=1 λij , fur 1 ≤ i ≤ n nennen wir die
(konjunktiven) Klauseln der Formel.
(Fortsetzung nachste Folie)
245
3. Eine Formel ist in konjunktiver Normalform (KNF), wenn sie eineKonjunktion von Disjunktion von Literalen ist, d.h., wenn sie dieGestalt
n∧i=1
mi∨j=1
λij
hat, wobei n,m1, . . . ,mn ≥ 1 und die λij , fur 1 ≤ i ≤ n,1 ≤ j ≤ mi ,Literale sind.Die Subformeln
∨mij=1 λij , fur 1 ≤ i ≤ n nennen wir die
(disjunktiven) Klauseln der Formel.
246
Satz 3.66Jede Formel ist aquivalent zu einer Formel in DNF und zu einerFormel in KNF.
247
Beweis des Satzes
Sei ψ eine Formel.
1. Falls ψ unerfullbar, so ist ψ ≡ V1 ∧ ¬V1. Die Formel V1 ∧ ¬V1 ist sowohlin KNF als auch in DNF.Falls ψ erfullbar ist, liefert der Beweis von Satz 3.53, angewandt auf dievon ψ berechnete boolesche Funktion, eine zu ψ aquivalente Formel inDNF (nachprufen).
2. Sei eψ die zu ψ duale Formel. Man beachte, dass eeψ = ψ.Sei ϕ eine zu eψ aquivalente Formel in DNF und eϕ die zu ϕ dualeFormel. Dann ist eϕ in KNF, und da
eψ ≡ ϕ
gilt nach Korollar 3.49
ψ =eeψ ≡ eϕ.
248
Ein DNF-Algorithmus
Eingabe: Formel ϕ ∈ AL({¬,∧,∨}) in NNF.Ausgabe: Formel ϕ ′ in DNF
Verfahren:
1. Wiederhole folgende Schritte:2. Wenn ϕ in DNF ist, dann halte mit
Ausgabe ϕ.3. Ersetze eine Subformel von ϕ der Gestalt
ψ1 ∧ (ψ2 ∨ψ3) durch (ψ1 ∧ψ2) ∨ (ψ1 ∧ψ3)oder eine Subformel der Gestalt
(ψ1 ∨ψ2) ∧ψ3 durch (ψ1 ∧ψ3) ∨ (ψ2 ∧ψ3).Sei ϕ ′ die resultierende Formel.
4. ϕ := ϕ ′.
249
Satz 3.67Fur jede Eingabeformel ϕ in NNF gibt der DNF-Algorithmus nachendlich vielen Schritten eine zu ϕ aquivalente Formel ϕ ′ in DNF aus.(ohne Beweis)
250
Eine kleine Formel mit großer DNF
Satz 3.68Sei n ≥ 1 und ϕn :=
∧ni=1(Xi ↔ Yi). Dann hat jede zu ϕn aquivalente
Formel in DNF mindestens 2n konjunktive Klauseln.(Beweis als Hausaufgabe)
251
Erfullbarkeit von Formeln in DNF
Lemma 3.691. Eine konjunktive Klausel λ1 ∧ . . .∧ λn ist genau dann erfullbar,
wenn λi 6= ¬λj fur 1 ≤ i , j ≤ n.2. Eine Formel in DNF ist genau dann erfullbar, wenn mindestens
eine ihrer Klauseln erfullbar ist.
252
Ein Erfullbarkeitstest fur Formeln in DNF
Die Erfullbarkeit einer DNF Formel lasst sich mit Hilfe des letztenLemmas ”leicht“ (und effizient) mit folgendem Verfahren testen:
Eingabe: Formel ϕ :=∨m
i=1∧ni
j=1 λij in DNF.Ziel: Entscheide ob ϕ erfullbar ist.
Verfahren:
1. Fur i = 1, . . . ,m2. Fur j = 1, . . . ,ni3. Fur k = j + 1, . . . ,ni4. Wenn λij = ¬λik oder λik = ¬λij dann5. Fahre fort mit dem nachsten i6. Halte mit Ausgabe ”ϕ ist erfullbar“7. Halte mit Ausgabe ”ϕ ist unerfullbar“
253
Das DNF-Verfahren zum Testen vonErfullbarkeit
Eingabe: Formel ϕZiel: Entscheide ob ϕ erfullbar ist.
Verfahren:
1. Finde zu ϕ aquivalente Formel ϕ1 ∈ AL({¬,∧,∨}).2. Finde zu ϕ1 aquivalente Formel ϕ2 in NNF.3. Finde zu ϕ2 aquivalente Formel ϕ3 in DNF.4. Teste, ob ϕ3 erfullbar ist.
254
§ 3.11 Anwendung: Schaltkreisentwurf
255
SchaltkreisentwurfDefinition 3.70Eine verallgemeinerte boolesche Funktion ist eine Funktionf : {0,1}m → {0,1}n fur m,n ≥ 1.
Beobachtung 3.71Ein Schaltkreis mit m Eingangen und n Ausgangen berechnet eineverallgemeinerte boolesche Funktion f : {0,1}m → {0,1}n.
Beobachtung 3.72Den Junktoren entsprechen einfache “logische” Schaltelemente.
Beispiel 3.73Schaltelemente fur ∧,∨,¬, die man als Und-Gatter, Oder-Gatter undInverter bezeichnet, werden ublicherweise wie folgt dargestellt:
256
Beispiel: Ein Addierer
1. Schritt: HalbaddiererEin-/Ausgabeverhalten:
D E A1 A0
0 0 0 00 1 0 11 0 0 11 1 1 0
Implementation:
257
2. Schritt: VolladdiererEin-/Ausgabeverhalten:
C D E A1 A0
0 0 0 0 00 0 1 0 10 1 0 0 11 0 0 0 10 1 1 1 01 0 1 1 01 1 0 1 01 1 1 1 1
Implementation:
258
3. Schritt: 4-Bit AddiererEin-/Ausgabeverhalten:
D3D2D1D0 + E3E2E1E0 = A4A3A2A1A0
Implementation:
259
Satz 3.74Ist τ eine adaquate Menge von Junktoren und τ die entsprechendeMenge von Schaltelementen, dann laßt sich jede verallgemeinerteboolesche Funktion durch einen Schaltkreis mit Schaltelementen in τberechnen.
260
Schaltkreisentwurf mittels DNF
Lemma 3.75Fur jede verallgemeinerte boolesche Funktion f : {0,1}m → {0,1}n gibtes Formeln
ϕ1(V1, . . . ,Vm), . . . , ϕn(V1, . . . ,Vm),
in DNF, so dass fur alle (b1, . . . ,bm) ∈ {0,1}m gilt:
f (b1, . . . ,bm) =(ϕ1[b1, . . . ,bm], . . . , ϕn[b1, . . . ,bm]
).
261
IdeeBasierend auf dem Lemma entwerfen wir Schaltkreise furverallgemeinerte boolesche Funktionen wie folgt:Ebene 1: Inverter und Und-GatterEbene 2: Oder-Gatter.Die Gatter der zweiten Ebene verwenden die Ausgange der erstenEbene gemeinsam.
262
Beispiel
A B C D E F0 0 0 0 0 00 0 1 1 0 00 1 0 1 0 00 1 1 1 1 01 0 0 1 0 01 0 1 1 1 01 1 0 1 1 01 1 1 1 0 1
DNF-BeschreibungϕD :=(¬XA ∧ ¬XB ∧ XC) ∨ (¬XA ∧ XB ∧ ¬XC) ∨ (¬XA ∧ XB ∧ XC)
∨(XA ∧ ¬XB ∧ ¬XC) ∨ (XA ∧ ¬XB ∧ XC) ∨ (XA ∧ XB ∧ ¬XC)
∨(XA ∧ XB ∧ XC),
ϕE :=(¬XA ∧ XB ∧ XC) ∨ (XA ∧ ¬XB ∧ XC) ∨ (XA ∧ XB ∧ ¬XC)
ϕF :=(XA ∧ XB ∧ XC).
263