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

comparison notes/tex/logic.tex @ 26:4436f8006ebd

fix minor errors; sixth slides and sheet

author	Markus Kaiser <markus.kaiser@in.tum.de>
date	Mon, 25 Nov 2013 23:16:14 +0100
parents	140a0060e2f8
children	f639b478a28b

comparison

equal deleted inserted replaced

-:9d87018168eb
+:4436f8006ebd
 \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 $\false = 0 = \bot \in \mathcal{F},\quad \true = 1 = \top \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}}\\
 \end{frame}
 }
 \defineUnit{aussagenlogikaequivalenzen}{%
 {
-\newcommand{\true}{1}
+\newcommand{\spc}{\hfill}
-\newcommand{\false}{0}
-\newcommand{\spc}{\hspace{3em}}
 \newcommand{\F}{F}
 \newcommand{\G}{G}
 \newcommand{\K}{H}
 \begin{frame}
 $\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)$
+\item[Bikonditional] $\F \leftrightarrow \G \equiv \neg(\F \otimes \G) \left[ \equiv (\F \rightarrow \G) \wedge (\G \rightarrow \F) \right]$
 \end{description}
 \end{frame}
 %\begin{frame}
 %\frametitle{Äquivalenzregeln}
 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
+\item Ausnahme: $\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} \]
 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
+\item Ausnahme: $\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} \]
 \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}
+\item $\emptyset$ steht für $\true$, $\left\{ \emptyset \right\}$ für $\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\}\]
 \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.
+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}
 \begin{block}{DPLL}
 Gegeben eine Formel $F$ in KNF
 \begin{itemize}
-\item Wenn $F = \mathrm{true}$ dann antworte \structure{erfüllbar}
+\item Wenn $F = \true$ dann antworte \structure{erfüllbar}
-\item Wenn $F = \mathrm{false}$ dann antworte \structure{unerfüllbar}
+\item Wenn $F = \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
+\item Prüfe ob $F[p\backslash\true]$ oder $F[p\backslash\false]$ erfüllbar
 \end{enumerate}
 \end{itemize}
 \end{block}
 \begin{itemize}
 \item Schlaue Wahl der Variable beschleunigt Ausführung
 \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
+$F$ \structure{folgt aus} $A$, wenn mit Hilfe der \alert{Semantik} der \alert{Aussagenlogik} $F$ unter der Annahme dass $A$ gilt zu $\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
 }
 \end{tabu}
 \end{frame}
 }
 }
+\defineUnit{praedikatenlogiksyntax}{%
+{
+\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$
+\item Jede Variable ist in $\terms$
+\item Sind $f$ eine Funktion und $t_1, \dots, t_n$ Terme, dann auch
+\[ f(t_1, \dots, t_n) \]
+\end{itemize}
+Funktionen wandeln Terme in \alert{Terme} um. Wir beschreiben sie mit Kleinbuchstaben.
+\end{definition}
+\begin{definition}[Prädikat]
+\structure{Prädikate} $P$ wandeln Terme in \alert{Wahrheitswerte} um.
+Wir beschreiben sie mit Großbuchstaben.\\
+Die Menge $\preds$ enthält alle \structure{Prädikate}.
+\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
+{
+\setlength{\belowdisplayskip}{0pt}
+\setlength{\abovedisplayskip}{0pt}
+\begin{itemize}
+\item Grundbausteile
+\smallskip
+\begin{align}
+V = \left\{ a, b, \dots \right\} &\subseteq \logic\tag{\alert{Variablen}}\\
+P(t_1, \dots, t_n) &\in \logic\tag{\alert{Prädikate, Konstanten}}\\
+t_i = t_j &\in\logic\tag{\alert{Gleichheit}}\\
+\shortintertext{\item Verknüpfungen der Aussagenlogik}
+\neg A &\in \logic\tag{\alert{Negation}}\\
+(A \wedge B), (A \vee B)&\in \logic\tag{\alert{Konjunktion, Disjunktion}}\\
+(A \rightarrow B)&\in \logic\tag{\alert{Implikation}}\\
+\shortintertext{\item \structure{Quantoren}}
+\exists x. A &\in \logic\tag{\alert{Existenzquantor}}\\
+\forall x. A &\in \logic\tag{\alert{Allquantor}}\\
+\end{align}
+\end{itemize}
+}
+\vspace{-1.5em}
+\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}.
+\end{definition}
+\begin{itemize}
+\item Üblicherweise klammert man wieder $\wedge$ und $\vee$
+\item Genauso klammert man Quantoren
+\[ \left( \forall x. F \right) \rightarrow G \text{\quad statt\quad} \forall x. F \rightarrow G \]
+\vfill
+\item \alert{Achtung!} Äußere Quantoren werden öfter anders interpretiert
+\[ \forall x \forall y. F \wedge G \leftrightarrow H \]
+Bindet formal \alert{nur an das F}!
+\end{itemize}
+\end{frame}
+}
+}
+\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
+\item Die \structure{Interpretation} $I_s$ weist den Atomen der Formel Werte zu.\\
+Sie spezifiziert
+\begin{itemize}
+\item \alert{Variablen} $x$ mit
+{
+\setlength{\belowdisplayskip}{0pt}
+\setlength{\abovedisplayskip}{0pt}
+\begin{align}
+x_s \in {} &U_s\\
+\shortintertext{\item \alert{Konstanten} $a$ mit}
+a_s \in {} &U_s\\
+\shortintertext{\item \alert{k-stellige Prädikate} $P$ mit}
+P_s \subseteq {} &U_s^k\\
+\shortintertext{\item \alert{Funktionen} $f$ mit}
+f_s : {} &U_s^k \to U_s
+\end{align}
+}
+\end{itemize}
+\end{itemize}
+\end{definition}
+\end{frame}
+}

Mercurial > 13ws.ds

comparison notes/tex/logic.tex @ 26:4436f8006ebd