\def\RCS$#1: #2 ${\expandafter\def\csname RCS#1\endcsname{\$#1: #2 \$}} \RCS$Id: gloin-zf.tex,v 1.15 2024/09/16 12:31:27 oj14ozun Exp $ \RequirePackage[l2tabu, orthodox]{nag} \documentclass[final,10pt,a4paper,landscape,ngerman]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{multicol} \usepackage{amssymb,amsmath} \usepackage{hyperref} \usepackage{lmodern} \usepackage{microtype} \usepackage{stmaryrd} \usepackage{babel} \usepackage{tikz} \usepackage{lplfitch} % -> apt install texlive-science \usepackage[extreme]{savetrees} % \renewcommand{\familydefault}{\sfdefault} \pagenumbering{gobble} \title{GLoIn Zusammenfassung} \author{ \footnotesize Verfasst vom FSI-Forum Nutzer \href{https://forum.fsi.cs.fau.de/t/gloin-zusammenfassung-reloaded/15673}{\texttt{pos1ende}}\\ \footnotesize In \href{https://wwwcip.cs.fau.de/~oj14ozun/src+etc/gloin-zf.tex}{\LaTeX gesetzt} von pkal } \date{ \raggedleft \footnotesize Letzte inhaltliche Änderungen: April 2019,\\ zuletzt aktualisiert: Februar 2023,\\ zuletzt gesetzt: \today. } \begin{document} \begin{multicols*}{4} \maketitle{} \paragraph{Atome $A, B, C, \dots \in \mathcal{A}$} Nicht weiter zerlegbare Aussage. Kann wahr ($\top$) oder falsch ($\bot$) annehmen. Bsp.: ``esRegnet'' \paragraph{Wahrheitsbelegungen $\kappa: \mathcal{A} \to \left\{ \top, \bot \right\}$} Eine Abbildung, d.h. $\kappa$ ordnet Atomen konkrete Wahrheitswerte zu. \paragraph{Prädikate $P, Q, R, \dots$} Bsp.: $\mathsf{istKleiner}(x, y)$. Ein Prädikat macht eine Aussage über Individuen (hier $x$ und $y$) und gibt einen Wahrheitswert zurück, wenn es ausgewertet wird. 0-stellige Prädikate sind Konstanten. \paragraph{Funktionen $f, g, h, \dots$} z.B. $\mathsf{mutter}(x)$ gibt ein Objekt / ein Individuum zurück (hier interpretiert als die Mutter von $x$). Nullstellige Funktionen sind Konstanten. \paragraph{Terme $D, E, F, \dots$} Ein Term ist eine Instanz der Grammatik: \[ T \;::=\; x \;|\; c \;|\; f(T, \dots, T) \] wo $x$ eine Variable, $c$ eine Konstante und $f$ eine Funktion ist. Ergebnis der Auswertung eines Terms ist ein Objekt/Individuum. \paragraph{Formeln $\phi, \psi, \dots$} Eine Formel ist eine Instanz der Grammatik: \begin{align*} \phi, \psi \;::=\; &P(t_1, \dots, t_n) \;|\; \neg \phi \;|\;\\ &\phi \land \psi \;|\; \phi \lor \psi \;|\; \phi \to \psi \;|\;\\ &\forall x (\phi) \;|\; \exists x (\phi) \end{align*} wo $t$ ein Term, und $x$ eine Variable ist. Ergebnis der Auswertung einer Formel mittels einer Wahrheitsbelegung ist ein Wahrheitswert. \subparagraph{Negationsnormalform (NNF)} Formel in NNF, wenn $\neg$ nur vor Atomen vorkommt. Aus jeder Formel kann mit diesen Schritten eine Formel in NNF erzeugt werden: \begin{enumerate} \item Negationen aufheben: $\neg\neg \phi \to \phi$ \item \emph{De Morgan} anwenden: \begin{equation*} \neg (\phi \land \psi) \to \neg\phi \lor \neg\psi\\ \neg (\phi \lor \psi) \to \neg\phi \land \neg\psi\\ \end{equation*} \item Negationen Auflösen $\neg\top \to \bot, \neg\bot\to\top$ \end{enumerate} \subparagraph{Konjunktive Normalform (CNF)} Formel der Form $(A \lor B \lor \neg C) \land (\neg A \lor C) \land (\neg B)$. Jede Formel hat eine CNF, und kann aus NNF erzeugt werden: \begin{enumerate} \item $\mathsf{CNF}(\phi \land \psi) = \mathsf{CNF}(\phi) \land \mathsf{CNF}(\psi)$ \item $\mathsf{CNF}((\phi \land \psi) \lor \lambda) = \mathsf{CNF}(\phi) \land \mathsf{CNF}(\psi)$ \item $\mathsf{CNF}(\phi) = \phi$, wenn $\phi$ kein ``$\land$'' enthält. \end{enumerate} \subparagraph{Disjunktive Normalform (DNF)} Inverse Normalform der KNF. Erzeugung: \begin{enumerate} \item $\mathsf{DNF}(\phi \lor \psi) = \mathsf{CNF}(\phi) \lor \mathsf{CNF}(\psi)$ \item $\mathsf{DNF}((\phi \lor \psi) \land \lambda) = \mathsf{DNF}(\phi \land \lambda) \land \mathsf{DNF}(\psi \lor \lambda)$ \item $\mathsf{DNF}(\phi) = \phi$, wenn $\phi$ kein ``$\lor$'' enthält. \end{enumerate} \paragraph{Einige Äquivalenzen} \begin{align*} A \to B &\equiv \neg A \lor B \equiv \neg B \to \neg A\\ A \iff B &\equiv (A \to B) \land (B \to A)\\ \neg\forall y(\phi) &\equiv \exists y(\neg \phi)\\ \neg\epsilon y(\phi) &\equiv \forall y(\neg \phi) \end{align*} \paragraph{Freie Variablen ($\mathsf{FV}$)} sind Menge an Variablen einer Formel, die durch keinen Quantor gebunden sind. \paragraph{Substitution} \[ \sigma = [ E_1/x_1, \dots, E_n/x_n ] \] ersetzt jeweils alle Variablen $x_i$ durch den Term $E_n$. Es berechnet sich durch: \[ x \sigma = \sigma (x) \] \[ f(E_1, \dots, E_n)\sigma \implies f(E_1\sigma, \dots, E_n\sigma) \] \[ P(E_1, \dots, E_n)\sigma \implies P(E_1\sigma, \dots, E_n\sigma) \] \[ (E = D)\sigma \implies E\sigma = D\sigma \] \[ (\neg \phi)\sigma \implies \neg (\phi \sigma) \] \[ (\phi \land \phi)\sigma \implies (\phi \sigma \land \psi\sigma) \] \[ (\phi \lor \phi)\sigma \implies (\phi \sigma \lor \psi\sigma) \] \[ (\forall x (\phi))\sigma \implies \forall x (\phi \sigma^{\prime}) \] \[ (\exists x (\phi))\sigma \implies \exists x (\phi \sigma^{\prime}) \] Wobei $\sigma^{\prime}(x) = y$, für alle anderen $z \neq x$ bleibt $\sigma^{\prime}(z) = \sigma(z)$. Wähle $y$ so, dass $y \notin \mathsf{FV}(\sigma(z))$ für alle $z \in \mathsf{FV}(\forall x(\phi))$ bzw. $\exists x (\phi)$. \paragraph{Weitere Normalformen} \subparagraph{Pränexe Normalform (PNF)} Alle Quantoren $Q_n \in \{ \forall, \exists \}$ stehen am Anfang der Formel: $Q_1 x_1 \dots Q_n x_n (\phi)$. Wird erzeugt durch wiederholtes anwenden von \[ \phi \land \exists x (\psi) \equiv \exists x (\phi \land \psi) \] \[ \phi \lor \exists x (\psi) \equiv \exists x (\phi \lor \psi) \] \[ \phi \land \forall x (\psi) \equiv \forall x (\phi \land \psi) \] \[ \phi \lor \forall x (\psi) \equiv \forall x (\phi \lor \psi) \] Nur falls $x \notin \mathsf{FV}(\phi)$. Dies kann durch Umbenennung erreicht werden: Wende $[\widetilde{x}/x]$ auf den Quantifizierten Teil an. Bspw.: \[ \phi \lor \exists x (\psi) \to \exists \phi \lor \widetilde{x} (\psi[\widetilde{x}/x])\] \subparagraph{Skolemform} ist PNF ohne Existenzquantoren. Nicht zu jeder Formel existiert eine Skolemform. Allerdings lässt sich zu jeder Formel eine \emph{erfüllbarkeitsäquivalente} Skolemform berechnen. $\phi$ und $\psi$ erfüllbarkeitsäquivalent gdw. ($\phi$ erfüllbar $\iff$ $\psi$ erfüllbar). Diese zu finden, für $\phi[c/x]$ ($c$ frisch) erfüllbar heißt Skolemisierung (aus PNF): \[ \forall x_1 \dots \forall x_n \exists y (\phi)\]\[ \implies \forall x_1 \dots \forall x_n (\phi [f_y(x_1, \dots, x_n)/y]) \] erschöpfend anwenden. Dabei für jedes $y$ eine neue Skolem-Funktion $f_y$ einführen. Diese hat als Parameter alle $\forall$-Quantifierten Variablen links vom zu eliminierenden ``$\exists$'' (also \textbf{nicht} die $\exists$-Quantifizierten). Falls keine ``$\forall$''s vor dem zu eliminierenden ``$\exists$'' stehen, ist $f_y$ von eine nullstellige Funktion: \emph{Skolem-Konstante}. \subparagraph{Klauselform} Sei $\Psi = \forall x_1 \dots \forall x_n (\phi)$ in Skolemform. Wenn $\psi$ in CNF gebracht wird, können alle ``$\forall$'' implizit angenommen werden, und $\psi$ als Klauselmenge geschrieben werden. \paragraph{Unifikation} Gleichungssystem \[S = \{E_1 \dot{=} E_2, E_3 \dot{=} E_4, \dots{}\},\] wobei $E_i$ Terme sind. $S$ ist gelöst, falls \begin{enumerate} \item jede Gleichung die Form $v\dot{=}E$ hat, wobei v eine Variable und E ein Term ist. \item jedes solche $v$ max. 1 mal auf einer linken Seite steht (nochmal in rechter Seite ist okay). \end{enumerate} Mit Unifikationsalgorithmus auf Unifizierbarkeit prüfbar: \begin{description} \item[\texttt{(delete)}] \[ S \cup \{ x \dot{=} x \} \implies S \] \item[\texttt{(decomp)}] \[ S \cup \{ f(E_1, \dots, E_n) \dot{=} f(D_1, \dots, D_n) \} \] \[ \implies S \cup \{ E_1 \dot{=} D_1, \dots, E_n \dot{=} D_n \} \] \item[\texttt{(conflict)}] für $f \neq g$ \[ S \cup \{ f(E_1, \dots, E_n) \dot{=} g(D_1, \dots, D_n) \} \implies \bot \] \item[\texttt{(orient)}] für $E$, keine Variable \[ S \cup \{ E \dot{=} x\} \implies S \cup \{ x \dot{=} E \} \] \item[\texttt{(occurs)}] für $x \in \mathsf{FV}(E), x \neq E$ \[ S \cup \{ x \dot{=} E \} \implies \bot \] \item[\texttt{(elim)}] für $x \notin \mathsf{FV}(E), x \in \mathsf{FV}(S)$ \[ S \cup \{ x \dot{=} E \implies S[E/x] \} \cup \{ x \dot{=} E \} \] \end{description} Falls $\bot$ erreicht wird, ist das System nicht \emph{unifizierbar}, ansonsten kann unifizierendes MGU aus $x_i \dot{=} E_i$ abgelesen werden. \paragraph{Resolution in FOL} Mit $\Phi$ in Klausenform kann Halbentscheidungsverfahren (Rekursiv Auszählbar, terminiert nicht wenn $\Phi$ erfüllbar) für \emph{Unerfüllbarkeit} von $\Phi$ ausgeführt werden: \[\left( \text{RIF} \right)\ \dfrac{C_{1},A_{1},\dots,A_{n}\text{\ \ \ \ \ }C_{2},\neg B}{C_{1}\sigma,C_{2}\sigma}\text{\ \ \ \ \ \ \ }\] \[ \sigma = \mathsf{mgu}\left( A_{1}\dot{=}B,\dots,A_{n}\dot{=}B \right) \] Wende RIF so lange an, bis $\Box$ erreicht oder RIF nicht mehr anwendbar. \paragraph{Fitch/natürliche Deduktion} $A, B$ seien Terme, $\Phi, \Psi$ Formeln und $c$ ein konkretes Subjekt. Die Regeln sind: \subparagraph{Konjunktion} \begin{equation*} (\land I) \; \dfrac{\phi \qquad \psi}{\phi \land \psi}, \quad (\land E_1) \; \dfrac{\phi \land \psi}{\phi}, \quad (\land E_2) \; \dfrac{\phi \land \psi}{\psi} \end{equation*} \subparagraph{Disjunktion} \begin{equation*} (\lor I_1) \; \dfrac{\phi}{\phi \lor \psi}, \quad (\lor I_2) \; \dfrac{\psi}{\phi \land \psi}, \quad (\lor E) \; \dfrac{ \dfrac{\dfrac{\phi}{\vdots}}{\chi} \dfrac{\dfrac{\psi}{\vdots}}{\chi} \phi \lor \psi}{\chi} \end{equation*} \subparagraph{Implikation} \begin{equation*} (\to I)\; \dfrac{ \dfrac{\dfrac{\phi}{\vdots}}{\psi} }{\phi \to \psi}, \quad (\to E) \; \dfrac{\phi \to \psi \qquad \phi }{\psi} \end{equation*} \subparagraph{Negation} \begin{equation*} (\neg I)\; \dfrac{ \dfrac{\dfrac{\phi}{\vdots}}{\bot} }{\neg \phi}, \quad (\neg E) \; \dfrac{\neg\neg\phi}{\phi} \quad \end{equation*} \subparagraph{Falsum} \begin{equation*} (\bot I) \; \dfrac{\phi\qquad\neg\phi}{\bot}, \quad (\bot E) \; \dfrac{\bot}{\Psi} \end{equation*} \subparagraph{Gleichheit} \begin{equation*} (= I)\; \dfrac{}{E = E}, \quad (= E) \; \dfrac{\phi[E/x] \quad E = D}{\phi[E/x]} \end{equation*} \subparagraph{Existenzquantor} \begin{equation*} (\exists I) \; \dfrac{\Phi[E/x]}{\exists x (\Phi)}, \quad (\exists E) \; \dfrac{ \exists x (\phi) \quad \dfrac{\dfrac{\fbox{c}, \Phi[c/x]}{\vdots}}{\phi} }{\phi} \end{equation*} \subparagraph{Allquantor} \begin{equation*} (\forall I) \quad \dfrac{ \dfrac{\dfrac{\fbox{c}}{\vdots}}{\phi[c/x]} }{\forall x (\phi)} \quad (\forall E) \quad \dfrac{\forall x (\phi)}{\phi[E/x]}, \end{equation*} \paragraph{Aristotelische Formen} sind Sonderformen in FOL: \begin{itemize} \item Alle $P$ sind $Q$: $\forall x (P(x) \to Q(x))$ \item Manche $P$ sind $Q$: $\exists x (P(x) \land Q(x))$ \end{itemize} \paragraph{Induktion} Kann auf verschiedene Strukturen betrieben werden. \subparagraph{``Normale'' Induktion} Zusammenbauen, zeige das für jede Vergrößerung z.Z. noch gilt. \begin{description} \item[I.A.] Zeige, dass z.Z. gilt für einfachste(s) Element(e). \item[I.V.] Seien beliebige(s) Element(e) $A, B, \dots{}$ welche z.Z. schon erfüllen gegeben. \item[I.S.] Sei $X$ beliebiges Element. (anders als $A, B, \dots{}$ erfüllt $X$ z.Z. noch nicht unbedingt) Fallunterscheidung: \begin{enumerate} \item $X$ hat Form aus I.A. $\to$ z.Z. gilt \item $X$ hat Form I \item $X$ hat Form II \end{enumerate} Für jede Art (ggf. mehrere, hier zwei), auf die man Element(e) zu einem nächst-komplexeren/größeren ``zusammenbauen'' kann: Zeige, dass das Komplexere dann immernoch z.Z. erfüllt. ``Verbaue'' dabei die $A, B, \dots{}$ aus der I.V., denn von diesen weiß man ja schon, dass sie z.Z. erfüllen. \end{description} \subparagraph{Strukturelle Induktion} auseinandernehmen, rekursiv auf einfachste Fälle zurückführen. \begin{description} \item[I.A.] Zeige für alle einfachsten Fälle, dass sie z.Z. erfüllen. \item[I.V.] Braucht man meist nicht! \item[I.S.] Sei $X$ beliebiges Element. Gehe alle Fälle durch, von welcher Form $X$ sein könnte: \begin{enumerate} \item $X$ hat Form aus I.A. $\to$ z.Z. gilt \item $X$ hat ``zusammengebaute'' Form (ggf. mehrere Arten, dann mehrere Fälle) Argumentiere, dass einige Bestandteile wieder beliebige Elemente sind, genau wie $X$, und deshalb diese Fallunterscheidung rekursiv angewendet werden kann, wobei man (da $X$ endlich groß etc. stets irgendwann auf den Fall a) stößt und dann z.Z. gilt.\\ Die Bestandteile erfüllen also z.Z. Beweise jetzt noch, dass für jede Art, sie zusammenzubauen (``Rekursionsschateln abbauen'') wieder z.Z. gilt. \end{enumerate} \end{description} \subparagraph{\emph{Course-Of-Values}-Induktion} Zu zeigen: $\forall n (P(n))$ BNF bilden, bestehend aus Signatur und einer Alternative für eine Variable. z.B. $E, E_1, E_2 ::= \mathsf{mult}(E_1, E_2) | \mathsf{zero}() | v$, mit Variable v. \begin{description} \item[I.A.] Zeige, dass $P$ für $v$ und Konstanten gilt \item[I.V.] \emph{Course-of-Values}-Induktion. $k, n$: Terme. ``$<$'' vergleicht Länge der Terme: $\forall n (\forall k < n (P(k))) \to P(n)$ \item[I.S.] Sei ein Term $n$ (Instanz der BNF) gegeben. Es gelte $\forall k \leq n (P(n))$. z.Z.: $\forall k \leq n+1 (P(n))$\\ Brich die Aussage auf die beteiligten Terme herunter (Siehe Seite 35 im Skript). Dank Induktions-Voraussetzung wissen wir, dass die zu beweisende Aussage bereits für die beteiligten Terme (die Bestandteile) gilt. Bilde daraus die benötigte Folgerung, also zeige, dass dann für ``Zusammengesetztes'' auch die zu beweisende Annahme gilt. \end{description} \paragraph{Modelle/Semantik} Ein $\Sigma$-Modell $\mathfrak{M}$ besteht aus \begin{itemize} \item einer nichtleeren Trägermenge $M$. \item Einer Interpretation für jedes $n$-stellige Funktionssysmbol $f/_n \in \Sigma$, durch eine Funktion \[\mathfrak{M}\llbracket f \rrbracket:\ M^{n} \mapsto M\] \item Einer Interpretation für jedes $n$-stellige Prädikatensymbol $P/_n \in \Sigma$, durch eine Teilmenge \[\mathfrak{M}\llbracket P\rrbracket \subseteq M^{n}\] \end{itemize} Eine Umgebung $\eta$ ist eine Abbildung $\eta: V \to M$, ordnet jeder Variablen $v \in V$ einen Wert $m \in M$ der Trägermenge zu. Ein spezielles $\Sigma$-Modell ist das Herbrand-Modell, in diesem gibt es keine Variablen in den Termen. Deshalb ist $\eta$ dann leer und kann weggelassen werden. Ein Term $E$ wird Interpretiert wie folgt: \[ \mathfrak{M} \llbracket x\rrbracket\eta = \eta(x)\] \[\mathfrak{M}\llbracket f(E_{1},\ \dots,E_{n})\rrbracket\eta \] \[ = \mathfrak{M}\llbracket f\rrbracket\eta(\mathfrak{M}\llbracket E_{1}\rrbracket\eta, \dots, \mathfrak{M}\llbracket E_{n}\rrbracket\eta) \] Erfülltheit von $\psi$ durch $\mathfrak{M}$ und $\eta$ (kurz $\mathfrak{M}, \eta \models \psi$): \begin{align*} \mathfrak{M}, \eta \models& (E = D) \iff M\llbracket E_n \rrbracket_{\eta} = M\llbracket D_n \rrbracket_{\eta} \\ \mathfrak{M}, \eta \models& P(E_1, \dots, E_n) \iff \in M\llbracket P \rrbracket \\ \mathfrak{M}, \eta \models& \forall x(\phi)\\ \iff& \;\text{für alle $m \in M$ gilt: } \mathfrak{M}, \eta \models \phi\\ \intertext{wo} \eta[x \mapsto m](y) =& \begin{cases} m & \text{ für } y = x\\ \eta(y) & \text{ sonst} \end{cases} \end{align*} \vfill {\noindent\tiny\ttfamily\RCSId} \end{multicols*} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: