Mercurial > 13ws.ds
annotate notes/tex/logic.tex @ 28:f639b478a28b
typo
author | Markus Kaiser <markus.kaiser@in.tum.de> |
---|---|
date | Mon, 02 Dec 2013 10:52:41 +0100 |
parents | 4436f8006ebd |
children | b5094b3e3111 |
rev | line source |
---|---|
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} | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
9 \item $\false = 0 = \bot \in \mathcal{F},\quad \true = 1 = \top \in \mathcal{F}$\hfill(\alert{Konstanten}) |
20 | 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 { | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
218 \newcommand{\spc}{\hfill} |
20 | 219 \newcommand{\F}{F} |
220 \newcommand{\G}{G} | |
221 \newcommand{\K}{H} | |
222 | |
223 \begin{frame} | |
224 \frametitle{Äquivalenzregeln} | |
225 \setbeamercovered{dynamic} | |
226 | |
227 \begin{description}[Triviale Kontradiktion\quad] | |
228 \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ | |
229 \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ | |
230 \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ | |
231 \item[Doppelte Negation] $\neg \neg \F \equiv \F$ | |
232 \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ | |
233 \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ | |
234 \bigskip | |
235 \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ | |
236 $\F \wedge \G \equiv \G \wedge \F$ | |
237 \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ | |
238 $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ | |
239 \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ | |
240 $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ | |
241 \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ | |
242 $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ | |
243 \bigskip | |
244 \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$ | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
245 \item[Bikonditional] $\F \leftrightarrow \G \equiv \neg(\F \otimes \G) \left[ \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \right]$ |
20 | 246 \end{description} |
247 \end{frame} | |
248 | |
249 %\begin{frame} | |
250 %\frametitle{Äquivalenzregeln} | |
251 %\setbeamercovered{dynamic} | |
252 | |
253 %\vspace{-2em} | |
254 %\begin{align} | |
255 %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ | |
256 %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ | |
257 %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ | |
258 %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ | |
259 %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ | |
260 %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ | |
261 %\bigskip | |
262 %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ | |
263 %\F \wedge \G &\equiv \G \wedge \F\\ | |
264 %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ | |
265 %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ | |
266 %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ | |
267 %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ | |
268 %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ | |
269 %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ | |
270 %\bigskip | |
271 %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ | |
272 %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ | |
273 %\end{align} | |
274 %\end{frame} | |
275 } | |
276 } | |
277 | |
278 \defineUnit{aussagenlogiknormalformen}{% | |
279 \begin{frame}[c] | |
280 \frametitle{Literale und Klauseln} | |
281 \setbeamercovered{dynamic} | |
282 | |
283 \begin{definition}[Literal] | |
284 Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable. | |
285 \end{definition} | |
286 | |
287 \begin{definition}[Klausel] | |
288 Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator. | |
289 \end{definition} | |
290 | |
291 \vfill | |
292 | |
293 \begin{example}[] | |
294 Seien $a, \neg b, c$ Literale. Dann sind | |
295 \begin{itemize} | |
296 \item $a \wedge \neg b \wedge c$ | |
297 \item $a \vee \neg b \vee c$ | |
298 \end{itemize} | |
299 Klauseln. | |
300 \end{example} | |
301 \end{frame} | |
302 | |
303 { | |
304 \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}} | |
305 \begin{frame} | |
306 \frametitle{DNF} | |
307 \setbeamercovered{dynamic} | |
308 | |
309 \begin{definition}[Disjunktive Normalform] | |
310 Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\ | |
311 Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist. | |
312 \[ F \defeq \bigvee \bigwedge_i L_i \] | |
313 \end{definition} | |
314 \begin{itemize} | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
315 \item Ausnahme: $\false$ ist auch in DNF |
20 | 316 \end{itemize} |
317 | |
318 \begin{example}[] | |
319 $F$ ist in DNF. | |
320 \[ 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} \] | |
321 \end{example} | |
322 \end{frame} | |
323 | |
324 \begin{frame} | |
325 \frametitle{KNF} | |
326 \setbeamercovered{dynamic} | |
327 | |
328 \begin{definition}[Konjunktive Normalform] | |
329 Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\ | |
330 Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist. | |
331 \[ F \defeq \bigwedge \bigvee_i L_i \] | |
332 \end{definition} | |
333 \begin{itemize} | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
334 \item Ausnahme: $\true$ ist auch in KNF |
20 | 335 \end{itemize} |
336 | |
337 \begin{example}[] | |
338 $F$ ist in KNF. | |
339 \[ 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} \] | |
340 \end{example} | |
341 \end{frame} | |
342 } | |
343 | |
344 \begin{frame} | |
345 \frametitle{Konstruktion der NF} | |
346 \setbeamercovered{dynamic} | |
347 | |
348 \begin{itemize} | |
349 \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar | |
350 \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!) | |
351 \item Oder: Konstruktion mit Wahrheitstabellen | |
352 \end{itemize} | |
353 | |
354 \vfill | |
355 | |
356 \begin{block}{Normalformen aus Wahrheitstabellen} | |
357 Gegeben eine Formel $F$ und ihre Wahrheitstabelle | |
358 \begin{itemize} | |
359 \item DNF | |
360 \begin{enumerate} | |
361 \item Betrachte Zeilen mit Eintrag \structure{$1$} | |
362 \item Bilde \structure{Konjunktion} aus der \structure{Belegung} | |
363 \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln | |
364 \end{enumerate} | |
365 \bigskip | |
366 \item KNF | |
367 \begin{enumerate} | |
368 \item Betrachte Zeilen mit Eintrag \alert{$0$} | |
369 \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung | |
370 \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln | |
371 \end{enumerate} | |
372 \end{itemize} | |
373 \end{block} | |
374 \end{frame} | |
375 | |
376 { | |
377 \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)} | |
378 \begin{frame} | |
379 \frametitle{Konstruktion der NF} | |
380 \setbeamercovered{dynamic} | |
381 | |
382 \begin{example}[] | |
383 Gegeben eine Formel $F$ mit folgender Semantik | |
384 \begin{center} | |
385 \begin{tabu} to .4\textwidth {ccc|[1.2pt]c} | |
386 a & b & c & $F$ \\ \tabucline[1.2pt]{-} | |
387 0 & 0 & 0 & 0 \\ | |
388 0 & 0 & 1 & 0 \\ | |
389 0 & 1 & 0 & 0 \\ | |
390 0 & 1 & 1 & 1 \\ | |
391 1 & 0 & 0 & 1 \\ | |
392 1 & 0 & 1 & 1 \\ | |
393 1 & 1 & 0 & 1 \\ | |
394 1 & 1 & 1 & 0 | |
395 \end{tabu} | |
396 \end{center} | |
397 $F$ dargestellt in | |
398 \begin{itemize} | |
399 \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$ | |
400 \medskip | |
401 \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$ | |
402 \end{itemize} | |
403 \end{example} | |
404 \end{frame} | |
405 | |
406 \begin{frame} | |
407 \frametitle{Mengendarstellung der KNF} | |
408 \setbeamercovered{dynamic} | |
409 | |
410 \begin{block}{Mengendarstellung der KNF} | |
411 Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden. | |
412 \begin{itemize} | |
413 \item Klauseln werden durch Mengen von Literalen dargestellt | |
414 \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\] | |
415 \item KNF-Formeln sind Mengen von Klauseln | |
416 \[ \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) \] | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
417 \item $\emptyset$ steht für $\true$, $\left\{ \emptyset \right\}$ für $\false$ |
20 | 418 \end{itemize} |
419 \end{block} | |
420 \begin{example}[] | |
421 Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF. | |
422 \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\] | |
423 \end{example} | |
424 \end{frame} | |
425 } | |
426 } | |
427 | |
428 \defineUnit{DPLL}{% | |
429 \begin{frame} | |
430 \frametitle{KNF aus Syntaxbaum} | |
431 \setbeamercovered{dynamic} | |
432 | |
433 \begin{block}{Idee} | |
434 Erzeuge die KNF aus dem Syntaxbaum | |
435 \begin{enumerate} | |
436 \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu | |
437 \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern | |
438 \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen} | |
439 \end{enumerate} | |
440 \end{block} | |
441 \begin{columns}[T] | |
442 \begin{column}{.7\textwidth} | |
443 % FIXME: onlys around A_\vee needed for "correct" fadein | |
444 \begin{align} | |
445 (x \wedge y) \vee z | |
446 \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\ | |
447 &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\ | |
448 &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\} | |
449 \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\ | |
450 &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\ | |
451 &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\ | |
452 &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\ | |
453 &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}} | |
454 \end{align} | |
455 \end{column} | |
456 \begin{column}{.3\textwidth} | |
457 \begin{tikzpicture}[grow=down, level distance = 33] | |
458 \tikzstyle{op} = [pretty] | |
459 \tikzstyle{var} = [pretty, rectangle] | |
460 \tikzstyle{edge from parent} = [edge] | |
461 | |
462 \tikzstyle{level 1} = [sibling distance = 50] | |
463 \tikzstyle{level 2} = [sibling distance = 30] | |
464 \node at (0, 0) {}; | |
465 \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}} | |
466 child { | |
467 node[op] {\alt<1>{$\wedge$}{$A_\wedge$}} | |
468 edge from parent | |
469 child { | |
470 node[var] {$x$} | |
471 edge from parent | |
472 } | |
473 child { | |
474 node[var] {$y$} | |
475 edge from parent | |
476 } | |
477 } | |
478 child { | |
479 node[var] {$z$} | |
480 }; | |
481 \end{tikzpicture} | |
482 \end{column} | |
483 \end{columns} | |
484 \end{frame} | |
485 | |
486 \begin{frame} | |
487 \frametitle{DPLL} | |
488 \setbeamercovered{dynamic} | |
489 | |
490 \begin{definition}[DPLL-Belegung] | |
491 Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\ | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
492 Dann bezeichnet \structure{$F[p\backslash\true]$} die Formel, die entsteht, wenn jedes Vorkommnis von $p$ in F durch $\true$ ersetzt und vereinfacht wird. |
20 | 493 \end{definition} |
494 | |
495 \begin{block}{DPLL} | |
496 Gegeben eine Formel $F$ in KNF | |
497 \begin{itemize} | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
498 \item Wenn $F = \true$ dann antworte \structure{erfüllbar} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
499 \item Wenn $F = \false$ dann antworte \structure{unerfüllbar} |
20 | 500 \item Sonst |
501 \begin{enumerate} | |
502 \item Wähle eine Variable $p$ in $F$ | |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
503 \item Prüfe ob $F[p\backslash\true]$ oder $F[p\backslash\false]$ erfüllbar |
20 | 504 \end{enumerate} |
505 \end{itemize} | |
506 \end{block} | |
507 \begin{itemize} | |
508 \item Schlaue Wahl der Variable beschleunigt Ausführung | |
509 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) | |
510 \end{itemize} | |
511 \end{frame} | |
512 } | |
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
513 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
514 \defineUnit{resolution}{% |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
515 \begin{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
516 \frametitle{Resolution} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
517 \setbeamercovered{dynamic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
518 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
519 \begin{definition}[Resolvent] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
520 Seien $K_1$, $K_2$ und $R$ Klauseln in Mengendarstellung. Dann heißt $R$ \structure{Resolvent} von $K_1$ und $K_2$ wenn $L \in K_1$, $\neg L \in K_2$ und |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
521 \begin{align} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
522 R &= \left( K_1 \setminus \left\{ L \right\} \right) \cup \left( K_2 \setminus \left\{ \neg L \right\} \right) |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
523 \end{align} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
524 \end{definition} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
525 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
526 \begin{block}{Resolution} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
527 Gegeben eine Formel $F$ in KNF in Mengendarstellung. |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
528 \begin{algorithmic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
529 \While{$\square = \emptyset \not \in F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
530 \State{$R \gets \text{Resolvent aus } F \text{ mit } R \not\in F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
531 \If{$R$ existiert} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
532 \State{$F \gets F \cup R$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
533 \Else |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
534 \State{\textbf{return} \structure{erfüllbar}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
535 \EndIf |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
536 \EndWhile |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
537 \State{\textbf{return} \structure{unerfüllbar}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
538 \end{algorithmic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
539 \end{block} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
540 \end{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
541 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
542 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
543 \defineUnit{natuerlichesschliessen}{% |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
544 \begin{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
545 \frametitle{Kalküle} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
546 \setbeamercovered{dynamic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
547 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
548 \begin{definition}[Kalkül] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
549 Ein \structure{Logikkalkül} stellt \structure{Inferenzregeln} bereit, mit denen Formeln \alert{syntaktisch} umgeformt werden können. |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
550 \end{definition} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
551 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
552 \begin{definition}[Folgerung] |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
553 $F$ \structure{folgt aus} $A$, wenn mit Hilfe der \alert{Semantik} der \alert{Aussagenlogik} $F$ unter der Annahme dass $A$ gilt zu $\true$ ausgewertet wird. Wir schreiben |
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
554 \[ A \vDash F \] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
555 \end{definition} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
556 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
557 \begin{definition}[Ableitung] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
558 $F$ kann aus $A$ \structure{abgeleitet} werden, wenn mit Hilfe \alert{syntaktischer} Umformungen in einem \alert{Logikkalkül} $F$ unter der Annahme $A$ bewiesen werden kann. Wir schreiben |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
559 \[ A \vdash F \] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
560 \end{definition} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
561 \end{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
562 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
563 \begin{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
564 \frametitle{Eigenschaften von Kalkülen} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
565 \setbeamercovered{dynamic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
566 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
567 \begin{block}{Eigenschaften von Kalkülen} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
568 \begin{description}[\quad vollständig (complete)] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
569 \item[korrekt (sound)] Es können \alert{nur} semantisch gültige Formeln abgeleitet werden. |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
570 \[ \text{Aus } A \vdash F \text{ folgt } A \vDash F \] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
571 \item[vollständig (complete)] \alert{Alle} semantisch gültigen Formeln können abgeleitet werden. |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
572 \[ \text{Aus } A \vDash F \text{ folgt } A \vdash F \] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
573 \end{description} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
574 \end{block} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
575 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
576 \begin{itemize} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
577 \item Für uns nur korrekte vollständige Kalküle |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
578 \item Beispiel für die Aussagenlogik: \structure{Natürliches Schließen} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
579 \medskip |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
580 \item Es gibt keine solchen Kalküle für die |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
581 \begin{itemize} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
582 \item Prädikatenlogik |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
583 \item Arithmetik |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
584 \end{itemize} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
585 \item Deshalb sind nicht alle Sätze der Mathematik beweisbar |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
586 \end{itemize} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
587 \end{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
588 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
589 { |
24 | 590 \newcommand{\F}{\tau} |
591 \newcommand{\G}{\varphi} | |
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
592 \newcommand{\K}{\chi} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
593 \newcommand{\subproof}[2]{% |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
594 \begin{tikzpicture}[y=.9em] |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
595 \path |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
596 (0, 0) node (a) {##1} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
597 ++(0, -1) node (b) {$\vdots$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
598 ++(0, -1) node[below] (c) {##2}; |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
599 \node[fit=(a)(b)(c), draw, inner sep=1pt] {}; |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
600 \end{tikzpicture}% |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
601 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
602 \newcommand{\topproof}[1]{% |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
603 ##1 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
604 \bottomAlignProof |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
605 \DisplayProof |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
606 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
607 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
608 \begin{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
609 \frametitle{Natürliches Schließen} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
610 \setbeamercovered{dynamic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
611 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
612 \vspace{-4pt} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
613 \tabulinesep=4pt |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
614 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
615 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
616 $\wedge$ & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
617 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
618 \AxiomC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
619 \AxiomC{$\G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
620 \RightLabel{\scriptsize $+\wedge$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
621 \BinaryInfC{$\F \wedge \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
622 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
623 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
624 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
625 \AxiomC{$\F \wedge \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
626 \RightLabel{\scriptsize $-\wedge_1$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
627 \UnaryInfC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
628 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
629 \quad |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
630 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
631 \AxiomC{$\F \wedge \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
632 \RightLabel{\scriptsize $-\wedge_2$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
633 \UnaryInfC{$\G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
634 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
635 \\ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
636 $\vee$ & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
637 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
638 \AxiomC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
639 \RightLabel{\scriptsize $+\vee_1$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
640 \UnaryInfC{$\F \vee \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
641 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
642 \quad |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
643 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
644 \AxiomC{$\G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
645 \RightLabel{\scriptsize $+\vee_2$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
646 \UnaryInfC{$\F \vee \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
647 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
648 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
649 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
650 \AxiomC{$\F \vee \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
651 \AxiomC{\subproof{$\F$}{$\K$}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
652 \AxiomC{\subproof{$\G$}{$\K$}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
653 \RightLabel{\scriptsize $-\vee$} |
23 | 654 \TrinaryInfC{$\K$\vphantom{$\F\G$}} |
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
655 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
656 \\ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
657 $\rightarrow$ & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
658 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
659 \AxiomC{\subproof{$\F$}{$\G$}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
660 \RightLabel{\scriptsize $+\rightarrow$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
661 \UnaryInfC{$\F \rightarrow \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
662 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
663 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
664 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
665 \AxiomC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
666 \AxiomC{$\F \rightarrow \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
667 \RightLabel{\scriptsize $-\rightarrow$, MP} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
668 \BinaryInfC{$\G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
669 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
670 \\ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
671 $\neg$ & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
672 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
673 \AxiomC{\subproof{$\F$}{$\bot$}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
674 \RightLabel{\scriptsize $+\neg$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
675 \UnaryInfC{$\neg \F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
676 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
677 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
678 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
679 \AxiomC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
680 \AxiomC{$\neg\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
681 \RightLabel{\scriptsize $-\neg$} |
24 | 682 \BinaryInfC{$\bot$} |
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
683 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
684 \end{tabu} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
685 \end{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
686 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
687 \begin{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
688 \frametitle{Natürliches Schließen} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
689 \setbeamercovered{dynamic} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
690 |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
691 \vspace{-4pt} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
692 \tabulinesep=4pt |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
693 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
694 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
695 $\bot$ & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
696 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
697 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
698 \AxiomC{$\bot$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
699 \RightLabel{\scriptsize $-\bot$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
700 \UnaryInfC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
701 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
702 \\ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
703 $\neg\neg$ & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
704 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
705 \AxiomC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
706 \RightLabel{\scriptsize $+\neg\neg$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
707 \UnaryInfC{$\neg\neg\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
708 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
709 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
710 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
711 \AxiomC{$\neg\neg\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
712 \RightLabel{\scriptsize $-\neg\neg$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
713 \UnaryInfC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
714 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
715 \end{tabu} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
716 \begin{itemize} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
717 \vfill |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
718 \item Praktische abgeleitete Regeln |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
719 \end{itemize} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
720 \tabulinesep=10pt |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
721 \begin{tabu} to \textwidth {X[c,m,.5]X[c,b,5]X[c,b,5]} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
722 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
723 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
724 \AxiomC{ } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
725 \RightLabel{\scriptsize LEM} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
726 \UnaryInfC{$\F \vee \neg\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
727 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
728 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
729 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
730 \AxiomC{\subproof{$\neg\F$}{$\bot$}} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
731 \RightLabel{\scriptsize $-\neg$, PBC} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
732 \UnaryInfC{$\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
733 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
734 \\ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
735 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
736 & |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
737 \topproof{ |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
738 \AxiomC{$\neg\G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
739 \AxiomC{$\F \rightarrow \G$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
740 \RightLabel{\scriptsize MT} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
741 \BinaryInfC{$\neg\F$} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
742 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
743 \end{tabu} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
744 \end{frame} |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
745 } |
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
746 } |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
747 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
748 \defineUnit{praedikatenlogiksyntax}{% |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
749 { |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
750 \newcommand{\terms}{\mathcal{T}} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
751 \newcommand{\preds}{\mathcal{P}} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
752 \newcommand{\logic}{\mathcal{L}} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
753 \begin{frame}[c] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
754 \frametitle{Syntax der Prädikatenlogik} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
755 \setbeamercovered{dynamic} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
756 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
757 \begin{definition}[Term] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
758 Die Menge $\terms$ aller \structure{Terme} ist induktiv definiert. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
759 \begin{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
760 \item Jede Konstante ist in $\terms$ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
761 \item Jede Variable ist in $\terms$ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
762 \item Sind $f$ eine Funktion und $t_1, \dots, t_n$ Terme, dann auch |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
763 \[ f(t_1, \dots, t_n) \] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
764 \end{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
765 Funktionen wandeln Terme in \alert{Terme} um. Wir beschreiben sie mit Kleinbuchstaben. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
766 \end{definition} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
767 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
768 \begin{definition}[Prädikat] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
769 \structure{Prädikate} $P$ wandeln Terme in \alert{Wahrheitswerte} um. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
770 Wir beschreiben sie mit Großbuchstaben.\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
771 Die Menge $\preds$ enthält alle \structure{Prädikate}. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
772 \end{definition} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
773 \end{frame} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
774 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
775 \begin{frame}[c] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
776 \frametitle{Syntax der Prädikatenlogik} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
777 \setbeamercovered{dynamic} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
778 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
779 \begin{definition}[Syntax der Prädikatenlogik] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
780 Die Menge \structure{$\logic$} aller \structure{prädikatenlogischen Formeln} ist induktiv definiert. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
781 Seien $A, B\in \logic$, $t_i \in \terms$ und $P \in \preds$. Dann sind alle Formeln |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
782 { |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
783 \setlength{\belowdisplayskip}{0pt} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
784 \setlength{\abovedisplayskip}{0pt} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
785 \begin{itemize} |
28 | 786 \item Grundbausteine |
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
787 \smallskip |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
788 \begin{align} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
789 V = \left\{ a, b, \dots \right\} &\subseteq \logic\tag{\alert{Variablen}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
790 P(t_1, \dots, t_n) &\in \logic\tag{\alert{Prädikate, Konstanten}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
791 t_i = t_j &\in\logic\tag{\alert{Gleichheit}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
792 \shortintertext{\item Verknüpfungen der Aussagenlogik} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
793 \neg A &\in \logic\tag{\alert{Negation}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
794 (A \wedge B), (A \vee B)&\in \logic\tag{\alert{Konjunktion, Disjunktion}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
795 (A \rightarrow B)&\in \logic\tag{\alert{Implikation}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
796 \shortintertext{\item \structure{Quantoren}} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
797 \exists x. A &\in \logic\tag{\alert{Existenzquantor}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
798 \forall x. A &\in \logic\tag{\alert{Allquantor}}\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
799 \end{align} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
800 \end{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
801 } |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
802 \vspace{-1.5em} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
803 \end{definition} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
804 \end{frame} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
805 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
806 \begin{frame} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
807 \frametitle{Operatorenbindung} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
808 \setbeamercovered{dynamic} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
809 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
810 \begin{definition}[Bindungsregeln] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
811 Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
812 \[ \forall \quad \exists \quad \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
813 Die Implikation ist \structure{rechtsassoziativ}. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
814 \end{definition} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
815 \begin{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
816 \item Üblicherweise klammert man wieder $\wedge$ und $\vee$ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
817 \item Genauso klammert man Quantoren |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
818 \[ \left( \forall x. F \right) \rightarrow G \text{\quad statt\quad} \forall x. F \rightarrow G \] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
819 \vfill |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
820 \item \alert{Achtung!} Äußere Quantoren werden öfter anders interpretiert |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
821 \[ \forall x \forall y. F \wedge G \leftrightarrow H \] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
822 Bindet formal \alert{nur an das F}! |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
823 \end{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
824 \end{frame} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
825 } |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
826 } |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
827 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
828 \defineUnit{praedikatenlogikstruktur}{% |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
829 \begin{frame}[c] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
830 \frametitle{Struktur} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
831 \setbeamercovered{dynamic} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
832 |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
833 \begin{definition}[Struktur] |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
834 Eine passende \structure{Struktur} $S = \left( U_s, I_s \right)$ zu einer Formel $F$ besteht aus einem \structure{Universum} $U_s$ und einer \structure{Interpretation} $I_s$. |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
835 \begin{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
836 \item Alle Terme werten zu einem Wert im \structure{Universum} $U_s$ aus |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
837 \item Die \structure{Interpretation} $I_s$ weist den Atomen der Formel Werte zu.\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
838 Sie spezifiziert |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
839 \begin{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
840 \item \alert{Variablen} $x$ mit |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
841 { |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
842 \setlength{\belowdisplayskip}{0pt} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
843 \setlength{\abovedisplayskip}{0pt} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
844 \begin{align} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
845 x_s \in {} &U_s\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
846 \shortintertext{\item \alert{Konstanten} $a$ mit} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
847 a_s \in {} &U_s\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
848 \shortintertext{\item \alert{k-stellige Prädikate} $P$ mit} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
849 P_s \subseteq {} &U_s^k\\ |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
850 \shortintertext{\item \alert{Funktionen} $f$ mit} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
851 f_s : {} &U_s^k \to U_s |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
852 \end{align} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
853 } |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
854 \end{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
855 \end{itemize} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
856 \end{definition} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
857 \end{frame} |
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
858 } |