Mercurial > 13ws.ds
view notes/tex/logic.tex @ 22:dc6b569c57c8
fifth slides and sheet
author | Markus Kaiser <markus.kaiser@in.tum.de> |
---|---|
date | Mon, 18 Nov 2013 23:49:37 +0100 |
parents | d9b98c2ba5ac |
children | 41623ba498a9 |
line wrap: on
line source
\defineUnit{aussagenlogiksyntax}{% \begin{frame}[c] \frametitle{Syntax der Aussagenlogik} \setbeamercovered{dynamic} \begin{definition}[Syntax der Aussagenlogik] Aussagenlogische \structure{Formeln} bestehen aus Konstanten, Variablen und Operatoren. Die Menge \structure{$\mathcal{F}$} aller Formeln ist induktiv definiert. \begin{itemize} \item $\mathrm{false} = 0 \in \mathcal{F},\quad \mathrm{true} = 1 \in \mathcal{F}$\hfill(\alert{Konstanten}) \item $V = \left\{ a, b, c,\ldots \right\} \subseteq \mathcal{F}$\hfill(\alert{Variablen})\\ \medskip \item Ist $A \in \mathcal{F}$ eine aussagenlogische Formel, dann auch \begin{align} \neg A &\in \mathcal{F}\tag{\alert{Negation}}\\ \intertext{\item Sind $A, B \in \mathcal{F}$ aussagenlogische Formeln, dann auch} (A \wedge B)&\in \mathcal{F}\tag{\alert{Konjunktion}}\\ (A \vee B)&\in \mathcal{F}\tag{\alert{Disjunktion}}\\ (A \rightarrow B)&\in \mathcal{F}\tag{\alert{Implikation}} \end{align} \end{itemize} Alle Formeln lassen sich so konstruieren. \end{definition} \end{frame} \begin{frame} \frametitle{Operatorenbindung} \setbeamercovered{dynamic} \begin{definition}[Bindungsregeln] Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist \[ \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \] Die Implikation ist \structure{rechtsassoziativ} \[ 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) \] \end{definition} \begin{itemize} \item Üblicherweise klammert man $\wedge$ und $\vee$ \[ (a \wedge b) \vee c \text{\quad statt\quad} a \wedge b \vee c \] \end{itemize} \begin{example}[] \begin{itemize} \item $\neg a \wedge b$\quad steht für \quad$ \left( \left( \neg a \right) \wedge b \right)$ \item $a \wedge b \rightarrow c \vee \neg d$\quad steht für \quad$((a \wedge b) \rightarrow (c \vee \left( \neg d \right)))$ \end{itemize} \end{example} \end{frame} \begin{frame} \frametitle{Syntaxbaum} \setbeamercovered{dynamic} \begin{block}{Syntaxbaum} \structure{Syntaxbäume} visualisieren in welcher Reihenfolge die Regeln zur induktiven Definition angewandt werden müssen, um eine Formel zu erzeugen. \end{block} \begin{example}[] Sei $F \defeq a \wedge b \rightarrow c \vee \neg d$ dann ist der dazu passende Syntaxbaum \centering \begin{tikzpicture}[grow=down, level distance = 33] \tikzstyle{every node} = [] \tikzstyle{op} = [pretty] \tikzstyle{var} = [pretty, rectangle] \tikzstyle{edge from parent} = [edge] \tikzstyle{level 1} = [sibling distance = 80] \tikzstyle{level 2} = [sibling distance = 40] \node[op] {$\rightarrow$} child { node[op] {$\wedge$} edge from parent child { node[var] {$a$} edge from parent } child { node[var] {$b$} edge from parent } } child { node[op] {$\vee$} edge from parent child { node[var] {$c$} edge from parent } child { node[op] {$\neg$} edge from parent child { node[var] {$d$} edge from parent } } }; \end{tikzpicture} \end{example} \end{frame} } \defineUnit{aussagenlogiksemantik}{% \begin{frame} \frametitle{Belegung} \setbeamercovered{dynamic} \begin{definition}[Belegung] Eine passende \structure{Belegung} $\beta$ zu einer Formel $F$ ordnet jeder Variable in $V$ einen Wahrheitswert aus $\left\{ 0, 1 \right\}$ zu. Es ist \[ \beta : V \to \left\{ 0, 1 \right\} \] \end{definition} \begin{itemize} \item Belegungen formalisieren Einsetzen \item Für $n$ Variablen existieren $2^n$ Belegungen \end{itemize} \begin{example}[] Sei $F \defeq \neg \left( a \wedge b \right)$ mit $V = \left\{ a, b \right\}$ und \begin{align} \beta : \left\{ a, b \right\} &\to \left\{ 0, 1 \right\}\\ a &\mapsto 1\\ b &\mapsto 0 \end{align} Dann ist $\beta$ eine zu $F$ passende \structure{Belegung}. \end{example} \end{frame} \begin{frame} \frametitle{Semantik der Aussagenlogik} \setbeamercovered{dynamic} \begin{definition}[Semantik einer Formel] Die \structure{Semantik} $[F]$ einer aussagenlogischen Formel $F$ ist eine Funktion, die jeder passenden Belegung $\beta$ einen Wahrheitswert zuordnet.\\ Sei $\mathcal{B} = \left\{ \beta_0, \beta_1, \ldots \right\}$ die Menge aller Belegungen zu $F$. Dann ist \[[F] : \mathcal{B} \to \left\{ 0, 1 \right\}\] \end{definition} \begin{itemize} \item Die Semantik löst eingesetzte Formeln auf \item Wird anhand der induktiven Syntax definiert \item Es gibt \alert{syntaktisch verschiedene} Formeln gleicher \structure{Semantik} \end{itemize} \begin{example}[] Sei $F \defeq \left( G \rightarrow H \right)$ mit $G, H$ Formeln. Dann ist \[ [F](\beta) = \begin{cases} 0 & \text{falls } [G](\beta) = 1 \text{ und } [H](\beta) = 0 \\ 1 & \text{sonst} \end{cases}\] \end{example} \end{frame} \begin{frame} \frametitle{Wahrheitstabelle} \setbeamercovered{dynamic} \begin{block}{Wahrheitstabelle} 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. \end{block} \begin{example}[] Sei $F \defeq a \vee b \rightarrow \neg c \wedge b$. Die zu $[F]$ gehörige Wahrheitstabelle ist \begin{center} \begin{tabu} to .5\textwidth {cccX|[1.2pt]Xccccc} a & b & c & & & $a \vee b$ & $\rightarrow$ & $\neg c$ & $\wedge$ & $b$ \\ \tabucline[1.2pt]{-} 0 & 0 & 0 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{0} & \\ 0 & 0 & 1 & & & \onslide<2->{0} & \onslide<3->{\structure{1}} & \onslide<2->{0} & \onslide<2->{0} & \\ 0 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ 0 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ 1 & 0 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{1} & \onslide<2->{0} & \\ 1 & 0 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ 1 & 1 & 0 & & & \onslide<2->{1} & \onslide<3->{\structure{1}} & \onslide<2->{1} & \onslide<2->{1} & \\ 1 & 1 & 1 & & & \onslide<2->{1} & \onslide<3->{\structure{0}} & \onslide<2->{0} & \onslide<2->{0} & \\ \end{tabu} \end{center} \end{example} \end{frame} \begin{frame} \frametitle{Äquivalente Formeln} \setbeamercovered{dynamic} \begin{definition}[Äquivalente Formeln] Man nennt zwei Formeln \structure{äquivalent}, wenn sie dieselbe Semantik besitzen.\\ Seien $F, G$ Formeln mit Belegungen $\mathcal{B} = \mathcal{B}_F = \mathcal{B}_G$. $F$ und $G$ sind äquivalent wenn \[ \forall \beta \in \mathcal{B}. [F](\beta) = [G](\beta) \] Man schreibt \structure{$F \equiv G$} oder \structure{$F \leftrightarrow G$}. \end{definition} \begin{example}[] Für $F \defeq a \rightarrow b$ und $G \defeq \neg a \vee b$ gilt $F \equiv G$. \begin{center} \begin{tabu} to .4\textwidth {cc|[1.2pt]XcX||Xccc} a & b & & $a \Rightarrow b$ & & & $\neg a$ & $\vee$ & $b$ \\ \tabucline[1.2pt]{-} 0 & 0 & & \structure{1} & & & 1 & \structure{1} \\ 0 & 1 & & \structure{1} & & & 1 & \structure{1} \\ 1 & 0 & & \structure{0} & & & 0 & \structure{0} \\ 1 & 1 & & \structure{1} & & & 0 & \structure{1} \\ \end{tabu} \end{center} \end{example} \end{frame} \begin{frame} \frametitle{Eigenschaften von Formeln} \setbeamercovered{dynamic} \begin{block}{Eigenschaften aussagenlogischer Formeln} Sei $F$ eine aussagenlogische Formel mit Variablen $V$ und der Menge der passenden Belegungen $\mathcal{B}$. Man nennt F \begin{description}[\quad unerfüllbar] \item[erfüllbar] $\exists \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ kann wahr sein) \item[unerfüllbar] $\forall \beta \in \mathcal{B}. [F](\beta) = 0$\hfill($F$ ist nie wahr) \item[gültig] $\forall \beta \in \mathcal{B}. [F](\beta) = 1$\hfill($F$ ist immer wahr) \end{description} \end{block} \begin{itemize} \item Eine unerfüllbare Formel nennt man \structure{Widerspruch} \item Eine gültige Formel nennt man \structure{Tautologie} \end{itemize} \end{frame} } \defineUnit{aussagenlogikaequivalenzen}{% { \newcommand{\true}{1} \newcommand{\false}{0} \newcommand{\spc}{\hspace{3em}} \newcommand{\F}{F} \newcommand{\G}{G} \newcommand{\K}{H} \begin{frame} \frametitle{Äquivalenzregeln} \setbeamercovered{dynamic} \begin{description}[Triviale Kontradiktion\quad] \item[Identität] $\F \wedge \true \equiv \F \spc \F \vee \false \equiv \F$ \item[Dominanz] $\F \vee \true \equiv \true \spc \F \wedge \false \equiv \false$ \item[Idempotenz] $\F \vee \F \equiv \F \spc \F \wedge \F \equiv \F$ \item[Doppelte Negation] $\neg \neg \F \equiv \F$ \item[Triviale Tautologie] $\F \vee \neg \F \equiv \true$ \item[Triviale Kontradiktion] $\F \wedge \neg \F \equiv \false$ \bigskip \item[Kommutativität] $\F \vee \G \equiv \G \vee \F$\\ $\F \wedge \G \equiv \G \wedge \F$ \item[Assoziativität] $(\F \vee \G) \vee \K \equiv \F \vee (\G \vee \K)$\\ $(\F \wedge \G) \wedge \K \equiv \F \wedge (\G \wedge \K)$ \item[Distributivität] $\F \vee (\G \wedge \K) \equiv (\F \vee \G) \wedge (\F \vee \K)$\\ $\F \wedge (\G \vee \K) \equiv (\F \wedge \G) \vee (\F \wedge \K)$ \item[De Morgan] $\neg(\F \wedge \G) \equiv \neg \F \vee \neg \G$\\ $\neg(\F \vee \G) \equiv \neg\F \wedge \neg\G$ \bigskip \item[Implikation] $\F \rightarrow \G \equiv \neg \F \vee \G$ \item[Bikonditional] $\F \leftrightarrow \G \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F)$ \end{description} \end{frame} %\begin{frame} %\frametitle{Äquivalenzregeln} %\setbeamercovered{dynamic} %\vspace{-2em} %\begin{align} %\F \wedge \true &\equiv \F \spc \F \vee \false \equiv \F \tag{\structure{Identität}}\\ %\F \vee \true &\equiv \true \spc \F \wedge \false \equiv \false \tag{\structure{Dominanz}}\\ %\F \vee \F &\equiv \F \spc \F \wedge \F \equiv \F \tag{\structure{Idempotenz}}\\ %\neg \neg \F &\equiv \F \tag{\structure{Doppelte Negation}}\\ %\F \vee \neg \F &\equiv \true \tag{\structure{Triviale Tautologie}}\\ %\F \wedge \neg \F &\equiv \false \tag{\structure{Triviale Kontradiktion}}\\ %\bigskip %\F \vee \G &\equiv \G \vee \F \tag{\structure{Kommutativität}}\\ %\F \wedge \G &\equiv \G \wedge \F\\ %(\F \vee \G) \vee \K &\equiv \F \vee (\G \vee \K) \tag{\structure{Assoziativität}}\\ %(\F \wedge \G) \wedge \K &\equiv \F \wedge (\G \wedge \K)\\ %\F \vee (\G \wedge \K) &\equiv (\F \vee \G) \wedge (\F \vee \K) \tag{\structure{Distributivität}}\\ %\F \wedge (\G \vee \K) &\equiv (\F \wedge \G) \vee (\F \wedge \K)\\ %\neg(\F \wedge \G) &\equiv \neg \F \vee \neg \G \tag{\structure{De Morgan}}\\ %\neg(\F \vee \G) &\equiv \neg\F \wedge \neg\G\\ %\bigskip %\F \rightarrow \G &\equiv \neg \F \vee \G \tag{\structure{Implikation}}\\ %\F \leftrightarrow \G &\equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \tag{\structure{Bikonditional}}\\ %\end{align} %\end{frame} } } \defineUnit{aussagenlogiknormalformen}{% \begin{frame}[c] \frametitle{Literale und Klauseln} \setbeamercovered{dynamic} \begin{definition}[Literal] Ein \structure{Literal} ist eine Variable $v \in V$ oder die Negation $\neg v$ einer Variable. \end{definition} \begin{definition}[Klausel] Eine \structure{Klausel} verknüpft mehrere Literale mit einem assoziativen Operator. \end{definition} \vfill \begin{example}[] Seien $a, \neg b, c$ Literale. Dann sind \begin{itemize} \item $a \wedge \neg b \wedge c$ \item $a \vee \neg b \vee c$ \end{itemize} Klauseln. \end{example} \end{frame} { \newcommand{\klausel}[2]{\underbracket{(##2)}_{\text{##1-Klausel}}} \begin{frame} \frametitle{DNF} \setbeamercovered{dynamic} \begin{definition}[Disjunktive Normalform] Eine \structure{DNF-Klausel} ist eine Konjunktion von Literalen $L_i$.\\ Eine Formel $F$, ist in \structure{Disjunktiver Normalform}, wenn sie eine Disjunktion von DNF-Klauseln ist. \[ F \defeq \bigvee \bigwedge_i L_i \] \end{definition} \begin{itemize} \item Ausnahme: $\textrm{false}$ ist auch in DNF \end{itemize} \begin{example}[] $F$ ist in DNF. \[ 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} \] \end{example} \end{frame} \begin{frame} \frametitle{KNF} \setbeamercovered{dynamic} \begin{definition}[Konjunktive Normalform] Eine \structure{KNF-Klausel} ist eine Disjunktion von Literalen $L_i$.\\ Eine Formel $F$, ist in \structure{Konjunktiver Normalform}, wenn sie eine Konjunktion von KNF-Klauseln ist. \[ F \defeq \bigwedge \bigvee_i L_i \] \end{definition} \begin{itemize} \item Ausnahme: $\textrm{true}$ ist auch in KNF \end{itemize} \begin{example}[] $F$ ist in KNF. \[ 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} \] \end{example} \end{frame} } \begin{frame} \frametitle{Konstruktion der NF} \setbeamercovered{dynamic} \begin{itemize} \item \structure{Jede} nicht-triviale Formel ist in DNF und KNF umwandelbar \item Durch Äquivalenzumformungen berechenbar (exponentiell groß!) \item Oder: Konstruktion mit Wahrheitstabellen \end{itemize} \vfill \begin{block}{Normalformen aus Wahrheitstabellen} Gegeben eine Formel $F$ und ihre Wahrheitstabelle \begin{itemize} \item DNF \begin{enumerate} \item Betrachte Zeilen mit Eintrag \structure{$1$} \item Bilde \structure{Konjunktion} aus der \structure{Belegung} \item Bilde \structure{Disjunktion} aller erhaltenen Klauseln \end{enumerate} \bigskip \item KNF \begin{enumerate} \item Betrachte Zeilen mit Eintrag \alert{$0$} \item Bilde \alert{Disjunktion} aus der \alert{Negation} der Belegung \item Bilde \alert{Konjunktion} aller erhaltenen Klauseln \end{enumerate} \end{itemize} \end{block} \end{frame} { \newcommand{\klausel}[4]{(##2 a ##1 ##3 b ##1 ##4 c)} \begin{frame} \frametitle{Konstruktion der NF} \setbeamercovered{dynamic} \begin{example}[] Gegeben eine Formel $F$ mit folgender Semantik \begin{center} \begin{tabu} to .4\textwidth {ccc|[1.2pt]c} a & b & c & $F$ \\ \tabucline[1.2pt]{-} 0 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 1 & 1 & 1 \\ 1 & 0 & 0 & 1 \\ 1 & 0 & 1 & 1 \\ 1 & 1 & 0 & 1 \\ 1 & 1 & 1 & 0 \end{tabu} \end{center} $F$ dargestellt in \begin{itemize} \item DNF $\hfill\klausel{\wedge}{\neg}{}{} \vee (a \wedge \neg b) \vee \klausel{\wedge}{}{}{\neg}\hfill$ \medskip \item KNF $\hfill(a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}\hfill$ \end{itemize} \end{example} \end{frame} \begin{frame} \frametitle{Mengendarstellung der KNF} \setbeamercovered{dynamic} \begin{block}{Mengendarstellung der KNF} Eine Formel $F = \bigwedge \bigvee L_i$ in \structure{KNF} kann in einer \structure{Mengendarstellung} repräsentiert werden. \begin{itemize} \item Klauseln werden durch Mengen von Literalen dargestellt \[\left\{ a, \neg b, c \right\} \text{ steht für } (a \vee \neg b \vee c)\] \item KNF-Formeln sind Mengen von Klauseln \[ \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) \] \item $\emptyset$ steht für \textrm{true}, $\left\{ \emptyset \right\}$ für \textrm{false} \end{itemize} \end{block} \begin{example}[] Gegeben $F \defeq (a \vee b) \wedge \klausel{\vee}{\neg}{}{\neg} \wedge \klausel{\vee}{\neg}{\neg}{\neg}$ in KNF. \[ \left\{ \left\{ a, b \right\}, \left\{ \neg a, b, \neg c \right\}, \left\{ \neg a, \neg b, \neg c \right\} \right\}\] \end{example} \end{frame} } } \defineUnit{DPLL}{% \begin{frame} \frametitle{KNF aus Syntaxbaum} \setbeamercovered{dynamic} \begin{block}{Idee} Erzeuge die KNF aus dem Syntaxbaum \begin{enumerate} \item<1-> Weise jedem \structure{inneren Knoten} eine Variable zu \item<1,3-> Variablen sind \structure{abhängig} von ihren Kindern \item<1,4-> Berechne \structure{kleine} KNFs und führe diese \structure{zusammen} \end{enumerate} \end{block} \begin{columns}[T] \begin{column}{.7\textwidth} % FIXME: onlys around A_\vee needed for "correct" fadein \begin{align} (x \wedge y) \vee z \uncover<3->{\equiv &\hphantom{{}\wedge {}}\only<3->{A_\vee}\\ &\structure{\wedge (A_\vee \leftrightarrow A_\wedge \vee z)}\\ &\alert{\wedge (A_\wedge \leftrightarrow x \wedge y)}\\} \uncover<4->{\equiv &\hphantom{{}\wedge {}}\only<4->{A_\vee}\\ &\structure{\wedge (A_\vee \vee \neg A_\wedge) \wedge (A_\vee \vee \neg z)}\\ &\qquad\structure{\wedge (\neg A_\vee \vee A_\wedge \vee z)}\\ &\alert{\wedge (\neg A_\wedge \vee x) \wedge (\neg A_\wedge \vee y)} \\ &\qquad\alert{\wedge(A_\wedge \vee \neg x \vee \neg y)}} \end{align} \end{column} \begin{column}{.3\textwidth} \begin{tikzpicture}[grow=down, level distance = 33] \tikzstyle{op} = [pretty] \tikzstyle{var} = [pretty, rectangle] \tikzstyle{edge from parent} = [edge] \tikzstyle{level 1} = [sibling distance = 50] \tikzstyle{level 2} = [sibling distance = 30] \node at (0, 0) {}; \node[op] at (0, -1) {\alt<1>{$\vee$}{$A_\vee$}} child { node[op] {\alt<1>{$\wedge$}{$A_\wedge$}} edge from parent child { node[var] {$x$} edge from parent } child { node[var] {$y$} edge from parent } } child { node[var] {$z$} }; \end{tikzpicture} \end{column} \end{columns} \end{frame} \begin{frame} \frametitle{DPLL} \setbeamercovered{dynamic} \begin{definition}[DPLL-Belegung] Sei $F$ eine Formel in KNF und $p$ eine Variable von $F$.\\ Dann bezeichnet \structure{$F[p\backslash\mathrm{true}]$} die Formel, die entsteht, wenn jedes Vorkommnis von $p$ in F durch $\mathrm{true}$ ersetzt und vereinfacht wird. \end{definition} \begin{block}{DPLL} Gegeben eine Formel $F$ in KNF \begin{itemize} \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$ \item Prüfe ob $F[p\backslash\mathrm{true}]$ oder $F[p\backslash\mathrm{false}]$ erfüllbar \end{enumerate} \end{itemize} \end{block} \begin{itemize} \item Schlaue Wahl der Variable beschleunigt Ausführung \item Wähle Variablen die einzeln stehen (\structure{One-Literal-Rule}) \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} } }