Mercurial > 13ws.ds
annotate notes/tex/logic.tex @ 45:e65f4b1a6e32
remove fairly useless setbeamercovered
| author | Markus Kaiser <markus.kaiser@in.tum.de> |
|---|---|
| date | Wed, 08 Jan 2014 14:26:02 +0100 |
| parents | 3de775b67d8c |
| children | a78ea627829e |
| rev | line source |
|---|---|
| 20 | 1 \defineUnit{aussagenlogiksyntax}{% |
| 2 \begin{frame}[c] | |
| 3 \frametitle{Syntax der Aussagenlogik} | |
| 4 | |
| 5 \begin{definition}[Syntax der Aussagenlogik] | |
| 6 Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert. | |
| 7 \begin{itemize} | |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
8 \item $\false = 0 = \bot \in \mathcal{F},\quad \true = 1 = \top \in \mathcal{F}$\hfill(\alert{Konstanten}) |
| 20 | 9 \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\ |
| 10 \medskip | |
| 11 \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch | |
| 12 \begin{align} | |
| 13 \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\ | |
| 14 \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch} | |
| 15 (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\ | |
| 16 (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\ | |
| 17 (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}} | |
| 18 \end{align} | |
| 19 \end{itemize} | |
| 20 Alle Formeln lassen sich so konstruieren. | |
| 21 \end{definition} | |
| 22 \end{frame} | |
| 23 | |
| 24 \begin{frame} | |
| 25 \frametitle{Operatorenbindung} | |
| 26 | |
| 27 \begin{definition}[Bindungsregeln] | |
| 28 Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist | |
| 29 \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \] | |
| 30 Die Implikation ist \structure{rechtsassoziativ} | |
| 31 \[ 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) \] | |
| 32 \end{definition} | |
| 33 \begin{itemize} | |
| 34 \item Üblicherweise klammert man $\wedge$ und $\vee$ | |
| 35 \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \] | |
| 36 \end{itemize} | |
| 37 \begin{example}[] | |
| 38 \begin{itemize} | |
| 39 \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$ | |
| 40 \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$ | |
| 41 \end{itemize} | |
| 42 \end{example} | |
| 43 \end{frame} | |
| 44 | |
| 45 \begin{frame} | |
| 46 \frametitle{Syntaxbaum} | |
| 47 | |
| 48 \begin{block}{Syntaxbaum} | |
| 49 \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen. | |
| 50 \end{block} | |
| 51 \begin{example}[] | |
| 52 Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum | |
| 53 \centering | |
| 54 \begin{tikzpicture}[grow=down, level distance = 33] | |
| 55 \tikzstyle{every node} = [] | |
| 56 \tikzstyle{op} = [pretty] | |
| 57 \tikzstyle{var} = [pretty, rectangle] | |
| 58 \tikzstyle{edge from parent} = [edge] | |
| 59 | |
| 60 \tikzstyle{level 1} = [sibling distance = 80] | |
| 61 \tikzstyle{level 2} = [sibling distance = 40] | |
| 62 \node[op] {$\rightarrow$} | |
| 63 child { | |
| 64 node[op] {$\wedge$} | |
| 65 edge from parent | |
| 66 child { | |
| 67 node[var] {$a$} | |
| 68 edge from parent | |
| 69 } | |
| 70 child { | |
| 71 node[var] {$b$} | |
| 72 edge from parent | |
| 73 } | |
| 74 } | |
| 75 child { | |
| 76 node[op] {$\vee$} | |
| 77 edge from parent | |
| 78 child { | |
| 79 node[var] {$c$} | |
| 80 edge from parent | |
| 81 } | |
| 82 child { | |
| 83 node[op] {$\neg$} | |
| 84 edge from parent | |
| 85 child { | |
| 86 node[var] {$d$} | |
| 87 edge from parent | |
| 88 } | |
| 89 } | |
| 90 }; | |
| 91 \end{tikzpicture} | |
| 92 \end{example} | |
| 93 \end{frame} | |
| 94 } | |
| 95 | |
| 96 \defineUnit{aussagenlogiksemantik}{% | |
| 97 \begin{frame} | |
| 98 \frametitle{Belegung} | |
| 99 | |
| 100 \begin{definition}[Belegung] | |
| 101 Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist | |
| 102 \[ \beta : V \to \left\{ 0, 1 \right\} \] | |
| 103 \end{definition} | |
| 104 \begin{itemize} | |
| 105 \item Belegungen formalisieren Einsetzen | |
| 106 \item Für $n$ Variablen existieren $2^n$ Belegungen | |
| 107 \end{itemize} | |
| 108 \begin{example}[] | |
| 109 Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und | |
| 110 \begin{align} | |
| 111 \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\ | |
| 112 a &\mapsto 1\\ | |
| 113 b &\mapsto 0 | |
| 114 \end{align} | |
| 115 Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}. | |
| 116 \end{example} | |
| 117 \end{frame} | |
| 118 | |
| 119 \begin{frame} | |
| 120 \frametitle{Semantik der Aussagenlogik} | |
| 121 | |
| 122 \begin{definition}[Semantik einer Formel] | |
| 123 Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\ | |
| 124 Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist | |
| 125 \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\] | |
| 126 \end{definition} | |
| 127 \begin{itemize} | |
| 128 \item Die Semantik löst eingesetzte Formeln auf | |
| 129 \item Wird anhand der induktiven Syntax definiert | |
| 130 \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik} | |
| 131 \end{itemize} | |
| 132 \begin{example}[] | |
| 133 Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist | |
| 134 \[ [F](\beta) = \begin{cases} | |
| 135 0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\ | |
| 136 1 & \text{sonst} | |
| 137 \end{cases}\] | |
| 138 \end{example} | |
| 139 \end{frame} | |
| 140 | |
| 141 \begin{frame} | |
| 142 \frametitle{Wahrheitstabelle} | |
| 143 | |
| 144 \begin{block}{Wahrheitstabelle} | |
| 145 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. | |
| 146 \end{block} | |
| 147 \begin{example}[] | |
| 148 Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist | |
| 149 \begin{center} | |
| 150 \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc} | |
| 151 a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-} | |
| 152 0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\ | |
| 153 0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\ | |
| 154 0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ | |
| 155 0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ | |
| 156 1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\ | |
| 157 1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ | |
| 158 1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ | |
| 159 1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ | |
| 160 \end{tabu} | |
| 161 \end{center} | |
| 162 \end{example} | |
| 163 \end{frame} | |
| 164 | |
| 165 \begin{frame} | |
| 166 \frametitle{Äquivalente Formeln} | |
| 167 | |
| 168 \begin{definition}[Äquivalente Formeln] | |
| 169 Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\ | |
| 170 Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn | |
| 171 \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \] | |
| 172 Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}. | |
| 173 \end{definition} | |
| 174 | |
| 175 \begin{example}[] | |
| 176 Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. | |
| 177 \begin{center} | |
| 178 \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} | |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
179 a & b & & $a \rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} |
| 20 | 180 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ |
| 181 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ | |
| 182 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ | |
| 183 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ | |
| 184 \end{tabu} | |
| 185 \end{center} | |
| 186 \end{example} | |
| 187 \end{frame} | |
| 188 | |
| 189 \begin{frame} | |
| 190 \frametitle{Eigenschaften von Formeln} | |
| 191 | |
| 192 \begin{block}{Eigenschaften aussagenlogischer Formeln} | |
| 193 Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F | |
| 194 \begin{description}[\quad unerfüllbar] | |
| 195 \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein) | |
| 196 \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr) | |
| 197 \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr) | |
| 198 \end{description} | |
| 199 \end{block} | |
| 200 \begin{itemize} | |
| 201 \item Eine unerfüllbare Formel nennt man \structure{Widerspruch} | |
| 202 \item Eine gültige Formel nennt man \structure{Tautologie} | |
| 203 \end{itemize} | |
| 204 | |
| 205 \end{frame} | |
| 206 } | |
| 207 | |
| 208 \defineUnit{aussagenlogikaequivalenzen}{% | |
| 209 { | |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
210 \newcommand{\spc}{\hfill} |
| 20 | 211 \newcommand{\F}{F} |
| 212 \newcommand{\G}{G} | |
| 213 \newcommand{\K}{H} | |
| 214 | |
| 215 \begin{frame} | |
| 216 \frametitle{Äquivalenzregeln} | |
| 217 | |
| 218 \begin{description}[Triviale Kontradiktion\quad] | |
| 219 \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ | |
| 220 \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ | |
| 221 \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ | |
| 222 \item[Doppelte Negation] $\neg \neg \F \equiv \F$ | |
| 223 \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ | |
| 224 \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ | |
| 225 \bigskip | |
| 226 \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ | |
| 227 $\F \wedge \G \equiv \G \wedge \F$ | |
| 228 \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ | |
| 229 $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ | |
| 230 \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ | |
| 231 $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ | |
| 232 \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ | |
| 233 $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ | |
| 234 \bigskip | |
| 235 \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
|
236 \item[Bikonditional] $\F \leftrightarrow \G \equiv \neg(\F \otimes \G) \left[ \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \right]$ |
| 20 | 237 \end{description} |
| 238 \end{frame} | |
| 239 | |
| 240 %\begin{frame} | |
| 241 %\frametitle{Äquivalenzregeln} | |
| 242 | |
| 243 %\vspace{-2em} | |
| 244 %\begin{align} | |
| 245 %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ | |
| 246 %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ | |
| 247 %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ | |
| 248 %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ | |
| 249 %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ | |
| 250 %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ | |
| 251 %\bigskip | |
| 252 %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ | |
| 253 %\F \wedge \G &\equiv \G \wedge \F\\ | |
| 254 %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ | |
| 255 %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ | |
| 256 %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ | |
| 257 %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ | |
| 258 %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ | |
| 259 %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ | |
| 260 %\bigskip | |
| 261 %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ | |
| 262 %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ | |
| 263 %\end{align} | |
| 264 %\end{frame} | |
| 265 } | |
| 266 } | |
| 267 | |
| 268 \defineUnit{aussagenlogiknormalformen}{% | |
| 269 \begin{frame}[c] | |
| 270 \frametitle{Literale und Klauseln} | |
| 271 | |
| 272 \begin{definition}[Literal] | |
| 273 Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable. | |
| 274 \end{definition} | |
| 275 | |
| 276 \begin{definition}[Klausel] | |
| 277 Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator. | |
| 278 \end{definition} | |
| 279 | |
| 280 \vfill | |
| 281 | |
| 282 \begin{example}[] | |
| 283 Seien $a, \neg b, c$ Literale. Dann sind | |
| 284 \begin{itemize} | |
| 285 \item $a \wedge \neg b \wedge c$ | |
| 286 \item $a \vee \neg b \vee c$ | |
| 287 \end{itemize} | |
| 288 Klauseln. | |
| 289 \end{example} | |
| 290 \end{frame} | |
| 291 | |
| 292 { | |
| 293 \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}} | |
| 294 \begin{frame} | |
| 295 \frametitle{DNF} | |
| 296 | |
| 297 \begin{definition}[Disjunktive Normalform] | |
| 298 Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\ | |
| 299 Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist. | |
| 300 \[ F \defeq \bigvee \bigwedge_i L_i \] | |
| 301 \end{definition} | |
| 302 \begin{itemize} | |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
303 \item Ausnahme: $\false$ ist auch in DNF |
| 20 | 304 \end{itemize} |
| 305 | |
| 306 \begin{example}[] | |
| 307 $F$ ist in DNF. | |
| 308 \[ 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} \] | |
| 309 \end{example} | |
| 310 \end{frame} | |
| 311 | |
| 312 \begin{frame} | |
| 313 \frametitle{KNF} | |
| 314 | |
| 315 \begin{definition}[Konjunktive Normalform] | |
| 316 Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\ | |
| 317 Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist. | |
| 318 \[ F \defeq \bigwedge \bigvee_i L_i \] | |
| 319 \end{definition} | |
| 320 \begin{itemize} | |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
321 \item Ausnahme: $\true$ ist auch in KNF |
| 20 | 322 \end{itemize} |
| 323 | |
| 324 \begin{example}[] | |
| 325 $F$ ist in KNF. | |
| 326 \[ 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} \] | |
| 327 \end{example} | |
| 328 \end{frame} | |
| 329 } | |
| 330 | |
| 331 \begin{frame} | |
| 332 \frametitle{Konstruktion der NF} | |
| 333 | |
| 334 \begin{itemize} | |
| 335 \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar | |
| 336 \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!) | |
| 337 \item Oder: Konstruktion mit Wahrheitstabellen | |
| 338 \end{itemize} | |
| 339 | |
| 340 \vfill | |
| 341 | |
| 342 \begin{block}{Normalformen aus Wahrheitstabellen} | |
| 343 Gegeben eine Formel $F$ und ihre Wahrheitstabelle | |
| 344 \begin{itemize} | |
| 345 \item DNF | |
| 346 \begin{enumerate} | |
| 347 \item Betrachte Zeilen mit Eintrag \structure{$1$} | |
| 348 \item Bilde \structure{Konjunktion} aus der \structure{Belegung} | |
| 349 \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln | |
| 350 \end{enumerate} | |
| 351 \bigskip | |
| 352 \item KNF | |
| 353 \begin{enumerate} | |
| 354 \item Betrachte Zeilen mit Eintrag \alert{$0$} | |
| 355 \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung | |
| 356 \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln | |
| 357 \end{enumerate} | |
| 358 \end{itemize} | |
| 359 \end{block} | |
| 360 \end{frame} | |
| 361 | |
| 362 { | |
| 363 \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)} | |
| 364 \begin{frame} | |
| 365 \frametitle{Konstruktion der NF} | |
| 366 | |
| 367 \begin{example}[] | |
| 368 Gegeben eine Formel $F$ mit folgender Semantik | |
| 369 \begin{center} | |
| 370 \begin{tabu} to .4\textwidth {ccc|[1.2pt]c} | |
| 371 a & b & c & $F$ \\ \tabucline[1.2pt]{-} | |
| 372 0 & 0 & 0 & 0 \\ | |
| 373 0 & 0 & 1 & 0 \\ | |
| 374 0 & 1 & 0 & 0 \\ | |
| 375 0 & 1 & 1 & 1 \\ | |
| 376 1 & 0 & 0 & 1 \\ | |
| 377 1 & 0 & 1 & 1 \\ | |
| 378 1 & 1 & 0 & 1 \\ | |
| 379 1 & 1 & 1 & 0 | |
| 380 \end{tabu} | |
| 381 \end{center} | |
| 382 $F$ dargestellt in | |
| 383 \begin{itemize} | |
| 384 \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$ | |
| 385 \medskip | |
| 386 \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$ | |
| 387 \end{itemize} | |
| 388 \end{example} | |
| 389 \end{frame} | |
| 390 | |
| 391 \begin{frame} | |
| 392 \frametitle{Mengendarstellung der KNF} | |
| 393 | |
| 394 \begin{block}{Mengendarstellung der KNF} | |
| 395 Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden. | |
| 396 \begin{itemize} | |
| 397 \item Klauseln werden durch Mengen von Literalen dargestellt | |
| 398 \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\] | |
| 399 \item KNF-Formeln sind Mengen von Klauseln | |
| 400 \[ \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
|
401 \item $\emptyset$ steht für $\true$, $\left\{ \emptyset \right\}$ für $\false$ |
| 20 | 402 \end{itemize} |
| 403 \end{block} | |
| 404 \begin{example}[] | |
| 405 Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF. | |
| 406 \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\] | |
| 407 \end{example} | |
| 408 \end{frame} | |
| 409 } | |
| 410 } | |
| 411 | |
| 412 \defineUnit{DPLL}{% | |
| 413 \begin{frame} | |
| 414 \frametitle{KNF aus Syntaxbaum} | |
| 415 | |
| 416 \begin{block}{Idee} | |
| 417 Erzeuge die KNF aus dem Syntaxbaum | |
| 418 \begin{enumerate} | |
| 419 \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu | |
| 420 \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern | |
| 421 \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen} | |
| 422 \end{enumerate} | |
| 423 \end{block} | |
| 424 \begin{columns}[T] | |
| 425 \begin{column}{.7\textwidth} | |
| 426 % FIXME: onlys around A_\vee needed for "correct" fadein | |
| 427 \begin{align} | |
| 428 (x \wedge y) \vee z | |
| 429 \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\ | |
| 430 &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\ | |
| 431 &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\} | |
| 432 \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\ | |
| 433 &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\ | |
| 434 &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\ | |
| 435 &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\ | |
| 436 &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}} | |
| 437 \end{align} | |
| 438 \end{column} | |
| 439 \begin{column}{.3\textwidth} | |
| 440 \begin{tikzpicture}[grow=down, level distance = 33] | |
| 441 \tikzstyle{op} = [pretty] | |
| 442 \tikzstyle{var} = [pretty, rectangle] | |
| 443 \tikzstyle{edge from parent} = [edge] | |
| 444 | |
| 445 \tikzstyle{level 1} = [sibling distance = 50] | |
| 446 \tikzstyle{level 2} = [sibling distance = 30] | |
| 447 \node at (0, 0) {}; | |
| 448 \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}} | |
| 449 child { | |
| 450 node[op] {\alt<1>{$\wedge$}{$A_\wedge$}} | |
| 451 edge from parent | |
| 452 child { | |
| 453 node[var] {$x$} | |
| 454 edge from parent | |
| 455 } | |
| 456 child { | |
| 457 node[var] {$y$} | |
| 458 edge from parent | |
| 459 } | |
| 460 } | |
| 461 child { | |
| 462 node[var] {$z$} | |
| 463 }; | |
| 464 \end{tikzpicture} | |
| 465 \end{column} | |
| 466 \end{columns} | |
| 467 \end{frame} | |
| 468 | |
| 469 \begin{frame} | |
| 470 \frametitle{DPLL} | |
| 471 | |
| 472 \begin{definition}[DPLL-Belegung] | |
| 473 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
|
474 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 | 475 \end{definition} |
| 476 | |
| 477 \begin{block}{DPLL} | |
| 478 Gegeben eine Formel $F$ in KNF | |
| 479 \begin{itemize} | |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
480 \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
|
481 \item Wenn $F = \false$ dann antworte \structure{unerfüllbar} |
| 20 | 482 \item Sonst |
| 483 \begin{enumerate} | |
| 484 \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
|
485 \item Prüfe ob $F[p\backslash\true]$ oder $F[p\backslash\false]$ erfüllbar |
| 20 | 486 \end{enumerate} |
| 487 \end{itemize} | |
| 488 \end{block} | |
| 489 \begin{itemize} | |
| 490 \item Schlaue Wahl der Variable beschleunigt Ausführung | |
| 491 \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) | |
| 492 \end{itemize} | |
| 493 \end{frame} | |
| 494 } | |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
495 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
496 \defineUnit{resolution}{% |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
497 \begin{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
498 \frametitle{Resolution} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
499 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
500 \begin{definition}[Resolvent] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
501 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
|
502 \begin{align} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
503 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
|
504 \end{align} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
505 \end{definition} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
506 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
507 \begin{block}{Resolution} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
508 Gegeben eine Formel $F$ in KNF in Mengendarstellung. |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
509 \begin{algorithmic} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
510 \While{$\square = \emptyset \not \in F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
511 \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
|
512 \If{$R$ existiert} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
513 \State{$F \gets F \cup R$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
514 \Else |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
515 \State{\textbf{return} \structure{erfüllbar}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
516 \EndIf |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
517 \EndWhile |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
518 \State{\textbf{return} \structure{unerfüllbar}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
519 \end{algorithmic} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
520 \end{block} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
521 \end{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
522 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
523 |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
524 \defineUnit{kalkuele}{% |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
525 \begin{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
526 \frametitle{Kalküle} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
527 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
528 \begin{definition}[Kalkül] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
529 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
|
530 \end{definition} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
531 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
532 \begin{definition}[Folgerung] |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
533 $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
|
534 \[ A \vDash F \] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
535 \end{definition} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
536 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
537 \begin{definition}[Ableitung] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
538 $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
|
539 \[ A \vdash F \] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
540 \end{definition} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
541 \end{frame} |
|
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 \begin{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
544 \frametitle{Eigenschaften von Kalkülen} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
545 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
546 \begin{block}{Eigenschaften von Kalkülen} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
547 \begin{description}[\quad vollständig (complete)] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
548 \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
|
549 \[ \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
|
550 \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
|
551 \[ \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
|
552 \end{description} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
553 \end{block} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
554 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
555 \begin{itemize} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
556 \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
|
557 \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
|
558 \medskip |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
559 \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
|
560 \begin{itemize} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
561 \item Prädikatenlogik |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
562 \item Arithmetik |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
563 \end{itemize} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
564 \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
|
565 \end{itemize} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
566 \end{frame} |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
567 } |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
568 |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
569 \defineUnit{natuerlichesschliessen}{% |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
570 { |
| 24 | 571 \newcommand{\F}{\tau} |
| 572 \newcommand{\G}{\varphi} | |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
573 \newcommand{\K}{\chi} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
574 \newcommand{\subproof}[2]{% |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
575 \begin{tikzpicture}[y=.9em] |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
576 \path |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
577 (0, 0) node (a) {##1} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
578 ++(0, -1) node (b) {$\vdots$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
579 ++(0, -1) node[below] (c) {##2}; |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
580 \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
|
581 \end{tikzpicture}% |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
582 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
583 \newcommand{\topproof}[1]{% |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
584 ##1 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
585 \bottomAlignProof |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
586 \DisplayProof |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
587 } |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
588 \newcommand{\capt}[1]{\vspace{-1em}##1} |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
589 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
590 \begin{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
591 \frametitle{Natürliches Schließen} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
592 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
593 \tabulinesep=4pt |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
594 \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
|
595 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
596 \capt{$\wedge$} & |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
597 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
598 \AxiomC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
599 \AxiomC{$\G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
600 \RightLabel{\scriptsize $+\wedge$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
601 \BinaryInfC{$\F \wedge \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
602 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
603 & |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
604 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
605 \AxiomC{$\F \wedge \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
606 \RightLabel{\scriptsize $-\wedge_1$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
607 \UnaryInfC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
608 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
609 \quad |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
610 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
611 \AxiomC{$\F \wedge \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
612 \RightLabel{\scriptsize $-\wedge_2$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
613 \UnaryInfC{$\G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
614 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
615 \\ |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
616 \capt{$\vee$} & |
|
22
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 \RightLabel{\scriptsize $+\vee_1$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
620 \UnaryInfC{$\F \vee \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
621 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
622 \quad |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
623 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
624 \AxiomC{$\G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
625 \RightLabel{\scriptsize $+\vee_2$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
626 \UnaryInfC{$\F \vee \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
627 } |
|
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 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
630 \AxiomC{$\F \vee \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
631 \AxiomC{\subproof{$\F$}{$\K$}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
632 \AxiomC{\subproof{$\G$}{$\K$}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
633 \RightLabel{\scriptsize $-\vee$} |
| 23 | 634 \TrinaryInfC{$\K$\vphantom{$\F\G$}} |
|
22
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 \\ |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
637 \capt{$\rightarrow$} & |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
638 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
639 \AxiomC{\subproof{$\F$}{$\G$}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
640 \RightLabel{\scriptsize $+\rightarrow$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
641 \UnaryInfC{$\F \rightarrow \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
642 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
643 & |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
644 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
645 \AxiomC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
646 \AxiomC{$\F \rightarrow \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
647 \RightLabel{\scriptsize $-\rightarrow$, MP} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
648 \BinaryInfC{$\G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
649 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
650 \\ |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
651 \capt{$\neg$} & |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
652 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
653 \AxiomC{\subproof{$\F$}{$\bot$}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
654 \RightLabel{\scriptsize $+\neg$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
655 \UnaryInfC{$\neg \F$} |
|
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 & |
|
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{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
660 \AxiomC{$\neg\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
661 \RightLabel{\scriptsize $-\neg$} |
| 24 | 662 \BinaryInfC{$\bot$} |
|
22
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 \end{tabu} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
665 \end{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
666 |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
667 \begin{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
668 \frametitle{Natürliches Schließen} |
|
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 \tabulinesep=4pt |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
671 \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
|
672 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
673 \capt{$\bot$} & |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
674 & |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
675 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
676 \AxiomC{$\bot$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
677 \RightLabel{\scriptsize $-\bot$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
678 \UnaryInfC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
679 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
680 \\ |
|
32
b5094b3e3111
reorganize units; fix spacing in calculus rules; fix small old errors
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
28
diff
changeset
|
681 \capt{$\neg\neg$} & |
|
22
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
682 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
683 \AxiomC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
684 \RightLabel{\scriptsize $+\neg\neg$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
685 \UnaryInfC{$\neg\neg\F$} |
|
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 & |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
688 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
689 \AxiomC{$\neg\neg\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
690 \RightLabel{\scriptsize $-\neg\neg$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
691 \UnaryInfC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
692 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
693 \end{tabu} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
694 \begin{itemize} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
695 \vfill |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
696 \item Praktische abgeleitete Regeln |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
697 \end{itemize} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
698 \tabulinesep=10pt |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
699 \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
|
700 & |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
701 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
702 \AxiomC{ } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
703 \RightLabel{\scriptsize LEM} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
704 \UnaryInfC{$\F \vee \neg\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
705 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
706 & |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
707 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
708 \AxiomC{\subproof{$\neg\F$}{$\bot$}} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
709 \RightLabel{\scriptsize $-\neg$, PBC} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
710 \UnaryInfC{$\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
711 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
712 \\ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
713 & |
|
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 \topproof{ |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
716 \AxiomC{$\neg\G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
717 \AxiomC{$\F \rightarrow \G$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
718 \RightLabel{\scriptsize MT} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
719 \BinaryInfC{$\neg\F$} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
720 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
721 \end{tabu} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
722 \end{frame} |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
723 } |
|
dc6b569c57c8
fifth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
20
diff
changeset
|
724 } |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
725 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
726 \defineUnit{praedikatenlogiksyntax}{% |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
727 { |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
728 \newcommand{\terms}{\mathcal{T}} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
729 \newcommand{\preds}{\mathcal{P}} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
730 \newcommand{\logic}{\mathcal{L}} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
731 \begin{frame}[c] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
732 \frametitle{Syntax der Prädikatenlogik} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
733 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
734 \begin{definition}[Term] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
735 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
|
736 \begin{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
737 \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
|
738 \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
|
739 \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
|
740 \[ 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
|
741 \end{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
742 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
|
743 \end{definition} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
744 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
745 \begin{definition}[Prädikat] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
746 \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
|
747 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
|
748 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
|
749 \end{definition} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
750 \end{frame} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
751 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
752 \begin{frame}[c] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
753 \frametitle{Syntax der Prädikatenlogik} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
754 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
755 \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
|
756 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
|
757 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
|
758 { |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
759 \setlength{\belowdisplayskip}{0pt} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
760 \setlength{\abovedisplayskip}{0pt} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
761 \begin{itemize} |
| 28 | 762 \item Grundbausteine |
|
26
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
763 \smallskip |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
764 \begin{align} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
765 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
|
766 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
|
767 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
|
768 \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
|
769 \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
|
770 (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
|
771 (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
|
772 \shortintertext{\item \structure{Quantoren}} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
773 \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
|
774 \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
|
775 \end{align} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
776 \end{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
777 } |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
778 \vspace{-1.5em} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
779 \end{definition} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
780 \end{frame} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
781 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
782 \begin{frame} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
783 \frametitle{Operatorenbindung} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
784 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
785 \begin{definition}[Bindungsregeln] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
786 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
|
787 \[ \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
|
788 Die Implikation ist \structure{rechtsassoziativ}. |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
789 \end{definition} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
790 \begin{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
791 \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
|
792 \item Genauso klammert man Quantoren |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
793 \[ \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
|
794 \vfill |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
795 \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
|
796 \[ \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
|
797 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
|
798 \end{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
799 \end{frame} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
800 } |
|
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 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
803 \defineUnit{praedikatenlogikstruktur}{% |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
804 \begin{frame}[c] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
805 \frametitle{Struktur} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
806 |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
807 \begin{definition}[Struktur] |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
808 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
|
809 \begin{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
810 \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
|
811 \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
|
812 Sie spezifiziert |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
813 \begin{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
814 \item \alert{Variablen} $x$ mit |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
815 { |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
816 \setlength{\belowdisplayskip}{0pt} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
817 \setlength{\abovedisplayskip}{0pt} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
818 \begin{align} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
819 x_s \in {} &U_s\\ |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
820 \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
|
821 a_s \in {} &U_s\\ |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
822 \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
|
823 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
|
824 \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
|
825 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
|
826 \end{align} |
|
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 \end{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
829 \end{itemize} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
830 \end{definition} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
831 \end{frame} |
|
4436f8006ebd
fix minor errors; sixth slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
24
diff
changeset
|
832 } |
|
35
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
833 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
834 \defineUnit{natuerlichesschliessenquantoren}{% |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
835 { |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
836 \newcommand{\F}{\tau} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
837 \newcommand{\G}{\varphi} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
838 \newcommand{\K}{\chi} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
839 \newcommand{\subproof}[2]{% |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
840 \begin{tikzpicture}[y=.9em] |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
841 \path |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
842 (0, 0) node (a) {##1} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
843 ++(0, -1) node (b) {$\vdots$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
844 ++(0, -1) node[below] (c) {##2}; |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
845 \node[fit=(a)(b)(c), draw, inner sep=1pt] {}; |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
846 \end{tikzpicture}% |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
847 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
848 \newcommand{\topproof}[1]{% |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
849 ##1 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
850 \bottomAlignProof |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
851 \DisplayProof |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
852 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
853 \newcommand{\capt}[1]{\vspace{-2em}##1} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
854 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
855 \begin{frame} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
856 \frametitle{Natürliches Schließen} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
857 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
858 \begin{definition}[Ersetzung] |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
859 Sei $\G$ eine Formel und $a$ eine Konstante.\\ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
860 Mit \structure{$\G[x/a]$} bezeichnen wir die Formel die man erhält, wenn man alle \alert{freien} Vorkommnisse von \structure{$x$} in \structure{$\G$} durch \structure{$a$} \structure{ersetzt}. |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
861 \end{definition} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
862 \vfill |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
863 \tabulinesep=4pt |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
864 \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
865 & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
866 \capt{$\exists$} & |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
867 \topproof{ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
868 \AxiomC{$\F[x/a]$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
869 \RightLabel{\scriptsize $+\exists$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
870 \UnaryInfC{$\exists x. \F$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
871 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
872 & |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
873 \topproof{ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
874 \AxiomC{$\exists x. \F$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
875 \AxiomC{\subproof{$a. \F[x/a]$}{$\K$}} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
876 \RightLabel{\scriptsize $-\exists$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
877 \BinaryInfC{$\K$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
878 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
879 \\ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
880 \capt{$\forall$} & |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
881 \topproof{ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
882 \AxiomC{\subproof{$a$}{$\F[x/a]$}} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
883 \RightLabel{\scriptsize $+\forall$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
884 \UnaryInfC{$\forall x. \F$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
885 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
886 & |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
887 \topproof{ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
888 \AxiomC{$\forall x. \F$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
889 \RightLabel{\scriptsize $-\forall$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
890 \UnaryInfC{$\F[x/a]$} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
891 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
892 \end{tabu} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
893 \begin{itemize} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
894 \vfill |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
895 \item Man muss ein \alert{unbenutztes $a$} in $+\forall$ und $-\exists$ wählen |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
896 \end{itemize} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
897 \end{frame} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
898 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
899 } |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
900 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
901 \defineUnit{induktion}{% |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
902 \begin{frame} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
903 \frametitle{Vollständige Induktion} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
904 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
905 \begin{block}{Vollständige Induktion} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
906 Die \structure{vollständige Induktion} ist eine Beweistechnik, um zu zeigen, dass alle natürlichen Zahlen ein Prädikat $P$ erfüllen. |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
907 \[ \alert{\forall n \in \N_0. P(x)} \] |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
908 Ein solcher Beweis besteht aus |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
909 \begin{description}[Induktionsanfang\quad] |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
910 \item[Induktionsanfang] Man zeigt, dass $P(0)$ gilt. |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
911 \item[Induktionsschritt] Man zeigt für ein beliebiges $k$, dass\\ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
912 wenn $P(k)$ gilt (\structure{Induktionshypothese}),\\ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
913 dann auch $P(k+1)$. |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
914 \end{description} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
915 Zusammen beweisen die Teile, dass das Prädikat für alle $n \in \N_0$ gilt.\\ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
916 \vspace{1em} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
917 In Prädikatenlogik formuliert gilt in $\N_0$ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
918 \begin{align} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
919 \structure{ P(0) \wedge \forall k . \left( P(k) \rightarrow P(k+1) \right)} &\rightarrow \alert{\forall n. P(n)} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
920 \end{align} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
921 \end{block} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
922 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
923 \vfill |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
924 |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
925 \begin{itemize} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
926 \item Kann verallgemeinert werden, z.B. auf $\Z$ |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
927 \item Aber nicht auf $\R$ (Warum?) |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
928 \end{itemize} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
929 \end{frame} |
|
010d8f7fa899
seventh slides and sheet
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
32
diff
changeset
|
930 } |
|
37
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
931 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
932 \defineUnit{wohlfundierteinduktion}{% |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
933 \begin{frame} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
934 \frametitle{Wohlfundierte Relation} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
935 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
936 \begin{definition}[Wohlfundierte Relation] |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
937 Eine Relation $\prec \subseteq A \times A$ heißt \structure{wohlfundiert}, wenn keine \alert{unendlichen Folgen} von Elementen $a_1, a_2, a_3, \dots \in A$ existieren, sodass |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
938 \[a_1 \succ a_2 \succ a_3 \succ \dots\] |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
939 Jede Kette hat ein \structure{unteres Ende}. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
940 \end{definition} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
941 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
942 \vfill |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
943 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
944 \begin{example}[] |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
945 \begin{itemize} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
946 \item $\prec_1 \defeq \left\{ (a, b) \in \N^2 \mid a < b \right\}$ ist wohlfundiert. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
947 \item $\prec_2 \defeq \left\{ (a, b) \in \N^2 \mid a > b \right\}$ ist \alert{nicht} wohlfundiert. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
948 \item $\prec_3 \defeq \left\{ (a, b) \in \Z^2 \mid a < b \right\}$ ist \alert{nicht} wohlfundiert. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
949 \item $\prec_4 \defeq \left\{ (a, b) \in \N^2 \mid \exists x . x \text{ teilt } a \wedge x \text{ teilt } b \right\}$ ist \alert{nicht} wohlfundiert. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
950 \smallskip |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
951 \item $\prec_5 \defeq \emptyset$ ist wohlfundiert. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
952 \end{itemize} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
953 \end{example} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
954 \end{frame} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
955 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
956 \begin{frame} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
957 \frametitle{Wohlfundierte Induktion} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
958 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
959 \begin{block}{Wohlfundierte Induktion} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
960 Die \structure{wohlfundierte Induktion} verallgemeinert die vollständige Induktion.\\ |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
961 Um für eine Menge $A$ mit wohlfundierter Relation $\prec$ ein Prädikat |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
962 \[ \alert{\forall a \in A.\; P(a)} \] |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
963 zu zeigen, beweist man |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
964 \begin{description}[Induktionsanfang\quad] |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
965 \item[Induktionsanfang] Man zeigt, dass für alle bezüglich $\prec$ \structure{minimalen} Elemente $m_i$ das Prädikat gilt. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
966 \item[Induktionsschritt] Man zeigt, dass wenn \structure{alle kleineren} Elemente als $n$ das Prädikat erfüllen, so auch $n$. |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
967 \end{description} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
968 \vspace{1em} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
969 In Prädikatenlogik formuliert gilt |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
970 \begin{align} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
971 \structure{\forall a \in A. \left( \forall b \prec a.\; P(b) \rightarrow P(a) \right)} \quad\text{gdw.}\quad \alert{\forall a \in A.\; P(a)} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
972 \end{align} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
973 \end{block} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
974 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
975 \vfill |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
976 |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
977 \begin{itemize} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
978 \item Wo ist der Induktionsanfang? |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
979 \end{itemize} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
980 \end{frame} |
|
3de775b67d8c
eigth sheet and notes
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
35
diff
changeset
|
981 } |