13ws.ds: notes/tex/logic.tex comparison

comparison 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

comparison

equal deleted inserted replaced

-:5734c1faf9cd
+:e65f4b1a6e32
 \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 $\false = 0 = \bot \in \mathcal{F},\quad \true = 1 = \top \in \mathcal{F}$\hfill(\alert{Konstanten})
 \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}
 \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}[]
 }
 \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}
 \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{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}[]
 \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) \]
 \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)
 \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$
 \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}}\\
 }
 \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}
 {
 \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{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{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
 {
 \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}
 \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
 }
 \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
 \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\true]$} die Formel, die entsteht, wenn jedes Vorkommnis von $p$ in F durch $\true$ ersetzt und vereinfacht wird.
 \end{definition}
 }
 \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)
 }
 \defineUnit{kalkuele}{%
 \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}
 \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 \]
 }
 \newcommand{\capt}[1]{\vspace{-1em}##1}
 \begin{frame}
 \frametitle{Natürliches Schließen}
-\setbeamercovered{dynamic}
 \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{$\wedge$} &
 \end{tabu}
 \end{frame}
 \begin{frame}
 \frametitle{Natürliches Schließen}
-\setbeamercovered{dynamic}
 \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{$\bot$} &
 \newcommand{\terms}{\mathcal{T}}
 \newcommand{\preds}{\mathcal{P}}
 \newcommand{\logic}{\mathcal{L}}
 \begin{frame}[c]
 \frametitle{Syntax der Prädikatenlogik}
-\setbeamercovered{dynamic}
 \begin{definition}[Term]
 Die Menge $\terms$ aller \structure{Terme} ist induktiv definiert.
 \begin{itemize}
 \item Jede Konstante ist in $\terms$
 \end{definition}
 \end{frame}
 \begin{frame}[c]
 \frametitle{Syntax der Prädikatenlogik}
-\setbeamercovered{dynamic}
 \begin{definition}[Syntax der Prädikatenlogik]
 Die Menge \structure{$\logic$} aller \structure{prädikatenlogischen Formeln} ist induktiv definiert.
 Seien $A, B\in \logic$, $t_i \in \terms$ und $P \in \preds$. Dann sind alle Formeln
 {
 \end{definition}
 \end{frame}
 \begin{frame}
 \frametitle{Operatorenbindung}
-\setbeamercovered{dynamic}
 \begin{definition}[Bindungsregeln]
 Die \structure{Bindungsstärke} der Operatoren in absteigender Reihenfolge ist
 \[ \forall \quad \exists \quad \neg \quad \wedge \quad \vee \quad \rightarrow \quad \leftrightarrow \]
 Die Implikation ist \structure{rechtsassoziativ}.
 }
 \defineUnit{praedikatenlogikstruktur}{%
 \begin{frame}[c]
 \frametitle{Struktur}
-\setbeamercovered{dynamic}
 \begin{definition}[Struktur]
 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$.
 \begin{itemize}
 \item Alle Terme werten zu einem Wert im \structure{Universum} $U_s$ aus
 }
 \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}
 }
 \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
 }
 \defineUnit{wohlfundierteinduktion}{%
 \begin{frame}
 \frametitle{Wohlfundierte Relation}
-\setbeamercovered{dynamic}
 \begin{definition}[Wohlfundierte Relation]
 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
 \[a_1 \succ a_2 \succ a_3 \succ \dots\]
 Jede Kette hat ein \structure{unteres Ende}.
 \end{example}
 \end{frame}
 \begin{frame}
 \frametitle{Wohlfundierte Induktion}
-\setbeamercovered{dynamic}
 \begin{block}{Wohlfundierte Induktion}
 Die \structure{wohlfundierte Induktion} verallgemeinert die vollständige Induktion.\\
 Um für eine Menge $A$ mit wohlfundierter Relation $\prec$ ein Prädikat
 \[ \alert{\forall a \in A.\; P(a)} \]

Mercurial > 13ws.ds

comparison notes/tex/logic.tex @ 45:e65f4b1a6e32