changeset 22:dc6b569c57c8

fifth slides and sheet
author Markus Kaiser <markus.kaiser@in.tum.de>
date Mon, 18 Nov 2013 23:49:37 +0100
parents 03a0cf37ddaa
children 41623ba498a9
files ds13-05.pdf notes/tex/logic.tex notes/tex/preamble.tex notes/tex/ue05_notes.tex notes/ue05_notes.pdf
diffstat 5 files changed, 253 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
Binary file ds13-05.pdf has changed
--- a/notes/tex/logic.tex	Mon Nov 18 15:20:06 2013 +0100
+++ b/notes/tex/logic.tex	Mon Nov 18 23:49:37 2013 +0100
@@ -497,8 +497,8 @@
     \begin{block}{DPLL}
         Gegeben eine Formel $F$ in KNF
         \begin{itemize}
-            \item Wenn $F = \mathrm{true}$ dann antworte \enquote{erfüllbar}
-            \item Wenn $F = \mathrm{false}$ dann antworte \enquote{unerfüllbar}
+            \item Wenn $F = \mathrm{true}$ dann antworte \structure{erfüllbar}
+            \item Wenn $F = \mathrm{false}$ dann antworte \structure{unerfüllbar}
             \item Sonst
                 \begin{enumerate}
                     \item Wähle eine Variable $p$ in $F$
@@ -512,3 +512,237 @@
     \end{itemize}
 \end{frame}
 }
+
+\defineUnit{resolution}{%
+\begin{frame}
+    \frametitle{Resolution}
+    \setbeamercovered{dynamic}
+
+    \begin{definition}[Resolvent]
+        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
+        \begin{align}
+            R &= \left( K_1 \setminus \left\{ L \right\} \right) \cup \left( K_2 \setminus \left\{ \neg L \right\} \right)
+        \end{align}
+    \end{definition}
+
+    \begin{block}{Resolution}
+        Gegeben eine Formel $F$ in KNF in Mengendarstellung.
+        \begin{algorithmic}
+            \While{$\square = \emptyset \not \in F$}
+                \State{$R \gets \text{Resolvent aus } F \text{ mit } R \not\in F$}
+                \If{$R$ existiert}
+                    \State{$F \gets F \cup R$}
+                \Else
+                    \State{\textbf{return} \structure{erfüllbar}}
+                \EndIf
+            \EndWhile
+            \State{\textbf{return} \structure{unerfüllbar}}
+        \end{algorithmic}
+    \end{block}
+\end{frame}
+}
+
+\defineUnit{natuerlichesschliessen}{%
+\begin{frame}
+    \frametitle{Kalküle}
+    \setbeamercovered{dynamic}
+
+    \begin{definition}[Kalkül]
+        Ein \structure{Logikkalkül} stellt \structure{Inferenzregeln} bereit, mit denen Formeln \alert{syntaktisch} umgeformt werden können.
+    \end{definition}
+
+    \begin{definition}[Folgerung]
+        $F$ \structure{folgt aus} $A$, wenn mit Hilfe der \alert{Semantik} der \alert{Aussagenlogik} $F$ unter der Annahme dass $A$ gilt zu $\mathrm{true}$ ausgewertet wird. Wir schreiben
+        \[ A \vDash F \]
+    \end{definition}
+
+    \begin{definition}[Ableitung]
+        $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
+        \[ A \vdash F \]
+    \end{definition}
+\end{frame}
+
+\begin{frame}
+    \frametitle{Eigenschaften von Kalkülen}
+    \setbeamercovered{dynamic}
+
+    \begin{block}{Eigenschaften von Kalkülen}
+        \begin{description}[\quad vollständig (complete)]
+            \item[korrekt (sound)] Es können \alert{nur} semantisch gültige Formeln abgeleitet werden.
+                \[ \text{Aus } A \vdash F \text{ folgt } A \vDash F \]
+            \item[vollständig (complete)] \alert{Alle} semantisch gültigen Formeln können abgeleitet werden.
+                \[ \text{Aus } A \vDash F \text{ folgt } A \vdash F \]
+        \end{description}
+    \end{block}
+
+    \begin{itemize}
+        \item Für uns nur korrekte vollständige Kalküle
+        \item Beispiel für die Aussagenlogik: \structure{Natürliches Schließen}
+            \medskip
+        \item Es gibt keine solchen Kalküle für die
+            \begin{itemize}
+                \item Prädikatenlogik
+                \item Arithmetik
+            \end{itemize}
+        \item Deshalb sind nicht alle Sätze der Mathematik beweisbar
+    \end{itemize}
+\end{frame}
+
+{
+    \newcommand{\F}{\phi}
+    \newcommand{\G}{\psi}
+    \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
+    }
+
+    \begin{frame}
+        \frametitle{Natürliches Schließen}
+        \setbeamercovered{dynamic}
+
+        \vspace{-4pt}
+        \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]{-}
+            $\wedge$ &
+                \topproof{
+                    \AxiomC{$\F$}
+                    \AxiomC{$\G$}
+                    \RightLabel{\scriptsize $+\wedge$}
+                    \BinaryInfC{$\F \wedge \G$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\F \wedge \G$}
+                    \RightLabel{\scriptsize $-\wedge_1$}
+                    \UnaryInfC{$\F$}
+                }
+                \quad
+                \topproof{
+                    \AxiomC{$\F \wedge \G$}
+                    \RightLabel{\scriptsize $-\wedge_2$}
+                    \UnaryInfC{$\G$}
+                }
+            \\
+            $\vee$ &
+                \topproof{
+                    \AxiomC{$\F$}
+                    \RightLabel{\scriptsize $+\vee_1$}
+                    \UnaryInfC{$\F \vee \G$}
+                }
+                \quad
+                \topproof{
+                    \AxiomC{$\G$}
+                    \RightLabel{\scriptsize $+\vee_2$}
+                    \UnaryInfC{$\F \vee \G$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\F \vee \G$}
+                    \AxiomC{\subproof{$\F$}{$\K$}}
+                    \AxiomC{\subproof{$\G$}{$\K$}}
+                    \RightLabel{\scriptsize $-\vee$}
+                    \TrinaryInfC{$\K$}
+                }
+            \\
+            $\rightarrow$ &
+                \topproof{
+                    \AxiomC{\subproof{$\F$}{$\G$}}
+                    \RightLabel{\scriptsize $+\rightarrow$}
+                    \UnaryInfC{$\F \rightarrow \G$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\F$}
+                    \AxiomC{$\F \rightarrow \G$}
+                    \RightLabel{\scriptsize $-\rightarrow$, MP}
+                    \BinaryInfC{$\G$}
+                }
+            \\
+            $\neg$ &
+                \topproof{
+                    \AxiomC{\subproof{$\F$}{$\bot$}}
+                    \RightLabel{\scriptsize $+\neg$}
+                    \UnaryInfC{$\neg \F$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\F$}
+                    \AxiomC{$\neg\F$}
+                    \RightLabel{\scriptsize $-\neg$}
+                    \UnaryInfC{$\bot$}
+                }
+        \end{tabu}
+    \end{frame}
+
+    \begin{frame}
+        \frametitle{Natürliches Schließen}
+        \setbeamercovered{dynamic}
+
+        \vspace{-4pt}
+        \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]{-}
+            $\bot$ &
+            &
+                \topproof{
+                    \AxiomC{$\bot$}
+                    \RightLabel{\scriptsize $-\bot$}
+                    \UnaryInfC{$\F$}
+                }
+            \\
+            $\neg\neg$ &
+                \topproof{
+                    \AxiomC{$\F$}
+                    \RightLabel{\scriptsize $+\neg\neg$}
+                    \UnaryInfC{$\neg\neg\F$}
+                }
+            &
+                \topproof{
+                    \AxiomC{$\neg\neg\F$}
+                    \RightLabel{\scriptsize $-\neg\neg$}
+                    \UnaryInfC{$\F$}
+                }
+        \end{tabu}
+        \begin{itemize}
+                \vfill
+            \item Praktische abgeleitete Regeln
+        \end{itemize}
+        \tabulinesep=10pt
+        \begin{tabu} to \textwidth {X[c,m,.5]X[c,b,5]X[c,b,5]}
+            &
+                \topproof{
+                    \AxiomC{ }
+                    \RightLabel{\scriptsize LEM}
+                    \UnaryInfC{$\F \vee \neg\F$}
+                }
+            &
+                \topproof{
+                    \AxiomC{\subproof{$\neg\F$}{$\bot$}}
+                    \RightLabel{\scriptsize $-\neg$, PBC}
+                    \UnaryInfC{$\F$}
+                }
+            \\
+            &
+            &
+                \topproof{
+                    \AxiomC{$\neg\G$}
+                    \AxiomC{$\F \rightarrow \G$}
+                    \RightLabel{\scriptsize MT}
+                    \BinaryInfC{$\neg\F$}
+                }
+        \end{tabu}
+    \end{frame}
+}
+}
--- a/notes/tex/preamble.tex	Mon Nov 18 15:20:06 2013 +0100
+++ b/notes/tex/preamble.tex	Mon Nov 18 23:49:37 2013 +0100
@@ -24,6 +24,7 @@
 \usetikzlibrary{shapes}
 \usetikzlibrary{positioning}
 \usetikzlibrary{chains}
+\usetikzlibrary{fit}
 
 \usepackage{amsmath}
 \usepackage{mathdots}
@@ -33,6 +34,10 @@
 \usepackage{csquotes}
 \usepackage{wasysym}
 
+\usepackage[noend]{algpseudocode}
+% Proof trees
+\usepackage{bussproofs}
+
 \usepackage{beamerthemeLEA2}
 
 \newcommand{\N}{\mathbb{N}}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/notes/tex/ue05_notes.tex	Mon Nov 18 23:49:37 2013 +0100
@@ -0,0 +1,12 @@
+\input{preamble.tex}
+\input{frames.tex}
+
+\title{Übung 5: Resolution \& Kalküle}
+\subtitle{Diskrete Strukturen im Wintersemester 2013/2014}
+\author{\href{mailto:markus.kaiser@in.tum.de}{Markus Kaiser}}
+
+\begin{document}
+\showUnit{titel}
+\showUnit{resolution}
+\showUnit{natuerlichesschliessen}
+\end{document}
Binary file notes/ue05_notes.pdf has changed