logik.tex

\documentclass{cheat-sheet}

\pdfinfo{
  /Title (Zusammenfassung Logik für Informatiker)
  /Author (Tim Baumann)
}

\usepackage{MnSymbol} % \leftmodels, \rightmodels
\usepackage{bussproofs} % natural deduction type-setting
\usepackage{nicefrac} % Für Ersetzung, z.B. $[t/x]$
\usepackage{pgffor} % \foreach-Schleifen

\newcommand{\Ibm}{I, \beta \models}
\newcommand{\Ibnm}{I, \beta \not\models}
\newcommand{\Iba}[1]{(#1)_{I,\beta}} % I-Beta-Auswertung
\newcommand{\lra}{\leftrightarrow}
\newcommand{\At}{\mathrm{At}} % Atomare Formeln
\newcommand{\Term}{\mathrm{Term}} % Term
\newcommand{\For}{\mathrm{For}} % Formel
\newcommand{\TFor}{\mathrm{TFor}} % Formel in temporaler Logik
\newcommand{\CTFor}{\mathrm{CTFor}} % Formel in Computation-Tree-Logic
\newcommand{\MFor}{\mathrm{MFor}} % Formel in modaler Logik
\newcommand{\Res}{\mathrm{Res}} % Resolvente
\newcommand{\Ax}{\mathrm{Ax}} % Axiom
\newcommand{\FV}{\mathrm{FV}} % Freie Variablen
\newcommand{\BV}{\mathrm{BV}} % Gebundene Variablen
\newcommand{\eqmodels}{\leftmodels \rightmodels} % Äquivalenz von Formeln
\newcommand{\subst}[2]{\nicefrac{#1}{#2}} % Ersetzung
\newcommand{\HoareT}[3]{\{ #1 \} \enspace #2 \enspace \{ #3 \}} % Hoare-Tripel
\newcommand{\nspace}[1]{\foreach \i in {1,...,#1}{ \! }} % Negativer Abstand
\newcommand{\X}{\mathbf{X}} % Next, im nächsten Zustand (verwendet in temporaler Logik)
\newcommand{\G}{\mathbf{G}} % Globally, in allen Zuständen (verwendet in temporaler Logik)
\newcommand{\F}{\mathbf{F}} % Finally, in mindestens einem der folgenden Zuständen (verwendet in temporaler Logik)
\newcommand{\U}{\,\mathbf{U}\,} % Until (verwendet in temporaler Logik)

% Für Computation-Tree-Logic:
\newcommand{\A}{\mathbf{A}}
\newcommand{\E}{\mathbf{E}}
\newcommand{\AG}{\mathbf{AG}}
\newcommand{\EG}{\mathbf{EG}}
\newcommand{\AF}{\mathbf{AF}}
\newcommand{\EF}{\mathbf{EF}}
\newcommand{\AX}{\mathbf{AX}}
\newcommand{\EX}{\mathbf{EX}}


\begin{document}

\maketitle{Zusammenfassung Logik für Informatiker}

\section{Prädikatenlogik erster Stufe}

% Kapitel 1.1. Syntax

\begin{nota}
  Die Symbole $x_0, x_1, ...$ seien reserviert für die Verwendung als Variablennamen.
\end{nota}

\begin{defn}
  Eine \emph{Signatur} ist ein Paar $(\mathcal{F}, \mathcal{P})$, wobei $\mathcal{F}$ und $\mathcal{P}$ disjunkte, höchstens abzählbare Zeichenmengen sind. Dabei gibt es Folgen $(\mathcal{F}^n)_{n \in \N_0}$ und $(\mathcal{P}^n)_{n \in \N_0}$, sodass gilt:
  \[
    \mathcal{F} = \bigsqcup_{n \in \N_0} \mathcal{F}^n, \quad
    \mathcal{P} = \bigsqcup_{n \in \N_0} \mathcal{P}^n.
  \]
  Wir interpretieren $\mathcal{F}^n$ als Menge der $n$-stelligen Funktionssymbole, $\mathcal{F}^0$ als Menge von Konstanten und $\mathcal{P}^n$ als Menge der $n$-stelligen Prädikatensymbole.
\end{defn}

\begin{defn}
  Die Menge $\emph{\Term_{\mathcal{F}, \mathcal{P}}}$ ist die kleinste Menge mit
  \begin{itemize}
    \item $\{ x_0, x_1, ... \} \subset \Term$
    \item $\fa{n \in \N_0} \fa{f \in \mathcal{F}^n} \fa{t_1, ..., t_n \in \Term} f(t_1, ..., t_n) \in \Term$
  \end{itemize}
\end{defn}

\begin{defn}
  Die Menge der \emph{atomaren $(\mathcal{F}, \mathcal{P})$-Formeln} ist induktiv definiert als die kleinste Menge $\At_{\mathcal{F},\mathcal{P}}$ mit
  \begin{itemize}
    \item $\fa{t_1, t_2 \in \Term_{\mathcal{F},\mathcal{P}}} (t_1 = t_2) \in \At_{\mathcal{F},\mathcal{P}}$ \enspace (Logik mit Gleichheit)
    \item $\fa{n \in \N_0} \fa{P \in \mathcal{P}^n} \fa{t_1, ..., t_n \in \Term_{\mathcal{F},\mathcal{P}}} P(t_1, ..., t_n) \in \At_{\mathcal{F},\mathcal{P}}$
  \end{itemize}
\end{defn}

\begin{nota}
  $true \coloneqq p_0 \vee \neg p_0, \quad false \coloneqq \neg true$ \quad für $p_0 \in \mathcal{P}^0$ fest.
\end{nota}

\begin{defn}
  Die Menge der \emph{$(\mathcal{F}, \mathcal{P})$-Formeln} ist induktiv definiert als kleinste Menge $\For_{\mathcal{F},\mathcal{P}}$ mit
  \begin{itemize}
    \miniitem{0.29 \linewidth}{$\At_{\mathcal{F},\mathcal{P}} \subset \For_{\mathcal{F},\mathcal{P}}$}
    \miniitem{0.69 \linewidth}{$\fa{A \in \For_{\mathcal{F},\mathcal{P}}} \{ \neg A, \fa{x}\!A, \ex{x}\!A \} \subset \For_{\mathcal{F},\mathcal{P}}$}
    \item $\fa{A, B \in \For_{\mathcal{F},\mathcal{P}}} \{ A \wedge B, A \vee B, A \to B, A \lra B \} \subset \For_{\mathcal{F},\mathcal{P}}$
  \end{itemize}
\end{defn}

% Ausgelassen: Herleitung, Induktion über Herleitungen

% Kapitel 1.2. Semantik

\begin{defn}
  Eine Interpretation $I$ einer Signatur $(\mathcal{F}, \mathcal{P})$ besteht aus einer Menge $D = D_I$ und Zuordnungen
  \[
    \blank^I : \prod_{n \in \N_0} \prod_{f \in \mathcal{F}^n} (D_I)^n \to D_I, \quad
    \blank^I : \prod_{n \in \N_0} \prod_{P \in \mathcal{P}^n} (D_I)^n \to \{ F, T \}
  \]
\end{defn}

\begin{defn}
  Eine Belegung $\beta$ zu einer Interpretation $I$ ist eine Funktion
  \[ \beta : \{ x_0, x_1, ... \} \to D_I. \]
\end{defn}

\begin{nota}
  Sei $\beta : \{ x_0, x_1, ... \} \to D_I$ eine Belegung zu einer Interpretation $I$, $x$ eine Variable und $d \in D_I$. Dann setze
  \[ \beta_x^d : \{ x_0, x_1, ... \} \to D_I, \quad y \mapsto \begin{cases} d, & \text{falls } x = y \\ \beta(y), & \text{sonst} \end{cases} \]
\end{nota}

% Ausgelassen: Definition Auswertung

\begin{defn}
  Die \emph{Auswertung} eines Terms $t$ unter $I$ und $\beta$ (geschrieben $t_{I,\beta}$) ist induktiv definiert als
  \begin{itemize}
    \miniitem{0.3 \linewidth}{$x_{I, \beta} \coloneqq \beta(x)$}
    \miniitem{0.6 \linewidth}{$f(t_1, ..., t_n) \coloneqq f^I((t_1)_{I, \beta}, ..., (t_n)_{I, \beta})$}
  \end{itemize}
\end{defn}

\begin{defn}
  Eine Interpretation $I$ und eine Belegung $\beta$ \emph{erfüllen} eine eine Formel $F$, geschrieben $I, \beta \models F$, falls
  \begin{alignat*}{3}
    & \Ibm (t_1 = t_2) &&\coloniff&& \Iba{t_1} = \Iba{t_2}\\[-2pt]
    & \Ibm P(t_1, ..., t_n) &&\coloniff&& P^I(\Iba{t_1}, ..., \Iba{t_n}) \\[-2pt]
    & \Ibm \neg A &&\coloniff&& \Ibnm A \\[-2pt]
    & \Ibm A \wedge B &&\coloniff&& (\Ibm A) \wedge (\Ibm B) \\[-2pt]
    & \Ibm A \vee B &&\coloniff&& (\Ibm A) \vee (\Ibm B) \\[-2pt]
    & \Ibm A \to B &&\coloniff&& (\Ibnm A) \vee (\Ibm B) \\[-2pt]
    & \Ibm A \lra B &&\coloniff&& \quad\, ((\Ibnm A) \wedge (\Ibnm B))\\[-2pt]
    & && && \vee ((\Ibm A) \wedge (\Ibm B)) \\[-2pt]
    & \Ibm \fa{x} A &&\coloniff&& \fa{d \in D_I} I, \beta_x^d \models A \\[-2pt]
    & \Ibm \ex{x} A &&\coloniff&& \ex{d \in D_I} I, \beta_x^d \models A
  \end{alignat*}
\end{defn}

% Ausgelassen: Einführung von Wahrheitstafeln

\begin{prop}
  Es gilt für alle Interpretationen $I$, Belegungen $\beta$ und Formeln $A, B$:
  \begin{alignat*}{2}
    & \Ibm A &&\iff \Ibnm \neg A \iff \Ibm \neg\neg A\\[-2pt]
    & \Ibm A \wedge B &&\iff \Ibm \neg (A \to \neg B)\\[-2pt]
    & \Ibm A \vee B &&\iff \Ibm \neg A \to B\\[-2pt]
    & \Ibm A \lra B &&\iff \Ibm (A \to B) \wedge (B \to A)\\[-2pt]
    & \Ibm \ex{x} A &&\iff \Ibm \neg \fa{x} \neg A
  \end{alignat*}
\end{prop}

% Kapitel 1.3. Modelle und Folgerbarkeit

\begin{defn}
  Seien $A \in \For$, $M \subset \For$ und $I$ eine Interpretation. Dann heißt $I$ ein \emph{Modell} von $A$ bzw. $M$, falls
  \begin{align*}
    I \models A &\coloniff \text{für alle Belegungen $\beta$ gilt } \Ibm A,\\
    I \models M &\coloniff \fa{F \in M} I \models F.
  \end{align*}
\end{defn}

\begin{nota}
  Für $M \subset \For$, eine Interpretation $I$ und eine Belegung $\beta$ schreiben wir:
  \[ \Ibm M \coloniff \fa{F \in M} \Ibm F \]
\end{nota}

\begin{defn}
  Seien $A, B \subset \For$. Man sagt, $B$ \emph{folgt} aus $A$ (geschrieben $A \models B$), falls für alle Interpretationen $I$ und Belegungen $\beta$ gilt:
  \[ \Ibm A \implies \Ibm B. \]
  Falls $A \models B$ und $B \models A$ gilt, so heißen $A$ und $B$ \emph{logisch äquivalent}, geschrieben $A \eqmodels B$.
\end{defn}

\begin{nota}
  $A_1, ..., A_n \models A \coloniff \{ A_1, ..., A_n \} \models A$
\end{nota}

\begin{satz}
  Für alle Interpretationen $I$ und $n \in \N$ gilt:
  \[ I \models \{ A_1, ..., A_n \} \iff I \models A_1 \wedge ... \wedge A_n \]
\end{satz}

\begin{satz}
  Für alle $A, B \in \For$ und $M \subset \For$ gilt:
  \[ M \models A \to B \iff M \cup \{A\} \models B \]
\end{satz}

\begin{defn}
  Eine Formel $A \in \For$ heißt \emph{Tautologie} oder \emph{(allgemein-) gültig} (geschrieben $\models A$), falls $I \models A$ für alle Interpretationen $I$ gilt.
\end{defn}

\begin{defn}
  Eine Formel $A \in \For$ heißt \emph{erfüllbar}, wenn es eine Interpretation $I$ und eine Belegung $\beta$ mit $\Ibm A$ gibt. Falls es dies nicht gibt, so heißt $A$ \emph{unerfüllbar}.
\end{defn}

\begin{satz}
  Für $A \in \For$ gilt:
  \begin{itemize}
    \miniitem{0.45\linewidth}{$\models A \implies A \text{ ist erfüllbar}$}
    \miniitem{0.35\linewidth}{$\models A \iff \emptyset \models A$}
  \end{itemize}
\end{satz}

\begin{satz}
  Sei $A \in \For$ und $M \subset \For$. Dann gilt $M \models A$ genau dann, wenn $M \cup \{ \neg A \}$ unerfüllbar ist. Insbesondere ist $A$ genau dann gültig, wenn $\{ \neg A \}$ unerfüllbar ist.
\end{satz}

% Kapitel 1.4. Teil-Interpretationen

% Ausgelassen: Definition Teil-Interpretation, Teil-Modell

\begin{defn}
  \emph{Universelle Formeln} sind Formeln, die sich nach den folgenden Regeln herleiten lassen:

  \begin{center}
    \begin{minipage}{0.32\linewidth}
      \begin{prooftree}
        \AxiomC{$A$ ist quantorenfrei}
        \UnaryInfC{$A$}
      \end{prooftree}
    \end{minipage}
    \begin{minipage}{0.21\linewidth}
      \begin{prooftree}
        \AxiomC{$A\nspace{8}$}
        \AxiomC{$B$}
        \BinaryInfC{$A \wedge B$}
      \end{prooftree}
    \end{minipage}
    \begin{minipage}{0.21\linewidth}
      \begin{prooftree}
        \AxiomC{$A\nspace{8}$}
        \AxiomC{$B$}
        \BinaryInfC{$A \vee B$}
      \end{prooftree}
    \end{minipage}
    \begin{minipage}{0.21\linewidth}
      \begin{prooftree}
        \AxiomC{$A$}
        \UnaryInfC{$\fa{x} A$}
      \end{prooftree}
    \end{minipage}
  \end{center}
\end{defn}

\begin{samepage}
  
\begin{prop}
  Sei $I$ eine Teil-Interpretation zu $J$, $\beta$ eine Belegung zu $I$ und $A$ eine universelle Formel. Dann gilt:
  \[ J, \beta \models A \implies I, \beta \models A. \]
\end{prop}

\section{Aussagenlogik}

\end{samepage}

% Kapitel 2.1. Allgemeines, Wahrheitstafeln

% Ausgelassen: Begriff Atom

% Ausgelassen: Entscheidbarkeit des Wahrheitsgehalts mit Wahrheitstafeln
% Ausgelassen: Satz 2.3
% Ausgelassen: Strukturelle Definition von Ersetzung von $p_0$ durch $A$
% Ausgelassen: Lange Liste von aussagenlogischen Äquivalenzen (Kommutativität, Idempotenz, Distributivität, etc.)

\begin{defn}
  Für $p \in \mathcal{P}^0$ heißen die Ausdrücke $p$ und $\neg p$ \emph{Literale}. Eine Disjunktion von Literalen heißt \emph{Klausel}. Eine Formel ist in \emph{konjunktiver Normalform (KNF)}, wenn sie eine Konjunktion von Klauseln ist.
\end{defn}

% Ausgelassen: Disjunktive Normalform

\begin{prob}[\emph{SAT}]
  Gegeben sei eine Formel in konjunktiver Normalform. Frage: Ist diese Formel erfüllbar?
\end{prob}

\begin{defn}
  Eine Formel ist in \emph{Negationsnormalform (NNF)}, wenn Negationen nur unmittelbar vor Atomen stehen.
\end{defn}

% Ausgelassen: Verfahren, um Formel in NNF und dann in KNF zu überführen

% Kapitel 2.2. Der Hilbert-Kalkül

% Ausgelassen: Definition von Korrektheit und Vollständigkeit von Kalkülen

\begin{defn}
  Der \emph{Hilbert-Kalkül} besteht aus den Axiomen
  \begin{align*}
    \Ax_1 &\coloneqq \Set{ A \to (B \to A) }{ A, B \in \For }\\
    \Ax_2 &\coloneqq \Set{ (A \to (B \to C)) \to ((A \to B) \to (A \to C)) }{ A, B, C \in \For }\\
    \Ax_3 &\coloneqq \Set{ (\neg A \to \neg B) \to (B \to A) }{ A, B \in \For }
  \end{align*}
  und der Schlussregel \emph{Modus Ponens (MP)}
  \begin{prooftree}
    \AxiomC{$A\nspace{10}$}
    \AxiomC{$A \to B$}
    \BinaryInfC{$B$}
  \end{prooftree}
\end{defn}

\begin{defn}
  Eine Formel $F \in \For$ ist aus $M \subset \For$ \emph{H-herleitbar}, notiert $M \vdash_H A$, wenn es eine Folge $A_1, ..., A_n$ in $\For$ gibt mit $A_n = A$, sodass für alle $i \in \{ 1, ..., n \}$ gilt:
  \[
    A_i \in \Ax_1 \cup \Ax_2 \cup \Ax_3 \cup M
    \quad \text{oder} \quad
    \ex{j, k < i} A_j = A_k \to A_i.
  \]
\end{defn}

\begin{defn}
  $A \in \For$ heißt \emph{herleitbar}, notiert $\vdash A$, falls $\emptyset \vdash A$ gilt.
\end{defn}

\begin{beob}
  Präfixe und Verkettungen von Herleitungen sind ebenfalls Herleitungen.
\end{beob}

\begin{prop}
  \begin{itemize}
    \item Aus $M \vdash A$ und $M \vdash A \to B$ folgt $M \vdash B$.
    \item Aus $M \vdash \neg A \to \neg B$ folgt $M \vdash B \to A$.
  \end{itemize}
\end{prop}

\begin{satz}[Deduktionstheorem]
  $M \vdash A \to B \iff M \cup \{ A \} \vdash B$
\end{satz}

% 2.9.
\begin{satz}
  Für alle $A, B, C \in \For$ gilt:
  \begin{itemize}
    \miniitem{0.65 \linewidth}{$\vdash (A \to B) \to ((B \to C) \to (A \to C))$}
    \miniitem{0.32 \linewidth}{$\vdash \neg A \to (A \to B)$}
    \miniitem{0.32 \linewidth}{$\vdash \neg\neg A \to A$}
    \miniitem{0.32 \linewidth}{$\vdash A \to \neg\neg A$}
    \miniitem{0.32 \linewidth}{$\vdash (\neg A \to A) \to A$}
  \end{itemize}
\end{satz}

% 2.10.
\begin{prop}
  Es gilt:
  
  \begin{center}
    \begin{minipage}{0.4\linewidth}
      \begin{prooftree}
        \AxiomC{$A \to B$}
        \AxiomC{$B \to C$}
        \BinaryInfC{$A \to C$}
      \end{prooftree}
    \end{minipage}
    \begin{minipage}{0.15\linewidth}
      \begin{prooftree}
        \AxiomC{$\neg\neg A$}
        \UnaryInfC{$A$}
      \end{prooftree}
    \end{minipage}
  \end{center}
\end{prop}

% Kapitel 2.3. Korrektheit und Vollständigkeit

% 2.11.
\begin{satz}[Korrektheitssatz]
  Sei $A \in \For$ und $M \subset \For$. Dann gilt
  \[ M \vdash A \implies M \models A. \]
\end{satz}

\begin{defn}
  $M \subset \For$ heißt \emph{konsistent}, wenn für kein $A \in \For$ zugleich $M \vdash A$ und $M \vdash \neg A$ gilt.
\end{defn}

\begin{lem}
  \begin{itemize}
    \item Ist $M$ inkonsistent, so gilt $M \vdash B$ für alle $B \in \For$.
    \item Für $A \in \For$ gilt: $M \not\vdash A \implies M \cup \{ \neg A \}$ ist konsistent.
  \end{itemize}
\end{lem}

% 2.14.
\begin{lem}[Modell-Lemma]
  Jede konsistente Menge ist erfüllbar, \dh{} sie besitzt ein Modell.
\end{lem}

% 2.15.
\begin{satz}[Vollständigkeitssatz]
  Sei $A \in \For$ und $M \subset \For$. Dann gilt
  \[ M \models A \implies M \vdash A. \]
\end{satz}

% Ausgelassen: Rest von Zusammenfassung 2.16.
\begin{prop}
  Sei $M \subset \For$. Dann ist $M$ genau dann erfüllbar, wenn $M$ konsistent ist.
\end{prop}

\begin{samepage}

% 2.17.
\begin{satz}[Endlichkeits- bzw. Kompaktheitssatz]
  Sei $A \in \For$, $M \subset \For$.
  \begin{itemize}
    \item Dann gilt $M \models A$ genau dann, wenn es eine endliche Teilmenge $M' \subset M$ mit $M' \models A$ gibt.
    \item Dann ist $M$ genau dann erfüllbar, wenn jede endliche Teilmenge von $M$ erfüllbar ist.
  \end{itemize}
\end{satz}

\section{Hilbert-Kalkül für Prädikatenlogik}
  
\end{samepage}

% Kapitel 3.1. Vorbereitung

\begin{prop}
  Es gilt für alle $A \in \For$, $M \subset \For$:
  \[ M \models A \implies (\fa{\text{Interpretationen } I} I \models M \implies I \models A) \]
\end{prop}

\begin{acht}
  Die Umkehrung gilt nicht!
\end{acht}

% 3.2.
\begin{prop}
  Sei $A \in \For$. Dann gilt:
  \begin{itemize}
    \miniitem{0.28\linewidth}{$\fa{x} A \models A$}
    \miniitem{0.48\linewidth}{$A \models \fa{x} A$ nicht (i.\,A.)}
  \end{itemize}
\end{prop}

% Ausgelassen: Definition 3.2. (Rekursive Definition von freien und gebundenen Variablen)
% Vereinfachung:
\begin{defn}
  Sei $A \in \For$. Dann bezeichnet $\FV(A)$ die Menge der \emph{freien} Variablen und $\BV(A)$ die Menge der \emph{gebundenen} Variablen in $A$.
\end{defn}

\begin{defn}
  Eine Formel $A \in \For$ heißt \emph{geschlossen}, falls $\FV(A) = \emptyset$.
\end{defn}

\begin{defn}
  \begin{itemize}
    \item $\fa{x} A$ heißt \emph{Generalisierung} von $A \in \For$.
    \item Ist $\FV(A) = \{ y_1, ..., y_n \}$, so heißt jede der $n!$ Formeln $\fa{y_1} \fa{y_2} ...\, \fa{y_n} A$ ein \emph{universeller Abschluss} von $A$.
  \end{itemize}
\end{defn}

% 3.5.
\begin{satz}[Koinzidenzlemma]
  Seien $A, B \in \For$, $I$ eine Interpretation und $\beta_1, \beta_2$ Belegungen mit $\beta_1|_{\FV(A)} = \beta_2|_{\FV(A)}$. Dann gilt
  \[ I, \beta_1 \models A \enspace\iff\enspace I, \beta_2 \models A. \]
\end{satz}

\begin{kor}
  Seien $A, M$ geschlossen und $\beta_1, \beta_2$ Belegungen. Dann gilt
  \begin{itemize}
    \miniitem{0.48 \linewidth}{$I, \beta_1 \models M \iff I, \beta_2 \models M$}
    \miniitem{0.48 \linewidth}{$I, \beta_1 \models M \iff I \models M$}
    \item $M$ ist erfüllbar $\iff$ $M$ hat ein Modell
    \item $M \models A \iff (\fa{\text{Interpretationen } I} I \models M \iff I \models A)$
  \end{itemize}
\end{kor}

% 3.7
\begin{prop}
  \begin{minipage}{0.72 \linewidth}
    \begin{itemize}
      \miniitem{0.58 \linewidth}{$I \models A \iff I \models \fa{x} A$}
      \miniitem{0.40 \linewidth}{$\models A \iff \models \fa{x} A$}
    \end{itemize}
  \end{minipage}
\end{prop}

\begin{defn}
  Sei $x$ eine Variable und $t \in \Term$ ein Term. Dann ist die Substitution $[\subst{t}{x}]$ für Terme und Formeln folgendermaßen definiert:
  \begin{alignat*}{2}
    y[\subst{t}{x}] & \coloneqq \begin{cases}
      t, & \text{falls } y = x \\
      y, & \text{sonst}
    \end{cases} \\
    f(t_1, ..., t_n)[\subst{t}{x}] & \coloneqq f(t_1[\subst{t}{x}], ..., t_n[\subst{t}{x}]) \quad \text{für $f \in \mathcal{F}^n$} \\
    P(t_1, ..., t_n)[\subst{t}{x}] & \coloneqq P(t_1[\subst{t}{x}], ..., t_n[\subst{t}{x}]) \quad \text{für $P \in \mathcal{P}^n$} \\
    (t_1 = t_2)[\subst{t}{x}] & \coloneqq (t_1[\subst{t}{x}] = t_2[\subst{t}{x}]) \\
    (\neg A)[\subst{t}{x}] & \coloneqq \neg (A[\subst{t}{x}]) \\
    (A \to B)[\subst{t}{x}] & \coloneqq A[\subst{t}{x}] \to A[\subst{t}{x}] \\
    (\fa{y} A)[\subst{t}{x}] & \coloneqq \begin{cases}
      \fa{y} A, & \text{falls $x = y$} \\
      \fa{y} (A[\subst{t}{x}]), & \text{sonst und falls $y \not\in \FV(t)$} \\
      \fa{z} (A[\subst{z}{y}][\subst{t}{x}]), & \text{sonst}
    \end{cases}
  \end{alignat*}
  Im letzten Fall ist $z$ eine frische Variable, \dh{} $z \not\in \FV(t) \cup \FV(A)$.
\end{defn}

% Kapitel 3.2. Der Kalkül

\begin{defn}
  Der \emph{Hilbert-Kalkül} für Prädikatenlogik hat als Axiome für alle $A, B, C \in \For$ und $t \in \Term$ alle Generalisierungen von
  \begin{alignat*}{3}
    \Ax_1,\,&\Ax_2,\Ax_3 : \text{wie zuvor}\\
    \Ax_4 :\, & (\fa{x} A) \to A[\subst{t}{x}] && \text{(\textbf{SP}ezialisierung)}\\
    \Ax_5 :\, & A \to \fa{x} A, \quad \text{falls $x \not\in \FV(A)$} && \text{(\textbf{GE}neralisierung)}\\
    \Ax_6 :\, & (\fa{x} A \to B) \to ((\fa{x} A) \to (\fa{x} B)) \enspace && \text{(\textbf{D}istr. \textbf{A}llquantor)}\\
    \Ax_7 :\, & x = x && \text{(\textbf{RE}flexivität)}\\
    \Ax_8 :\, & (x = y) \to (A \to A') && \text{(\textbf{GL}eichheit)},
  \end{alignat*}
  wobei bei der letzten Regel $A$ quantorenfrei ist und $A'$ aus $A$ durch Ersetzen eines oder mehrerer Vorkommen von $x$ durch $y$ entsteht. Außerdem gilt die Schlussregel \emph{Modus Ponens}.
\end{defn}

% Ausgelassen: Satz 3.10.

% 3.11.
\begin{satz}[Deduktionstheorem]
  Wir beim Hilbert-Kalkül der Aussagenlogik gilt für $M \subset \For$ und $A, B \in \For$:
  \[ M \vdash A \to B \iff M \cup \{ A \} \vdash B \]
\end{satz}

% 3.12.
\begin{satz}[Generalisierungstheorem]
  Sei $M \subset \For$, $A \in \For$ und $M \vdash A$. Angenommen, es gilt $\fa{B \in M} x \not\in \FV(B)$. Dann gilt $M \vdash \fa{x} A$.
\end{satz}

% 3.13.
\begin{kor}
  $\vdash A \implies \vdash \fa{x} A$
\end{kor}

% 3.14.
\begin{prop}[$\alpha$-Konversion]
  Sei $y \notin \FV(\fa{x} A)$. Dann gilt
  \[ \vdash (\fa{x} A) \to (\fa{y} A[\subst{y}{x}]). \]
\end{prop}

% Kapitel 3.3. Korrektheit und Vollständigkeit

% 3.15.
\begin{satz}[Korrektheit]
  Es gilt für alle $M \subset \For$ und $A \in \For$:
  \[ M \vdash A \implies M \models A. \]
\end{satz}

% 3.16.
\begin{lem}
  Für $M \subset \For$ und $A \in \For$ gilt:
  \begin{itemize}
    \item $M \not\vdash A \implies M \cup \{ \neg A \}$ ist konsistent.
    \item $M \not\vdash \fa{x} A \implies M \cup \{ \neg \fa{x} A, \neg A[\subst{c}{x}] \}$ ist konsisten für jede Variable $c$, die nicht in $M$ und $A$ vorkommt.
  \end{itemize}
\end{lem}

% 3.17.
\begin{lem}[Modell-Lemma]
  konsistent $\iff$ erfüllbar
\end{lem}

% 3.18.
\begin{satz}[Löwenheim-Skolem]
  Jede erfüllbare Menge $M$ geschlossener Formeln hat ein höchstens abzählbares Modell bzw. im Falle von Logik ohne Gleichheit ein abzählbar unendliches Modell.
\end{satz}

% 3.19.
\begin{satz}[Vollständigkeit]
  Es gilt für alle $M \subset \For$ und $A \in \For$:
  \[ M \models A \implies M \vdash A. \]
\end{satz}

% 3.20.
\begin{satz}[Endlichkeits- bzw. Kompaktheitssatz der Prädikatenlogik]
  Sei $A \in \For$, $M \subset \For$.
  \begin{itemize}
    \item Dann gilt $M \models A$ genau dann, wenn es eine endliche Teilmenge $M' \subset M$ mit $M' \models A$ gibt.
    \item Dann ist $M$ genau dann erfüllbar, wenn jede endliche Teilmenge von $M$ erfüllbar ist.
  \end{itemize}
\end{satz}

\begin{bem}
  Die Menge der gültigen Formeln ist aufzählbar bzw. semi-entscheidbar.
\end{bem}

\begin{satz}[Church]
  Das Gültigkeitsproblem der Prädikatenlogik erster Stufe ist unentscheidbar.
\end{satz}

\begin{samepage}

\begin{kor}
  Es gibt kein $A \in \For$ mit
  \begin{itemize}
    \item $I \models A \iff$ $D_I$ ist endlich.
    \item Bei Logik ohne Gleichheit: $I \models A \iff \abs{D_I} = n$ für ein festes $n \in \N$.
  \end{itemize}
\end{kor}

\section{Weitere Beweisverfahren}

\end{samepage}

% Kapitel 4.1. Sequenzenkalkül

\begin{defn}
  Im \emph{Gentzen-Kalkül} ($\vdash_G$) gelten die folgenden Schlussregeln:

  \begin{tabular}{ r c l}
    rechts && links \\[8pt]

    \AxiomC{$M \cup \{ A \} \vdash_G B$}\UnaryInfC{$M \vdash A \to B$}\DisplayProof &
    Imp &
    \AxiomC{$M \cup \{ \neg C \} \vdash_G A\nspace{10}$}\AxiomC{$M \cup \{ B \} \vdash_G C$}\BinaryInfC{$M \cup \{ A \to B \} \vdash_G C$}\DisplayProof \\[8pt]

    \AxiomC{$M \cup \{ A \} \vdash_G \neg B$}\UnaryInfC{$M \cup \{ B \} \vdash_G \neg A$}\DisplayProof &
    Neg &
    \AxiomC{$M \cup \{ \neg B \} \vdash_G A$}\UnaryInfC{$M \cup \{ \neg A \} \vdash_G B$}\DisplayProof \\[8pt]

    \AxiomC{$M \vdash_G A\nspace{10}$}\AxiomC{$M \vdash_G B$}\BinaryInfC{$M \vdash_G A \wedge B$}\DisplayProof &
    Kon &
    \AxiomC{$M \cup \{ A, B \} \vdash_G C$}\UnaryInfC{$M \cup \{ A \wedge B \} \vdash_G C$}\DisplayProof \\[8pt]

    \AxiomC{$M \cup \{ \neg B \} \vdash_G A$}\UnaryInfC{$M \vdash_G A \vee B$}\DisplayProof &
    Dis &
    \AxiomC{$M \cup \{ A \} \vdash_G C\nspace{10}$}\AxiomC{$M \cup \{ B \} \vdash_G C$}\BinaryInfC{$M \cup \{ A \vee B \} \vdash_G C$}\DisplayProof
  \end{tabular}

  \begin{center}
    \AxiomC{\phantom{a}}\UnaryInfC{$M \cup \{ A \} \vdash_G A$}\DisplayProof (Axiom)
  \end{center}
\end{defn}

\begin{satz}[Korrektheit, Vollständigkeit]
  Es gilt für alle $A \in \For$ und $M \subset \For$: $M \vdash_G A \iff M \models A$.
\end{satz}

% Kapitel 4.2. Resolution

\begin{nota}
  Für ein Literal $l$ bezeichnet $\overline{l}$ das \emph{negierte Literal}, also
  \[ \overline{p} \coloneqq \neg p, \quad \overline{\neg p} \coloneqq p. \]
\end{nota}

\begin{defn}
  Sei $A$ eine Formel in KNF mit Klauseln $K$ und $K'$, sodass ein Literal $l$ existiert mit $l \in K$ und $\overline{l} \in K'$. Dann heißt
  \[
    R = (K \setminus \{ l \}) \cup (K' \setminus \{ \overline{l} \})
    \quad \text{\emph{Resolvente} von $K$ und $K'$.}
  \]
\end{defn}

\begin{defn}
  Ein \emph{Resolutionsschritt} fügt eine Resolvente einer Formel in KNF der Formel hinzu. Die Formel, die aus einer Formel $A$ durch mehrere Resolutionsschritte entsteht, sodass keine weiteren Resolutionsschritte möglich sind, wird mit $\Res^*(A)$ bezeichnet.
\end{defn}

% 4.1.
\begin{lem}
  Sei $A$ eine Formel in KNF mit Klauseln $K$ und $K'$ und einer Resolvente $R = (K \setminus \{ l \}) \cup (K' \setminus \{ \overline{l} \})$. Dann ist $A$ genau dann erfüllbar, wenn $A \cup R$ es ist.
\end{lem}

% 4.2.
\begin{satz}[Resolutionssatz]
  Eine KNF-Formel $A$ ist genau dann unerfüllbar, wenn $\emptyset \in \Res^*(A)$.
\end{satz}

\section{Zusicherungskalkül}

\begin{defn}
  Ein \emph{Hoare-Tripel} hat die Form
  \[ \HoareT{A}{S}{B}, \]
  wobei $A$ und $B$ prädikatenlogische Formeln, sogenannte \emph{Zusicherungen}, und $S$ eine Programmanweisung ist.
\end{defn}

% Kapitel 5.1. Semantik

\begin{defn}
  \begin{itemize}
    \item Ein Hoare-Tripel $\HoareT{A}{S}{B}$ \emph{gilt schwach}, wenn $B$ nach Ausführung von $S$ unter der Vorbedingung $A$ gilt, falls $S$ ohne Fehlerabbruch terminiert.
    \item Gilt das Hoare-Tripel schwach und sichert die Vorbedingung $A$ die Terminierung ohne Fehler von $S$, so gilt das Tripel \emph{streng}.
  \end{itemize}
\end{defn}

% Kapitel 5.2. Zusicherungskalkül

\begin{samepage}

\begin{defn}
  Im \emph{Zusicherungskalkül} (Hoare-Kalkül) gelten folgende Schlussregeln:
  \begin{center}
    % Zuweisungsaxiom
    \scalebox{0.88}{\AxiomC{\phantom{a}}\UnaryInfC{$\HoareT{B[\subst{E}{x}]}{x = E;}{B}$}\DisplayProof} \  (=p) \enspace
    \scalebox{0.88}{\AxiomC{\phantom{a}}\UnaryInfC{$\HoareT{D_E \wedge B[\subst{E}{x}]}{x = E;}{B}$}\DisplayProof} \  (=t)

    % Konsequenzregel
    \scalebox{0.88}{\AxiomC{$A \Rightarrow B\nspace{10}$}\AxiomC{$\HoareT{B}{S}{C}\nspace{10}$}\AxiomC{$C \Rightarrow D$}\TrinaryInfC{$\HoareT{A}{S}{D}$}\DisplayProof} (K)
    \enspace
    % Sequentielle Komposition
    \scalebox{0.88}{\AxiomC{$\HoareT{A}{S}{B}\nspace{10}$}\AxiomC{$\HoareT{B}{T}{C}$}\BinaryInfC{$\HoareT{A}{S; T}{C}$}\DisplayProof} (sK)

    % bedingte Anweisung
    \scalebox{0.88}{\AxiomC{$\HoareT{A \wedge B}{S}{C}\nspace{10}$}\AxiomC{$\HoareT{A \wedge \neg B}{T}{C}$}\BinaryInfC{$\HoareT{A}{\text{if } (B) \text{ then } S \text{ else } T }{C}$}\DisplayProof} \  (if)

    % while-Schleifen
    \scalebox{0.88}{\AxiomC{$\HoareT{A \wedge B}{S}{A}$}\UnaryInfC{$\HoareT{A}{\text{while } (B) \text{ do } S}{A \wedge \neg B}$}\DisplayProof} \  (Wp)

    \scalebox{0.88}{\AxiomC{$\fa{z \in \Z} \HoareT{A \wedge B \wedge t = z}{S}{A \wedge t < z}\nspace{10}$}\AxiomC{$A \wedge B \implies t \geq 0$}\BinaryInfC{$\HoareT{A}{\text{while } (B) \text{ do } S}{A \wedge \neg B}$}\DisplayProof} \  (Wt)
  \end{center}
\end{defn}

% Ausgelassen: Abgeleitete Schlussregeln für Schleifen

% Kapitel 5.3. Verwendungsmöglichkeiten des Zusicherungskalküls
% (nichts interessantes)

\section{Temporale Logik}

\end{samepage}

% Kapitel 6.1. LTL

\begin{defn}
  Ein \emph{Ablauf} $\pi = s_0, s_1, ...$ ist eine unendliche Folge von Zuständen aus einer Menge $S$ mit einer Bewertung $L : S \to \mathfrak{P}(\mathcal{P})$.
\end{defn}

\begin{nota}
  $\pi^j \coloneqq s_j, s_{j+1}, ...$ heißt \emph{$j$-tes Suffix} von $\pi$.
\end{nota}

\begin{defn}
  Sei $\mathcal{P}$ eine Menge von atomaren Formeln. Dann sind Formeln in (P)LTL (Propositional Linear Time Logic) über $\mathcal{P}$ definiert als kleinste Menge $\TFor_{\mathcal{P}}$ mit
  \begin{itemize}
    \miniitem{0.3 \linewidth}{$\mathcal{P} \subset \TFor_{\mathcal{P}}$}
    \miniitem{0.68 \linewidth}{$\fa{A \in \TFor_{\mathcal{P}}} \{ \G A, \F A, \X A \} \subset \TFor_{\mathcal{P}}$}
    \item $\fa{A, B \in \TFor_{\mathcal{P}}} \{ \neg A, A \wedge B, A \vee B, A \to B, A \lra B \} \subset \TFor_{\mathcal{P}}$
    \item $\fa{A, B \in \TFor_{\mathcal{P}}} (A \U B) \in \TFor_{\mathcal{P}}$
  \end{itemize}
\end{defn}

\begin{samepage}

\begin{defn}
  Sei $\pi = s_0, s_1, ...$ ein Ablauf. Eine Formel $A \in \TFor$ gilt für $\pi$ ($\pi$ erfüllt $A$, $\pi \models A$), falls gilt:
  \begin{alignat*}{3}
    & \pi \models p &&\coloniff p \in L(s_0)\\[-2pt]
    & \pi \models \neg A &&\coloniff \pi \not\models A\\[-2pt]
    & \pi \models A \vee B &&\coloniff (\pi \models A) \vee (\pi \models B)\\[-2pt]
    & \pi \models \X A &&\coloniff \pi^1 \models A\\[-2pt]
    & \pi \models \G A &&\coloniff \fa{j \in \N_0} \pi^j \models A\\[-2pt]
    & \pi \models \F A &&\coloniff \ex{j \in \N_0} \pi^j \models A\\[-2pt]
    & \pi \models A \U B &&\coloniff \ex{j \in \N_0} \pi^j \models B \wedge (\fa{i < j} \pi^i \models A)
  \end{alignat*}
\end{defn}

\begin{defn}
   Eine Formel $A \in \TFor$ heißt \emph{gültig} / \emph{erfüllbar}, falls alle Abläufe / ein Ablauf $A$ erfüllt.
\end{defn}

\end{samepage}

% 6.5.
\begin{prop}
  Für alle $A \in \TFor$ gilt:
  \begin{itemize}
    \miniitem{0.35 \linewidth}{$\G A \eqmodels \neg \F \neg A$}
    \miniitem{0.35 \linewidth}{$\F A \eqmodels true \U A$}
    \item $A \U B \eqmodels \neg ((\neg B) \U (\neg A \wedge \neg B)) \wedge \F B$
  \end{itemize}
\end{prop}

% 6.6.
\begin{satz}
  Für alle $A, B \in \TFor$ gilt:
  \begin{itemize}
    \miniitem{0.5 \linewidth}{$\models \G (A \to B) \to (\G A \to \G B)$}
    \miniitem{0.47 \linewidth}{$\models \X \G A \lra \G \X A$}
    \miniitem{0.5 \linewidth}{$\models (A \wedge \G (A \to \X A)) \to \G A$}
    \miniitem{0.47 \linewidth}{$\models \X \F A \to \F A$}
  \end{itemize}
\end{satz}

% Ausgelassen: Satz: Jede Eigenschaft ist Konjunktion einer Sicherheits- und einer Lebendigkeitseigenschaft

% 6.7.
\begin{defn}
  Eine \emph{Kripke-Struktur} $K = (S, \to, L, s_0)$ besteht aus einer Menge $S$ von Zuständen mit Startzustand $s_0$, einer Bewertung $L : S \to \mathfrak{P}(\mathcal{P})$ und einer Transitionsrelation $\to \, \subset S \times S$, sodass $\fa{s \in S} \ex{s' \in S} s \to s'$ gilt.
\end{defn}

\begin{defn}
  Ein \emph{Ablauf} $\pi$ von $K$ ist eine unendliche Folge von Zuständen beginnend mit $s_0$, also $\pi = s_0, s_1, s_2, ...$ mit $\forall{i \in \N_0} s_i \to s_{i+1}$. Die Zustände eines solchen Ablaufs heißen \emph{erreichbar}.
\end{defn}

\begin{defn}
  Eine Kripke-Struktur $K$ \emph{erfüllt} $A \in \TFor$, falls für alle Abläufe $\pi$ von $K$ gilt $\pi \models A$.
\end{defn}

% Kapitel 6.2. CTL

% Ausgelassen: 6.8 Syntax von CTL

\begin{samepage}

\begin{defn}
  Sei $\mathcal{P}$ eine Menge von atomaren Formeln. Dann sind Formeln in CTL (Computation Tree Logic) über $\mathcal{P}$ definiert als kleinste Menge $\CTFor_{\mathcal{P}}$ mit
  \begin{itemize}
    \item $\fa{A, B \in \TFor_{\mathcal{P}}} \{ \neg A, A \wedge B, A \vee B, A \to B, A \lra B \} \subset \CTFor_{\mathcal{P}}$
    \miniitem{0.23 \linewidth}{$\mathcal{P} \subset \CTFor_{\mathcal{P}}$}
    \miniitem{0.75 \linewidth}{$\fa{A,B {\in} \TFor_{\mathcal{P}}} \{ \A (A \U B), \E (A \U B) \} \subset \TFor_{\mathcal{P}}$}
    \item $\fa{A \in \TFor_{\mathcal{P}}} \{ \AG A, \AF A, \AX A, \EG A, \EF A, \EX A \} \subset \TFor_{\mathcal{P}}$
  \end{itemize}
\end{defn}

% 6.9.
\begin{defn}
  Sei $K$ eine Kripke-Struktur, $s$ ein Zustand. Eine Formel $A \in \CTFor$ \emph{gilt} für $(K, s)$, falls (koinduktive Definition)
  \begin{alignat*}{3}
    & K, s \models p &&\coloniff&& p \in L(s)\\[-2pt]
    & K, s \models \neg A &&\coloniff&& K, s \neg\models A\\[-2pt]
    & K, s \models A \vee &&\coloniff&& (K, s \models A) \vee (K, s \models B)\\[-2pt]
    & K, s \models \AX B &&\coloniff&& \fa{s' \in S} (s \to s') \Rightarrow K, s' \models B\\[-2pt]
    & K, s \models \EX B &&\coloniff&& \ex{s' \in S} (s \to s') \wedge (K, s' \models B)\\[-2pt]
    & K, s \models \AG B &&\coloniff&& K, s \models B \wedge \fa{s' \in S} (s \to s') \Rightarrow K, s' \models \AG B\\[-2pt]
    & K, s \models \EG B &&\coloniff&& K, s \models B \wedge \ex{s' \in S} (s \to s') \wedge (K, s' \models \EG B)\\[-2pt]
    & K, s \models \AF B &&\coloniff&& \fa{\text{Abläufe $\pi = s_0, s_1, s_2, ...$ von $K$ mit $s_0 = s$}} \\[-2pt]
      & && && \ex{j \in \N_0} K, s_j \models B \\[-2pt]
    & K, s \models \EF B &&\coloniff&& \ex{\text{Ablauf $\pi = s_0, s_1, s_2, ...$ von $K$ mit $s_0 = s$}} \\[-2pt]
      & && && \ex{j \in \N_0} K, s_j \models B \\[-2pt]
    & K, s \models \A (B \U C) &&\coloniff&& \fa{\text{Abläufe $\pi = s_0, s_1, s_2, ...$ von $K$ mit $s_0 = s$}} \\[-2pt]
    & && && \ex{j \in \N_0} (K, s_j \models C) \wedge (\fa{i < j} K, s_i \models B)\\[-2pt]
    & K, s \models \E (B \U C) &&\coloniff&& \ex{\text{Ablauf $\pi = s_0, s_1, s_2, ...$ von $K$ mit $s_0 = s$}} \\[-2pt]
    & && && \ex{j \in \N_0} (K, s_j \models C) \wedge (\fa{i < j} K, s_i \models B)
  \end{alignat*}
\end{defn}
  
\end{samepage}

\begin{nota}
  $K \models A \coloniff K, s_0 \models A$, wobei $s_0$ Startzustand von $K$.
\end{nota}

\begin{defn}
  Eine Formel $A \in \CTFor$ heißt \emph{gültig} / \emph{erfüllbar}, wenn alle Kripke-Strukturen / eine Kripke-Struktur $A$ erfüllen / erfüllt.
\end{defn}

% Ausgelassen: Satz 6.10.

\begin{samepage}

% 6.11.
\begin{satz}
  Für alle $B, C \in \CTFor$ gilt:
  \begin{itemize}
    \item $\models (B \wedge \AG (B \to \AX B)) \to \AG B$
    \item $\models \AX (B \to C) \wedge \AX B \to \AX C$
  \end{itemize}
\end{satz}

% 6.12.
\begin{satz}
  Für alle $A, B \in \CTFor$ gilt:
  \begin{itemize}
    \miniitem{0.40\linewidth}{$\AG B \eqmodels \neg \EF \neg B$}
    \miniitem{0.40\linewidth}{$\EG B \eqmodels \neg \AF \neg B$}
    \miniitem{0.40\linewidth}{$\EF B \eqmodels \E (true \U B)$}
    \miniitem{0.40\linewidth}{$\AF B \eqmodels \A (true \U B)$}
    \miniitem{0.34\linewidth}{$\AX B \eqmodels \neg \EX \neg B$}
    \miniitem{0.64\linewidth}{$\A (B \U C) \eqmodels \neg \E (\neg C \U (\neg C \wedge \neg B)) \wedge \AF C$}
  \end{itemize}
\end{satz}

% Kapitel 6.3. CTL-Model-Checking

% Ausgelassen: Beschreibung des Verfahrens

\section{Modale Logik}
  
\end{samepage}

\begin{defn}
  Sei $\mathcal{P}$ eine Menge von atomaren Formeln. Dann ist die Menge der Formeln in der modalen Logik definiert als kleinste Menge $\MFor_{\mathcal{P}}$ mit
  \begin{itemize}
    \item $\fa{A, B \in \MFor_{\mathcal{P}}} \{ \neg A, A \wedge B, A \vee B, A \to B, A \lra B \} \subset \MFor_{\mathcal{P}}$
    \miniitem{0.3 \linewidth}{$\mathcal{P} \subset \MFor_{\mathcal{P}}$}
    \miniitem{0.68 \linewidth}{$\fa{A \in \MFor_{\mathcal{P}}} \{ \square A, \diamond A \} \subset \MFor_{\mathcal{P}}$}
  \end{itemize}
\end{defn}

\begin{defn}
  Zustände in Kripke-Strukturen dürfen in diesem Kapitel auch keine Übergänge zu nächsten Zuständen besitzen, \dh{} es muss \textit{nicht} unbedingt gelten:
  \[ \fa{s \in S} \ex{s' \in S} s \to s'.\]
\end{defn}

\begin{defn}
  Für eine Kripke-Struktur mit Zustand $s$ und $A \in \MFor$ wird $K, s \models A$ analog zur CTL definiert, wobei $\square$ als $\AX$ und $\diamond$ wie $\EX$ behandelt wird.
\end{defn}

\begin{defn}
  Für eine Kripke-Struktur $K$ und $A \in \MFor_{\mathcal{P}}$ setzen wir
  \[ K \models A \coloniff \fa{s} K, s \models A. \]
\end{defn}

\begin{acht}
  Obige Definition weicht ab von der Definition in CTL!
\end{acht}

\begin{bem}
  Es gilt immer: \enspace \begin{minipage}{0.5\linewidth}\begin{itemize}\item $\models \square (A \to B) \wedge \square A \to \square B$\end{itemize}\end{minipage}
  \begin{itemize}
    \miniitem{0.44 \linewidth}{$\models \square (A \wedge B) \lra (\square A \wedge \square B)$}
    \miniitem{0.44 \linewidth}{$\models \diamond (A \vee B) \lra (\diamond A \vee \diamond B)$}
    \item $K, s \models \diamond true \iff \fa{A \in \MFor_{\mathcal{P}}} K, s \models \square A \to \diamond A$
  \end{itemize}
\end{bem}

\begin{defn}
  Ein \emph{Rahmen} $F = (S, \to)$ besteht aus einer Menge von Welten $S$ und einer Transitionsrelation $\to \, \subset S \times S$. Er \emph{erfüllt} eine modale Formel $A \in \MFor_{\mathcal{P}}$ genau dann, wenn jede Kripke-Struktur $K = (S, \to, L, s_0)$ mit $L : S \to \mathfrak{P}(\mathcal{P})$ beliebig $A$ erfüllt.
\end{defn}

\begin{defn}
  Eine Relation $\to \, \subset S \times S$ heißt \emph{euklidisch}, falls gilt:
  \[ \fa{s, s', s''} (s \to s') \wedge (s \to s'') \implies (s' \to s'') \]
\end{defn}

\begin{satz}
  Für jeden Rahmen $F = (S, \to)$ und jedes Atom $p$ gilt:
  \begin{itemize}
    \item $\to$ reflexiv $\Leftrightarrow$ $\fa{A\!}\!F$ erfüllt $\square A \to A$ $\Leftrightarrow$ $F$ erfüllt $\square p \to p$
    \item $\to$ transitiv $\Leftrightarrow$ $\fa{A\!}\!F$ erfüllt $\square A \to \square \square A$ $\Leftrightarrow$ $F$ erfüllt $\square p \to \square \square p$
    \item $\to$ euklidisch $\Leftrightarrow$ $\fa{A\!}\!F$ erfüllt $\diamond A \to \square \diamond A$ $\Leftrightarrow$ $F$ erfüllt $\diamond p \to \square \diamond p$.
  \end{itemize}
  Der Allquantor bezieht sich dabei auf alle $A \in \MFor_{\mathcal{P}}$.
\end{satz}

% Ausgelassen: Anwendung auf Wissen in Multi-Agenten-Systemen

\end{document}