# HG changeset patch # User Markus Kaiser # Date 1384814977 -3600 # Node ID dc6b569c57c8038bc7f429366bbfb8c30d4dcc7b # Parent 03a0cf37ddaa12cc791781aacd7727e9b2554aac fifth slides and sheet diff -r 03a0cf37ddaa -r dc6b569c57c8 ds13-05.pdf Binary file ds13-05.pdf has changed diff -r 03a0cf37ddaa -r dc6b569c57c8 notes/tex/logic.tex --- 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} +} +} diff -r 03a0cf37ddaa -r dc6b569c57c8 notes/tex/preamble.tex --- 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}} diff -r 03a0cf37ddaa -r dc6b569c57c8 notes/tex/ue05_notes.tex --- /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} diff -r 03a0cf37ddaa -r dc6b569c57c8 notes/ue05_notes.pdf Binary file notes/ue05_notes.pdf has changed