Progress on 600

chapters/200_grundlagen.tex

@@ -492,7 +492,7 @@ \subsubsection{Inverse Rollen (\texorpdfstring{$\ALCI$}{ALCI})}\label{inverse-ro
 \begin{definition}[Inverse Rollen]
 Für jeden Rollennamen $r$ ist $r^{-}$ die \emph{inverse
 Rolle} zu $r$. Wir definieren
-\[\left( r^{-} \right)^\MI = \left\{ \left( e,d \right) \mid \left( d,e \right) \in r^\MI\} \]
+\[\left( r^{-} \right)^\MI = \{ \left( e,d \right) \mid \left( d,e \right) \in r^\MI\} \]
 \end{definition}
 
 \begin{tafel}[Beispiel Nützlichkeit von inversen Rollen]

chapters/300_ausdruckstaerke_etc.tex

@@ -93,6 +93,7 @@ \subsection{Bisimulation}\label{bisimulation}
                     \end{scope}
                 \end{tikzpicture}
             \end{center}
+    \end{enumerate}
 \end{tafel}
 
 Seien $\MI_1$ und $\MI_2$ Interpretationen,

chapters/400_tableau.tex

@@ -162,7 +162,7 @@ \subsubsection{Tableau-Algorithmus}\label{tableau-algorithmus}
     \item \enquote{unerfüllbar} andernfalls, also wenn es in \emph{allen} vollständigen I-Bäumen einen offensichtlichen Widerspruch gibt.
 \end{itemize}
 
-\begin{tafel}[Beispielanwendung des Tableau-Algorithmus]
+\begin{tafel}[Beispielanwendung des Tableau-Algorithmus, TODO]
 
 Beispiel:
 
@@ -381,15 +381,13 @@ \subsubsection{Korrektheit und Vollständigkeit}
 
 \item $C = D \sqcap E$
     \begin{align*}
-        &C \in \ML(v)\\
-        &\implies (\sqcap\text{-Regel nicht anwendbar}) D \in \ML(v), E \in \ML(v)\\
-        &\implies (\text{I.V.}) v \in D^\MI,\ v \in E^\MI\\
-        &\implies (\text{Semantik}) v \in \left( D \sqcap E \right)^\MI
+        C \in \ML(v)
+        &\implies D \in \ML(v), E \in \ML(v) && \text{($\sqcap$-Regel nicht mehr anwendbar)}\\
+        &\implies v \in D^\MI,\ v \in E^\MI && \text{(I.V.)}\\
+        &\implies  v \in \left( D \sqcap E \right)^\MI && (\text{Semantik})
     \end{align*}
 
-\item $C = D \sqcup E$
-
-analog zu $\sqcap$.
+\item $C = D \sqcup E$: analog zu $\sqcap$.
 
 \item $C = \exists r.D$
 
@@ -399,9 +397,7 @@ \subsubsection{Korrektheit und Vollständigkeit}
 Nach I.V. gilt $v' \in D^\MI$; nach Konstruktion $(v,v') \in r^\MI$, woraus
 $v \in (\exists r.D^\MI)$ folgt.
 
-\item $C = \forall r.D$
-
-analog zu $\exists$.
+\item $C = \forall r.D$: analog zu $\exists$.
 \end{itemize}
     \end{proof}
 \end{tafel}
@@ -410,9 +406,7 @@ \subsubsection{Korrektheit und Vollständigkeit}
     \label{def:realisierbarkeit}
 Sei $B = \left( V,E,\ML \right)$ ein I-Baum und $\MI$ eine Interpretation. $\MI$
 \emph{realisiert} $B$, wenn es eine Funktion
-\begin{align*}
-    \pi : V \rightarrow \Delta^\MI
-\end{align*}
+\[ \pi : V \rightarrow \Delta^\MI \]
 gibt, so dass gilt:
 \begin{itemize}
 \item
@@ -430,7 +424,7 @@ \subsubsection{Korrektheit und Vollständigkeit}
 
 Beachte: ein realisierbarer I-Baum enthält keinen offensichtlichen Widerspruch.
 
-\begin{tafel}[Beispiel Realisierbarkeit]\mbox{}\\
+\begin{tafel}[Beispiel Realisierbarkeit, TODO]\mbox{}\\
 
 \includegraphics[width=2.0in,height=4.0in]{media/47real.png}
 \end{tafel}
@@ -610,7 +604,7 @@ \subsubsection{Blockieren}\label{blockieren}
 blockierten Vorgänger hat. Beachte, dass \enquote{Vorgänger} kein direkter Vorgänger sein muss.
 \end{definition}
 
-\begin{tafel}[Beispiel Blockieren]\mbox{}\\
+\begin{tafel}[Beispiel Blockieren]\mbox{}
     \begin{center}
     \begin{tikzpicture}
         \begin{scope}[every node/.style={circle,thick,draw}]
@@ -655,7 +649,7 @@ \subsubsection{Blockieren}\label{blockieren}
   $\ML\left( v' \right) = \left\{ C \right\}$
 \end{itemize}
 
-\begin{tafel}[Beispiel $\exists'$-Regel]\mbox{}\\
+\begin{tafel}[Beispiel $\exists'$-Regel, TODO]\mbox{}\\
 
 \includegraphics[width=5.71910in,height=2.33200in]{media/414block.png}
 

chapters/500_komplexitaet.tex

@@ -1,8 +1,6 @@
 \subsection{Komplexität mit TBoxen, obere
 Schranke}\label{komplexituxe4t-mit-tboxen-obere-schranke}
 
-\subsubsection{Obere Schranke}
-
 Wir wollen zeigen:
 
 \begin{theorem}
@@ -47,10 +45,8 @@ \subsubsection{Syntaktische Typen}\label{synt-typ}
 
 Beispiel:
 
-Sei $C_0 = A$, $\MT = \{\top \sqsubseteq C_{\MT}\}$ mit $$C_{\MT} = \exists r.\exists r.A \sqcap \forall r.A' \sqcap (\neg A \sqcup \neg A')$$
-
-Dann ist $$sub(C_0, \MT) = \{A, C_{\MT}, \exists r.\exists r.A, \forall r.A',\neg A \sqcup \neg A', \exists r.A, A', \neg A, \neg A'\}$$
-
+Sei $C_0 = A$, $\MT = \{\top \sqsubseteq C_{\MT}\}$ mit \[C_{\MT} = \exists r.\exists r.A \sqcap \forall r.A' \sqcap (\neg A \sqcup \neg A') \]
+Dann ist \[ \sub(C_0, \MT) = \{A, C_{\MT}, \exists r.\exists r.A, \forall r.A',\neg A \sqcup \neg A', \exists r.A, A', \neg A, \neg A'\} \]
 Sei $M = \{C_{\MT}, \exists r.\exists r. A, \forall r.A', \neg A \sqcup \neg A'\}$
 
 Die Typen für $C_0$ und $\MT$ sind:
@@ -199,9 +195,7 @@ \subsubsection{Schlechte Typen}\label{schlechter-typ}
 Die Erfüllbarkeit von $C_0$ bezüglich $\MT$ folgt dann aus:
 
 Behauptung: Für alle $C \in \sub(C_0, \MT)$ und alle $t \in \Gamma_i$ gilt:
-\begin{align*}
-    C \in t \implies t \in C^\MI
-\end{align*}
+\[ C \in t \implies t \in C^\MI \]
 
 \begin{tafel}[name=Beweis der Behauptung, continues=t:example51]
     Die Behauptung impliziert das Lemma.
@@ -257,7 +251,7 @@ \subsubsection{Schlechte Typen}\label{schlechter-typ}
     \begin{tafel}[Beweis der Behauptung]
     Per Induktion über $i$:
 
-    IA $i = 0$ trivial: jedes Element von $\Gamma$ (semantischer Typ) ist auch syntaktischer Typ (erfüllt a-d).
+    IA $i = 0$ jedes Element von $\Gamma$ (semantischer Typ) ist auch syntaktischer Typ (erfüllt a-d).
 
     IS $i \rightarrow i + 1$: Gelte $\Gamma \subseteq \Gamma_i$, zu zeigen $\Gamma \subseteq \Gamma_{i + 1}$.
 
@@ -739,7 +733,7 @@ \subsubsection{\texorpdfstring{$\ALC$}{ALC}-Worlds}\label{alc-worlds}
     \begin{align*}
         \Delta^\MI &= V\\
         r^\MI &= \{(v, v') \in E \mid \sigma(v') = r\} \quad \text{für alle Rollennamen } r\\
-        A^\MI &= \{v \mid A \in p_1(v)\} \quad \text{für alle Konzeptnamen } A\\
+        A^\MI &= \{v \mid A \in p_1(v)\} \quad \text{für alle Konzeptnamen } A
     \end{align*}
     ($p_1(v)$ erster Parameter in $\ell(v)$)
 
@@ -754,12 +748,10 @@ \subsubsection{\texorpdfstring{$\ALC$}{ALC}-Worlds}\label{alc-worlds}
     $\ALC-\texttt{Worlds}(C_0)$, der \texttt{true} zurückgibt.
     \begin{proof}
         Sei $C_0$ erfüllbar und $\MI$ ein Modell von $C_0$ mit $d_0 \in C_0^\MI$. Für jedes $d \in \Delta^\MI$ und $i \geq 0$ definiere:
-        \begin{align*}
-            t_i(d) = \{C \in \sub_i(C_0) \mid d \in C^\MI\}
-        \end{align*}
+        \[ t_i(d) = \{C \in \sub_i(C_0) \mid d \in C^\MI\} \]
         Idee: Wir verwenden $\MI$, um die nichtdeterministischen Entscheidungen von $\ALC-\texttt{Worlds}(C_0)$ zu einem erfolgreichen Lauf zu \enquote{lenken}. Zu diesen Zweck übergeben wir eine Element $d \in \Delta^\MI$ als virtuelles viertes Argument $p_4$ an \texttt{recurse}, so dass für alle $v \in V$:
         \begin{align*}
-             \tag{*}
+             \tag{*r
              \label{eqn:alc-worlds-impl}
             C \in p_1(v) \implies p_4(v) \in C^\MI
         \end{align*}