20
|
1 \defineUnit{aussagenlogiksyntax}{% |
|
2 \begin{frame}[c] |
|
3 \frametitle{Syntax der Aussagenlogik} |
|
4 \setbeamercovered{dynamic} |
|
5 |
|
6 \begin{definition}[Syntax der Aussagenlogik] |
|
7 Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert. |
|
8 \begin{itemize} |
|
9 \item $\mathrm{false} = 0 \in \mathcal{F},\quad \mathrm{true} = 1 \in \mathcal{F}$\hfill(\alert{Konstanten}) |
|
10 \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\ |
|
11 \medskip |
|
12 \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch |
|
13 \begin{align} |
|
14 \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\ |
|
15 \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch} |
|
16 (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\ |
|
17 (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\ |
|
18 (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}} |
|
19 \end{align} |
|
20 \end{itemize} |
|
21 Alle Formeln lassen sich so konstruieren. |
|
22 \end{definition} |
|
23 \end{frame} |
|
24 |
|
25 \begin{frame} |
|
26 \frametitle{Operatorenbindung} |
|
27 \setbeamercovered{dynamic} |
|
28 |
|
29 \begin{definition}[Bindungsregeln] |
|
30 Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist |
|
31 \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \] |
|
32 Die Implikation ist \structure{rechtsassoziativ} |
|
33 \[ a \rightarrow b \rightarrow c \rightarrow d\text{\quad steht für\quad} \left( a \rightarrow \left( b \rightarrow \left( c \rightarrow d \right) \right) \right) \] |
|
34 \end{definition} |
|
35 \begin{itemize} |
|
36 \item Üblicherweise klammert man $\wedge$ und $\vee$ |
|
37 \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \] |
|
38 \end{itemize} |
|
39 \begin{example}[] |
|
40 \begin{itemize} |
|
41 \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$ |
|
42 \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$ |
|
43 \end{itemize} |
|
44 \end{example} |
|
45 \end{frame} |
|
46 |
|
47 \begin{frame} |
|
48 \frametitle{Syntaxbaum} |
|
49 \setbeamercovered{dynamic} |
|
50 |
|
51 \begin{block}{Syntaxbaum} |
|
52 \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen. |
|
53 \end{block} |
|
54 \begin{example}[] |
|
55 Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum |
|
56 \centering |
|
57 \begin{tikzpicture}[grow=down, level distance = 33] |
|
58 \tikzstyle{every node} = [] |
|
59 \tikzstyle{op} = [pretty] |
|
60 \tikzstyle{var} = [pretty, rectangle] |
|
61 \tikzstyle{edge from parent} = [edge] |
|
62 |
|
63 \tikzstyle{level 1} = [sibling distance = 80] |
|
64 \tikzstyle{level 2} = [sibling distance = 40] |
|
65 \node[op] {$\rightarrow$} |
|
66 child { |
|
67 node[op] {$\wedge$} |
|
68 edge from parent |
|
69 child { |
|
70 node[var] {$a$} |
|
71 edge from parent |
|
72 } |
|
73 child { |
|
74 node[var] {$b$} |
|
75 edge from parent |
|
76 } |
|
77 } |
|
78 child { |
|
79 node[op] {$\vee$} |
|
80 edge from parent |
|
81 child { |
|
82 node[var] {$c$} |
|
83 edge from parent |
|
84 } |
|
85 child { |
|
86 node[op] {$\neg$} |
|
87 edge from parent |
|
88 child { |
|
89 node[var] {$d$} |
|
90 edge from parent |
|
91 } |
|
92 } |
|
93 }; |
|
94 \end{tikzpicture} |
|
95 \end{example} |
|
96 \end{frame} |
|
97 } |
|
98 |
|
99 \defineUnit{aussagenlogiksemantik}{% |
|
100 \begin{frame} |
|
101 \frametitle{Belegung} |
|
102 \setbeamercovered{dynamic} |
|
103 |
|
104 \begin{definition}[Belegung] |
|
105 Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist |
|
106 \[ \beta : V \to \left\{ 0, 1 \right\} \] |
|
107 \end{definition} |
|
108 \begin{itemize} |
|
109 \item Belegungen formalisieren Einsetzen |
|
110 \item Für $n$ Variablen existieren $2^n$ Belegungen |
|
111 \end{itemize} |
|
112 \begin{example}[] |
|
113 Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und |
|
114 \begin{align} |
|
115 \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\ |
|
116 a &\mapsto 1\\ |
|
117 b &\mapsto 0 |
|
118 \end{align} |
|
119 Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}. |
|
120 \end{example} |
|
121 \end{frame} |
|
122 |
|
123 \begin{frame} |
|
124 \frametitle{Semantik der Aussagenlogik} |
|
125 \setbeamercovered{dynamic} |
|
126 |
|
127 \begin{definition}[Semantik einer Formel] |
|
128 Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\ |
|
129 Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist |
|
130 \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\] |
|
131 \end{definition} |
|
132 \begin{itemize} |
|
133 \item Die Semantik löst eingesetzte Formeln auf |
|
134 \item Wird anhand der induktiven Syntax definiert |
|
135 \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik} |
|
136 \end{itemize} |
|
137 \begin{example}[] |
|
138 Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist |
|
139 \[ [F](\beta) = \begin{cases} |
|
140 0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\ |
|
141 1 & \text{sonst} |
|
142 \end{cases}\] |
|
143 \end{example} |
|
144 \end{frame} |
|
145 |
|
146 \begin{frame} |
|
147 \frametitle{Wahrheitstabelle} |
|
148 \setbeamercovered{dynamic} |
|
149 |
|
150 \begin{block}{Wahrheitstabelle} |
|
151 Die Semantik einer Formel kann mit Hilfe einer \structure{Wahrheitstabelle} visualisiert werden. Die Tabelle gibt den Wahrheitswert der Formel für jede mögliche Belegung an. |
|
152 \end{block} |
|
153 \begin{example}[] |
|
154 Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist |
|
155 \begin{center} |
|
156 \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc} |
|
157 a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-} |
|
158 0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\ |
|
159 0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\ |
|
160 0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ |
|
161 0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ |
|
162 1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\ |
|
163 1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ |
|
164 1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ |
|
165 1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ |
|
166 \end{tabu} |
|
167 \end{center} |
|
168 \end{example} |
|
169 \end{frame} |
|
170 |
|
171 \begin{frame} |
|
172 \frametitle{Äquivalente Formeln} |
|
173 \setbeamercovered{dynamic} |
|
174 |
|
175 \begin{definition}[Äquivalente Formeln] |
|
176 Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\ |
|
177 Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn |
|
178 \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \] |
|
179 Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}. |
|
180 \end{definition} |
|
181 |
|
182 \begin{example}[] |
|
183 Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. |
|
184 \begin{center} |
|
185 \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} |
|
186 a & b & & $a \Rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} |
|
187 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ |
|
188 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ |
|
189 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ |
|
190 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ |
|
191 \end{tabu} |
|
192 \end{center} |
|
193 \end{example} |
|
194 \end{frame} |
|
195 |
|
196 \begin{frame} |
|
197 \frametitle{Eigenschaften von Formeln} |
|
198 \setbeamercovered{dynamic} |
|
199 |
|
200 \begin{block}{Eigenschaften aussagenlogischer Formeln} |
|
201 Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F |
|
202 \begin{description}[\quad unerfüllbar] |
|
203 \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein) |
|
204 \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr) |
|
205 \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr) |
|
206 \end{description} |
|
207 \end{block} |
|
208 \begin{itemize} |
|
209 \item Eine unerfüllbare Formel nennt man \structure{Widerspruch} |
|
210 \item Eine gültige Formel nennt man \structure{Tautologie} |
|
211 \end{itemize} |
|
212 |
|
213 \end{frame} |
|
214 } |
|
215 |
|
216 \defineUnit{aussagenlogikaequivalenzen}{% |
|
217 { |
|
218 \newcommand{\true}{1} |
|
219 \newcommand{\false}{0} |
|
220 \newcommand{\spc}{\hspace{3em}} |
|
221 \newcommand{\F}{F} |
|
222 \newcommand{\G}{G} |
|
223 \newcommand{\K}{H} |
|
224 |
|
225 \begin{frame} |
|
226 \frametitle{Äquivalenzregeln} |
|
227 \setbeamercovered{dynamic} |
|
228 |
|
229 \begin{description}[Triviale Kontradiktion\quad] |
|
230 \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ |
|
231 \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ |
|
232 \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ |
|
233 \item[Doppelte Negation] $\neg \neg \F \equiv \F$ |
|
234 \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ |
|
235 \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ |
|
236 \bigskip |
|
237 \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ |
|
238 $\F \wedge \G \equiv \G \wedge \F$ |
|
239 \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ |
|
240 $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ |
|
241 \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ |
|
242 $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ |
|
243 \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ |
|
244 $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ |
|
245 \bigskip |
|
246 \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$ |
|
247 \item[Bikonditional] $\F \leftrightarrow \G \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F)$ |
|
248 \end{description} |
|
249 \end{frame} |
|
250 |
|
251 %\begin{frame} |
|
252 %\frametitle{Äquivalenzregeln} |
|
253 %\setbeamercovered{dynamic} |
|
254 |
|
255 %\vspace{-2em} |
|
256 %\begin{align} |
|
257 %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ |
|
258 %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ |
|
259 %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ |
|
260 %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ |
|
261 %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ |
|
262 %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ |
|
263 %\bigskip |
|
264 %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ |
|
265 %\F \wedge \G &\equiv \G \wedge \F\\ |
|
266 %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ |
|
267 %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ |
|
268 %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ |
|
269 %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ |
|
270 %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ |
|
271 %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ |
|
272 %\bigskip |
|
273 %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ |
|
274 %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ |
|
275 %\end{align} |
|
276 %\end{frame} |
|
277 } |
|
278 } |
|
279 |
|
280 \defineUnit{aussagenlogiknormalformen}{% |
|
281 \begin{frame}[c] |
|
282 \frametitle{Literale und Klauseln} |
|
283 \setbeamercovered{dynamic} |
|
284 |
|
285 \begin{definition}[Literal] |
|
286 Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable. |
|
287 \end{definition} |
|
288 |
|
289 \begin{definition}[Klausel] |
|
290 Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator. |
|
291 \end{definition} |
|
292 |
|
293 \vfill |
|
294 |
|
295 \begin{example}[] |
|
296 Seien $a, \neg b, c$ Literale. Dann sind |
|
297 \begin{itemize} |
|
298 \item $a \wedge \neg b \wedge c$ |
|
299 \item $a \vee \neg b \vee c$ |
|
300 \end{itemize} |
|
301 Klauseln. |
|
302 \end{example} |
|
303 \end{frame} |
|
304 |
|
305 { |
|
306 \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}} |
|
307 \begin{frame} |
|
308 \frametitle{DNF} |
|
309 \setbeamercovered{dynamic} |
|
310 |
|
311 \begin{definition}[Disjunktive Normalform] |
|
312 Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\ |
|
313 Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist. |
|
314 \[ F \defeq \bigvee \bigwedge_i L_i \] |
|
315 \end{definition} |
|
316 \begin{itemize} |
|
317 \item Ausnahme: $\textrm{false}$ ist auch in DNF |
|
318 \end{itemize} |
|
319 |
|
320 \begin{example}[] |
|
321 $F$ ist in DNF. |
|
322 \[ F \defeq \klausel{DNF}{a \structure{\wedge} b \structure{\wedge} \neg c} \alert{\vee} \klausel{DNF}{\neg b \structure{\wedge} c} \alert{\vee} \klausel{DNF}{\neg a \structure{\wedge} b \structure{\wedge} \neg c} \] |
|
323 \end{example} |
|
324 \end{frame} |
|
325 |
|
326 \begin{frame} |
|
327 \frametitle{KNF} |
|
328 \setbeamercovered{dynamic} |
|
329 |
|
330 \begin{definition}[Konjunktive Normalform] |
|
331 Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\ |
|
332 Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist. |
|
333 \[ F \defeq \bigwedge \bigvee_i L_i \] |
|
334 \end{definition} |
|
335 \begin{itemize} |
|
336 \item Ausnahme: $\textrm{true}$ ist auch in KNF |
|
337 \end{itemize} |
|
338 |
|
339 \begin{example}[] |
|
340 $F$ ist in KNF. |
|
341 \[ F \defeq \klausel{KNF}{\neg a \alert{\vee} b} \structure{\wedge} \klausel{KNF}{\neg b \alert{\vee} c} \structure{\wedge} \klausel{KNF}{a \alert{\vee} b \alert{\vee} \neg c} \] |
|
342 \end{example} |
|
343 \end{frame} |
|
344 } |
|
345 |
|
346 \begin{frame} |
|
347 \frametitle{Konstruktion der NF} |
|
348 \setbeamercovered{dynamic} |
|
349 |
|
350 \begin{itemize} |
|
351 \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar |
|
352 \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!) |
|
353 \item Oder: Konstruktion mit Wahrheitstabellen |
|
354 \end{itemize} |
|
355 |
|
356 \vfill |
|
357 |
|
358 \begin{block}{Normalformen aus Wahrheitstabellen} |
|
359 Gegeben eine Formel $F$ und ihre Wahrheitstabelle |
|
360 \begin{itemize} |
|
361 \item DNF |
|
362 \begin{enumerate} |
|
363 \item Betrachte Zeilen mit Eintrag \structure{$1$} |
|
364 \item Bilde \structure{Konjunktion} aus der \structure{Belegung} |
|
365 \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln |
|
366 \end{enumerate} |
|
367 \bigskip |
|
368 \item KNF |
|
369 \begin{enumerate} |
|
370 \item Betrachte Zeilen mit Eintrag \alert{$0$} |
|
371 \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung |
|
372 \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln |
|
373 \end{enumerate} |
|
374 \end{itemize} |
|
375 \end{block} |
|
376 \end{frame} |
|
377 |
|
378 { |
|
379 \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)} |
|
380 \begin{frame} |
|
381 \frametitle{Konstruktion der NF} |
|
382 \setbeamercovered{dynamic} |
|
383 |
|
384 \begin{example}[] |
|
385 Gegeben eine Formel $F$ mit folgender Semantik |
|
386 \begin{center} |
|
387 \begin{tabu} to .4\textwidth {ccc|[1.2pt]c} |
|
388 a & b & c & $F$ \\ \tabucline[1.2pt]{-} |
|
389 0 & 0 & 0 & 0 \\ |
|
390 0 & 0 & 1 & 0 \\ |
|
391 0 & 1 & 0 & 0 \\ |
|
392 0 & 1 & 1 & 1 \\ |
|
393 1 & 0 & 0 & 1 \\ |
|
394 1 & 0 & 1 & 1 \\ |
|
395 1 & 1 & 0 & 1 \\ |
|
396 1 & 1 & 1 & 0 |
|
397 \end{tabu} |
|
398 \end{center} |
|
399 $F$ dargestellt in |
|
400 \begin{itemize} |
|
401 \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$ |
|
402 \medskip |
|
403 \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$ |
|
404 \end{itemize} |
|
405 \end{example} |
|
406 \end{frame} |
|
407 |
|
408 \begin{frame} |
|
409 \frametitle{Mengendarstellung der KNF} |
|
410 \setbeamercovered{dynamic} |
|
411 |
|
412 \begin{block}{Mengendarstellung der KNF} |
|
413 Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden. |
|
414 \begin{itemize} |
|
415 \item Klauseln werden durch Mengen von Literalen dargestellt |
|
416 \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\] |
|
417 \item KNF-Formeln sind Mengen von Klauseln |
|
418 \[ \left\{ \left\{ \neg a \right\}, \left\{ a, \neg b, c \right\} \right\} \text{ steht für } \neg a \wedge (a \vee \neg b \vee c) \] |
|
419 \item $\emptyset$ steht für \textrm{true}, $\left\{ \emptyset \right\}$ für \textrm{false} |
|
420 \end{itemize} |
|
421 \end{block} |
|
422 \begin{example}[] |
|
423 Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF. |
|
424 \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\] |
|
425 \end{example} |
|
426 \end{frame} |
|
427 } |
|
428 } |
|
429 |
|
430 \defineUnit{DPLL}{% |
|
431 \begin{frame} |
|
432 \frametitle{KNF aus Syntaxbaum} |
|
433 \setbeamercovered{dynamic} |
|
434 |
|
435 \begin{block}{Idee} |
|
436 Erzeuge die KNF aus dem Syntaxbaum |
|
437 \begin{enumerate} |
|
438 \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu |
|
439 \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern |
|
440 \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen} |
|
441 \end{enumerate} |
|
442 \end{block} |
|
443 \begin{columns}[T] |
|
444 \begin{column}{.7\textwidth} |
|
445 % FIXME: onlys around A_\vee needed for "correct" fadein |
|
446 \begin{align} |
|
447 (x \wedge y) \vee z |
|
448 \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\ |
|
449 &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\ |
|
450 &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\} |
|
451 \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\ |
|
452 &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\ |
|
453 &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\ |
|
454 &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\ |
|
455 &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}} |
|
456 \end{align} |
|
457 \end{column} |
|
458 \begin{column}{.3\textwidth} |
|
459 \begin{tikzpicture}[grow=down, level distance = 33] |
|
460 \tikzstyle{op} = [pretty] |
|
461 \tikzstyle{var} = [pretty, rectangle] |
|
462 \tikzstyle{edge from parent} = [edge] |
|
463 |
|
464 \tikzstyle{level 1} = [sibling distance = 50] |
|
465 \tikzstyle{level 2} = [sibling distance = 30] |
|
466 \node at (0, 0) {}; |
|
467 \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}} |
|
468 child { |
|
469 node[op] {\alt<1>{$\wedge$}{$A_\wedge$}} |
|
470 edge from parent |
|
471 child { |
|
472 node[var] {$x$} |
|
473 edge from parent |
|
474 } |
|
475 child { |
|
476 node[var] {$y$} |
|
477 edge from parent |
|
478 } |
|
479 } |
|
480 child { |
|
481 node[var] {$z$} |
|
482 }; |
|
483 \end{tikzpicture} |
|
484 \end{column} |
|
485 \end{columns} |
|
486 \end{frame} |
|
487 |
|
488 \begin{frame} |
|
489 \frametitle{DPLL} |
|
490 \setbeamercovered{dynamic} |
|
491 |
|
492 \begin{definition}[DPLL-Belegung] |
|
493 Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\ |
|
494 Dann bezeichnet \structure{$F[p\backslash\mathrm{true}]$} die Formel, die entsteht, wenn jedes Vorkommnis von $p$ in F durch $\mathrm{true}$ ersetzt und vereinfacht wird. |
|
495 \end{definition} |
|
496 |
|
497 \begin{block}{DPLL} |
|
498 Gegeben eine Formel $F$ in KNF |
|
499 \begin{itemize} |
|
500 \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar} |
|
501 \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar} |
|
502 \item Sonst |
|
503 \begin{enumerate} |
|
504 \item Wähle eine Variable $p$ in $F$ |
|
505 \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar |
|
506 \end{enumerate} |
|
507 \end{itemize} |
|
508 \end{block} |
|
509 \begin{itemize} |
|
510 \item Schlaue Wahl der Variable beschleunigt Ausführung |
|
511 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) |
|
512 \end{itemize} |
|
513 \end{frame} |
|
514 } |