% $Id: gloin-zf.tex,v 1.9 2023/06/29 15:43:48 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 Philip \textsc{Kaluđerčić}
  }
}
\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} \rightarrow \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) \rightarrow \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*}
    (\rightarrow I)\; \dfrac{
      \dfrac{\dfrac{\phi}{\vdots}}{\psi}
    }{\phi \rightarrow \psi},
    \quad
    (\rightarrow E) \; \dfrac{\phi \rightarrow \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) \rightarrow 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. $\rightarrow$ 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. $\rightarrow$ 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))) \rightarrow 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 \rightarrow 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*}
\end{multicols*}
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: