# HG changeset patch
# User Markus Kaiser <markus.kaiser@in.tum.de>
# Date 1386023765 -3600
# Node ID 010d8f7fa899de91d946102dbc0be3ae562727b9
# Parent  18990097641350c338cbee740593fdc1ee647a99
seventh slides and sheet

diff -r 189900976413 -r 010d8f7fa899 ds13-07.pdf
Binary file ds13-07.pdf has changed
diff -r 189900976413 -r 010d8f7fa899 notes/tex/logic.tex
--- a/notes/tex/logic.tex	Mon Dec 02 23:35:45 2013 +0100
+++ b/notes/tex/logic.tex	Mon Dec 02 23:36:05 2013 +0100
@@ -857,3 +857,103 @@
     \end{definition}
 \end{frame}
 }
+
+\defineUnit{natuerlichesschliessenquantoren}{%
+{
+    \newcommand{\F}{\tau}
+    \newcommand{\G}{\varphi}
+    \newcommand{\K}{\chi}
+    \newcommand{\subproof}[2]{%
+        \begin{tikzpicture}[y=.9em]
+            \path
+            (0, 0) node (a) {##1}
+            ++(0, -1) node (b) {$\vdots$}
+            ++(0, -1) node[below] (c) {##2};
+            \node[fit=(a)(b)(c), draw, inner sep=1pt] {};
+        \end{tikzpicture}%
+    }
+    \newcommand{\topproof}[1]{%
+        ##1
+        \bottomAlignProof
+        \DisplayProof
+    }
+    \newcommand{\capt}[1]{\vspace{-2em}##1}
+
+    \begin{frame}
+        \frametitle{Natürliches Schließen}
+        \setbeamercovered{dynamic}
+
+        \begin{definition}[Ersetzung]
+            Sei $\G$ eine Formel und $a$ eine Konstante.\\
+            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}.
+        \end{definition}
+        \vfill
+        \tabulinesep=4pt
+        \begin{tabu} to \textwidth {X[c,m,.5]|[1pt]X[c,b,5]X[c,b,5]}
+            & \structure{Introduktion} & \structure{Elimination}\\\tabucline[1pt]{-}
+            \capt{$\exists$} &
+                \topproof{
+                    \AxiomC{$\F[x/a]$}
+                    \RightLabel{\scriptsize $+\exists$}
+                    \UnaryInfC{$\exists x. \F$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\exists x. \F$}
+                    \AxiomC{\subproof{$a. \F[x/a]$}{$\K$}}
+                    \RightLabel{\scriptsize $-\exists$}
+                    \BinaryInfC{$\K$}
+                }
+            \\
+            \capt{$\forall$} &
+                \topproof{
+                    \AxiomC{\subproof{$a$}{$\F[x/a]$}}
+                    \RightLabel{\scriptsize $+\forall$}
+                    \UnaryInfC{$\forall x. \F$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\forall x. \F$}
+                    \RightLabel{\scriptsize $-\forall$}
+                    \UnaryInfC{$\F[x/a]$}
+                }
+        \end{tabu}
+        \begin{itemize}
+            \vfill
+            \item Man muss ein \alert{unbenutztes $a$} in $+\forall$ und $-\exists$ wählen
+        \end{itemize}
+    \end{frame}
+}
+}
+
+\defineUnit{induktion}{%
+\begin{frame}
+    \frametitle{Vollständige Induktion}
+    \setbeamercovered{dynamic}
+
+    \begin{block}{Vollständige Induktion}
+        Die \structure{vollständige Induktion} ist eine Beweistechnik, um zu zeigen, dass alle natürlichen Zahlen ein Prädikat $P$ erfüllen.
+        \[ \alert{\forall n \in \N_0. P(x)} \]
+        Ein solcher Beweis besteht aus
+        \begin{description}[Induktionsanfang\quad]
+            \item[Induktionsanfang] Man zeigt, dass $P(0)$ gilt.
+            \item[Induktionsschritt] Man zeigt für ein beliebiges $k$, dass\\
+                wenn $P(k)$ gilt (\structure{Induktionshypothese}),\\
+                dann auch $P(k+1)$.
+        \end{description}
+        Zusammen beweisen die Teile, dass das Prädikat für alle $n \in \N_0$ gilt.\\
+        \vspace{1em}
+        In Prädikatenlogik formuliert gilt in $\N_0$
+        \begin{align}
+            \structure{ P(0) \wedge \forall k . \left( P(k) \rightarrow P(k+1) \right)} &\rightarrow \alert{\forall n. P(n)}
+        \end{align}
+    \end{block}
+
+    \vfill
+
+    \begin{itemize}
+        \item Kann verallgemeinert werden, z.B. auf $\Z$
+        \item Aber nicht auf $\R$ (Warum?)
+    \end{itemize}
+\end{frame}
+}
diff -r 189900976413 -r 010d8f7fa899 notes/tex/ue07_notes.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/notes/tex/ue07_notes.tex	Mon Dec 02 23:36:05 2013 +0100
@@ -0,0 +1,13 @@
+\input{preamble.tex}
+\input{frames.tex}
+
+\title{Übung 7: Prädikatenlogik II}
+\subtitle{Diskrete Strukturen im Wintersemester 2013/2014}
+\author{\href{mailto:markus.kaiser@in.tum.de}{Markus Kaiser}}
+
+\begin{document}
+\showUnit{titel}
+\showUnit{natuerlichesschliessen}
+\showUnit{natuerlichesschliessenquantoren}
+\showUnit{induktion}
+\end{document}
diff -r 189900976413 -r 010d8f7fa899 notes/ue07_notes.pdf
Binary file notes/ue07_notes.pdf has changed