%% LyX 1.3 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[10pt,twocolumn,german]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{geometry}
\geometry{verbose,a4paper,tmargin=1mm,bmargin=1mm,lmargin=1mm,rmargin=1mm,headheight=1mm,headsep=1mm,footskip=1mm}
\pagestyle{empty}
\setlength\parskip{0mm}
\setlength\parindent{0pt}
\usepackage{amsmath}
\usepackage{amssymb}
\IfFileExists{url.sty}{\usepackage{url}}
                      {\newcommand{\url}{\texttt}}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
\newcommand{\noun}[1]{\textsc{#1}}
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usepackage{gastex}
%\renewcommand{\thesubsubsection}{\alph{subsubsection})}
\usepackage[linktocpage,pdfpagelabels,colorlinks,hyperindex]{hyperref}
%\usepackage[dvips,ps2pdf,pdfpagelabels]{hyperref}
\usepackage[T1]{fontenc}
\usepackage{ae,aecompl}

\usepackage{babel}
\makeatother
\begin{document}

\paragraph{Formelblatt FGDI 3}

\textsf{<Marco.Moeller@macrolab.de>}

\textsf{Stand: 06.03.2006 - Version: 1.0.0}\\
\textsf{\noun{Erhältlich unter \url{http://privat.macrolab.de}}}

\textsf{Diese Formelsammlung basiert auf der Vorlesung {}``Formale
Grundlagen der Informatik - 3'' von Prof. Dr. Christoph Walther an
der Technischen Universität Darmstadt im Wintersemester 2005/06.}

\textsf{Die folgende Formelsammlung steht zum kostenlosen Download
zur Verfügung. Das Urheberrecht und sonstige Rechte an dem Text verbleiben
beim Verfasser, der keine Gewähr für die Richtigkeit und Vollständigkeit
der Inhalte übernehmen kann.}


\section{Korrektheit Reaktiver Systeme}

\begin{description}
\item [Transitionssystem]\textsf{$\mathcal{T}=\left(S,\rightarrow,r\right)$}

\begin{description}
\item [Zustände]\textsf{$S$}
\item [Transitionsrelation]\textsf{$\rightarrow\subseteq S\times S$}
\end{description}
\begin{itemize}
\item \textsf{infix notiert: $s\rightarrow t\Leftrightarrow\left(s,t\right)\in\rightarrow$}
\end{itemize}
\begin{description}
\item [Anfangszustand]\textsf{$r\in S$a}
\item [Pfad]\textsf{der Länge $n$, mit $\forall i,0\le i\le n:s_{i}\rightarrow s_{i+1}$\[
w=s_{0}\ldots s_{n}\]
}
\item [Ausführung]\textsf{falls $\forall i,0\le i:s_{i}\rightarrow s_{i+1}$\[
p=s_{0}s_{1}\ldots\]
}
\item [Wörter]\textsf{$S^{*}$sind endlich, $S^{\omega}$ sind unendlich}
\item [Element]\textsf{$\rho\left(i\right)$ ist das $i$-te Element von
$\rho$ (ab $0$ Zählen!)}
\item [Suffix]\textsf{$\rho^{i}$ ist das bei $i$ beginnende suffix von
$\rho$ (ab $0$ Zählen!)}
\end{description}
\item [Kripke~Struktur]\textsf{$\mathcal{K}=\left(S,\rightarrow,r,AP,\nu\right)$}

\begin{description}
\item [Transitionssystem]\textsf{das zugrunde liegt $\left(S,\rightarrow,r\right)$}
\item [Grundaussagen]\textsf{Menge $AP$}
\item [Interpretationen]\textsf{der Grundaussagen $\nu:AP\rightarrow2^{S}$}
\end{description}
\begin{itemize}
\item \textsf{Die Zustände haben als eine Menge von Flags}
\end{itemize}
\begin{description}
\item [Bild]\textsf{$\nu^{-1}\left(\rho\right)\in\left(2^{AP}\right)^{\omega}$
kann jeder Ausführung $\rho$ zugeordnet werden: $\nu^{-1}\left(\rho\right)\left(i\right)=\left\{ a\in AP|\rho\left(i\right)\in\nu\left(a\right)\right\} $}
\item [erfüllt]\textsf{$\mathcal{K}$ erfüllt eine LTL Formel $\phi$ (geschrieben
$\mathcal{K}\models\phi$) falls für alle bei $r$ beginnenden Ausführungen
$\rho$ gilt, dass $\nu^{-1}\left(\rho\right)\subseteq\left[\left[\phi\right]\right]$}
\end{description}
\begin{itemize}
\item \textsf{Es kann sowohl $\mathcal{K}\nvDash\phi$ als auch $\mathcal{K}\models\phi$
gelten!}
\end{itemize}
\item [LTL]\textsf{Formeln}
\end{description}
\begin{itemize}
\item \textsf{Ist $a\in AP$ so ist $a$ eine Formel}
\item \textsf{Sind $\phi_{1},\phi_{2}$ Formeln, so auch $\neg\phi_{1},\phi_{1}\vee\phi_{2},\textrm{X}\phi_{1},\phi_{1}\textrm{U}\phi_{2}$}
\item \textsf{Jede Formel definiert eine Menge von Wörtern aus $\left(2^{AP}\right)^{\omega}$.
Sei $\sigma\in\left(2^{AP}\right)^{\omega}$}
\item \textsf{Semantik $\left[\left[\phi\right]\right]=\left\{ \sigma|\sigma\models\phi\right\} $}\\
\textsf{}\begin{tabular}{l|l}
\textsf{gilt}&
\textsf{falls}\tabularnewline
\hline
\textsf{$\sigma\models a$}&
\textsf{$a\in\sigma\left(0\right)$}\tabularnewline
\textsf{$\sigma\models\neg\phi$}&
\textsf{$\sigma\nvDash\phi$}\tabularnewline
\textsf{$\sigma\models\phi_{1}\vee\phi_{2}$}&
\textsf{$\sigma\models\phi_{1}$ oder $\sigma\models\phi_{2}$}\tabularnewline
\textsf{$\sigma\models\textrm{X}\phi$}&
\textsf{$\sigma^{1}\models\phi$}\tabularnewline
\textsf{$\sigma\models\phi_{1}\textrm{U}\phi_{2}$}&
\textsf{$\exists i:\left(\sigma^{i}\models\phi_{2}\wedge\forall k<i:\sigma^{k}\models\phi_{1}\right)$}\tabularnewline
\end{tabular}
\item \textsf{$\phi_{1}\wedge\phi_{2}\equiv\neg\left(\neg\phi_{1}\vee\neg\phi_{2}\right)$}
\item \textsf{$\textrm{true}\equiv a\vee\neg a$}
\item \textsf{$\textrm{false}\equiv\neg\textrm{true}$}
\item \textsf{$\textrm{F}\phi\equiv\textrm{true U}\phi$}
\item \textsf{$\textrm{G}\phi\equiv\neg\textrm{F}\neg\phi$}
\item \textsf{$\phi_{1}\textrm{W}\phi_{2}\equiv\left(\phi_{1}\textrm{U}\phi_{2}\right)\vee\textrm{G}\phi_{1}$}
\item \textsf{$\phi_{1}\textrm{R}\phi_{2}\equiv\neg\left(\neg\phi_{1}\textrm{U}\neg\phi_{2}\right)$}
\item \textsf{$\textrm{X}\left(\phi_{1}\vee\phi_{2}\right)\equiv\textrm{X}\phi_{1}\vee\textrm{X}\phi_{2}$}
\item \textsf{$\textrm{X}\left(\phi_{1}\wedge\phi_{2}\right)\equiv\textrm{X}\phi_{1}\wedge\textrm{X}\phi_{2}$}
\item \textsf{$\textrm{X}\neg\phi\equiv\neg\textrm{X}\phi$}
\item \textsf{$\textrm{F}\left(\phi_{1}\vee\phi_{2}\right)\equiv\textrm{F}\phi_{1}\vee\textrm{F}\phi_{2}$}
\item \textsf{$\textrm{G}\neg\phi\equiv\neg\textrm{F}\phi$}
\item \textsf{$\textrm{G}\left(\phi_{1}\wedge\phi_{2}\right)\equiv\textrm{G}\phi_{1}\wedge\textrm{G}\phi_{2}$}
\item \textsf{$\left(\phi_{1}\wedge\phi_{2}\right)\textrm{U}\psi\equiv\left(\phi_{1}\textrm{U}\psi\right)\wedge\left(\phi_{2}\textrm{U}\psi\right)$}
\item \textsf{$\phi\textrm{U}\left(\psi_{1}\vee\psi_{2}\right)\equiv\left(\phi\textrm{U}\psi_{1}\right)\vee\left(\phi\textrm{U}\psi_{2}\right)$}
\item \textsf{$\textrm{F}\phi\equiv\textrm{FF}\phi$}
\item \textsf{$\textrm{G}\phi\equiv\textrm{GG}\phi$}
\item \textsf{$\phi\textrm{U}\psi\equiv\phi\textrm{U}\left(\phi\textrm{U}\psi\right)$}
\item \textsf{$\textrm{F}\equiv\phi\vee\textrm{XF}\phi$}
\item \textsf{$\textrm{G}\equiv\phi\wedge\textrm{XG}\phi$}
\item \textsf{$\phi\textrm{U}\psi\equiv\psi\vee\left(\phi\wedge\textrm{X}\left(\phi\textrm{U}\psi\right)\right)$}
\item \textsf{$\phi\textrm{W}\psi\equiv\psi\vee\left(\phi\wedge\textrm{X}\left(\phi\textrm{W}\psi\right)\right)$}
\end{itemize}
\begin{description}
\item [Büchi-Automat]\textsf{$\mathcal{B}=\left(Q,\Sigma,\delta,q_{0},F\right)$}

\begin{description}
\item [Zustandsmenge]\textsf{(endlich) $Q$}
\item [Alphabet]\textsf{(endlich) $\Sigma$}
\item [Übergangsrelation]\textsf{$\delta\subseteq Q\times\Sigma\times Q$}
\item [Anfangszustand]\textsf{$q_{0}\in Q$}
\item [akzeptierende]\textsf{Zustände $F\subseteq Q$}
\item [akzeptiert]\textsf{$\mathcal{B}$ akzeptiert $a_{0}a_{1}\ldots\in\Sigma^{\omega}$,
gdw. }
\end{description}
\begin{itemize}
\item \textsf{$\left(q_{i},a_{i},q_{i+1}\right)\in\delta$ für alle $i\ge0$}
\item \textsf{Es gilt $q_{i}\in F$ für unendlich viele $i$}
\end{itemize}
\begin{description}
\item [Sprache]\textsf{$\mathcal{L}\left(\mathcal{B}\right)=\left\{ \sigma\in\Sigma^{\omega}|\mathcal{B}\textrm{ akzeptiert }\sigma\right\} $}
\end{description}
\begin{itemize}
\item \textsf{von Büchi Automaten erkannte Sprachen heißen $\omega$-regulär}
\end{itemize}
\begin{description}
\item [Generalisierter~Büchi~Automat]\textsf{hat eine Menge $\mathcal{F}=\left\{ F_{1},\ldots,F_{n}\right\} $
von Akzeptanzmengen. Er akzeptiert, falls unenedlich viele zustände
in $F_{i}$ für} \textsf{\emph{jedes}} \textsf{$i$.}
\end{description}
\item [markiertes~Produckt]\textsf{$\mathcal{B}_{1}\times\mathcal{B}_{2}=\left(Q,\Sigma,\delta,q_{0},F\right)$}

\begin{description}
\item [gegeben]\textsf{$\mathcal{B}_{1}=\left(Q_{1},\Sigma,\delta_{1},q_{1},F_{1}\right)$
und $\mathcal{B}_{2}=\left(Q_{2},\Sigma,\delta_{2},q_{2},F_{2}\right)$}
\end{description}
\end{description}
\begin{itemize}
\item \textsf{$Q=Q_{1}\times Q_{2}\times\left\{ 1,2\right\} $}\\
\textsf{}\begin{tabular}{c|ccc}
\textsf{gilt}&
\multicolumn{3}{c}{\textsf{falls}}\tabularnewline
\textsf{$\in\delta$}&
\textsf{$\in\delta_{1}$}&
\textsf{$\in\delta_{2}$}&
\tabularnewline
\hline
\textsf{$\left(\left\langle s,t,1\right\rangle ,a,\left\langle s',t',1\right\rangle \right)$}&
\textsf{$\left(s,a,s'\right)$ }&
\textsf{$\left(t,a,t'\right)$ }&
\textsf{$s\notin F_{1}$}\tabularnewline
\textsf{$\left(\left\langle s,t,1\right\rangle ,a,\left\langle s',t',2\right\rangle \right)$}&
\textsf{$\left(s,a,s'\right)$}&
\textsf{$\left(t,a,t'\right)$}&
\textsf{$s\in F_{1}$}\tabularnewline
\textsf{$\left(\left\langle s,t,2\right\rangle ,a,\left\langle s',t',2\right\rangle \right)$}&
\textsf{$\left(s,a,s'\right)$}&
\textsf{$\left(t,a,t'\right)$}&
\textsf{$t\notin F_{2}$}\tabularnewline
\textsf{$\left(\left\langle s,t,2\right\rangle ,a,\left\langle s',t',1\right\rangle \right)$}&
\textsf{$\left(s,a,s'\right)$ }&
\textsf{$\left(t,a,t'\right)$}&
\textsf{$t\in F_{2}$}\tabularnewline
\end{tabular}
\item \textsf{$q_{0}=\left\langle q_{1},q_{2},1\right\rangle $}
\item \textsf{$F=F_{1}\times Q_{2}\times\left\{ 1\right\} $}
\end{itemize}
\begin{description}
\item [LTL~$\rightarrow$generalisierter~Büchi]~

\begin{description}
\item [gegeben]\textsf{LTL-Formel $\phi$ in Normalform, d.h. Negationen
sind nach Innen geschoben.}
\item [gesucht]\textsf{$\mathcal{B}_{\phi}=\left(Q,\Sigma,\delta,q,F\right)$}
\item [Abschluss]\textsf{$Cl\left(\phi\right)$ einer Formel $\phi$ ist
die Menge aller Unterformeln von $\phi$ und ihrer Negierungen}
\item [Alphabet]\textsf{$\Sigma=2^{AP}$ mit $AP$ den Atomen von $\phi$}
\item [Zustände]\textsf{$Q=$ Elemente von $2^{Cl\left(\phi\right)}$,
die folgende Zusatzbedingungen erfüllen}
\end{description}
\begin{itemize}
\item \textsf{$\forall\phi_{1}\in Cl\left(\phi\right):\neg\phi_{1}\in Q\Leftrightarrow\phi_{1}\notin Q$}
\item \textsf{$\forall\phi_{1}\wedge\phi_{2}\in Cl\left(\phi\right):\phi_{1}\wedge\phi_{2}\in Q\Leftrightarrow\phi_{1}\in Q\wedge\phi_{2}\in Q$}
\item \textsf{$\forall\phi_{1}\vee\phi_{2}\in Cl\left(\phi\right):\phi_{1}\vee\phi_{2}\in Q\Leftrightarrow\phi_{1}\in Q\vee\phi_{2}\in Q$}
\end{itemize}
\begin{description}
\item [Anfangszustände,]\textsf{alle die $\phi$ enthalten}
\item [Übergänge]\textsf{$s{{l\atop \rightarrow}}t$, falls $l=\left\{ p\in AP|p\in s\right\} $,
sowie}
\end{description}
\begin{itemize}
\item \textsf{$\forall\textrm{X}\phi_{1}\in Cl\left(\phi\right):\textrm{X}\phi_{1}\in s\Leftrightarrow\phi_{1}\in t$}
\item \textsf{$\forall\phi_{1}\textrm{U}\phi_{2}\in Cl\left(\phi\right):\phi_{1}\textrm{U}\phi_{2}\in s\Leftrightarrow\phi_{2}\in s\vee\left(\phi_{1}\in s\wedge\phi_{1}\textrm{U}\phi_{2}\in t\right)$}
\item \textsf{$\forall\phi_{1}\textrm{R}\phi_{2}\in Cl\left(\phi\right):\phi_{1}\textrm{R}\phi_{2}\in s\Leftrightarrow\phi_{1}\wedge\phi_{2}\in s\vee\left(\phi_{2}\in s\wedge\phi_{1}\textrm{R}\phi_{2}\in t\right)$}
\end{itemize}
\begin{description}
\item [Akzeptierende~Zustände]\textsf{Für jede Unterformel der Form $\psi\equiv\phi_{1}\textrm{U}\phi_{2}$
gibt es eine Akzeptanzmenge $F_{\psi}$ wie folgt:}
\end{description}
\begin{itemize}
\item \textsf{$F_{\psi}$ ist die Menge der Zustände, die $\phi_{2}$ oder
$\neg\phi_{1}\textrm{R}\neg\phi_{2}$ enthalten}
\end{itemize}
\item [Kripke~$\rightarrow$~Büchi]~
\end{description}
\begin{itemize}
\item \textsf{gegeben: $\mathcal{K}=\left(S,\rightarrow,r,AP,\nu\right)$}
\item \textsf{gesucht: $\mathcal{B}_{\mathcal{K}}=\left(Q,\Sigma,\delta,q,F\right)$}
\item \textsf{$F=Q=S$}
\item \textsf{$\Sigma=2^{AP}$}
\item \textsf{$\left(s,A,s'\right)\in\delta$ $\Leftrightarrow$ $s\rightarrow s'$
und $A=\left\{ p\in AP|s\in\nu\left(p\right)\right\} $}
\item \textsf{$q=r$}
\item \textsf{$\mathcal{K}\models\phi\Leftrightarrow\mathcal{L}\left(\mathcal{B_{K}}\right)\subseteq\left[\left[\phi\right]\right]\Leftrightarrow\mathcal{L}\left(\mathcal{B_{K}}\times\mathcal{B}_{\neg\phi}\right)=\emptyset$}

\begin{itemize}
\item \textsf{$\mathcal{L}\neq\emptyset$ wenn Graph von $\ldots$ enthält
als Kreise mit Enzustand drin die erreichbar vom Start sind}
\end{itemize}
\begin{description}
\item [SCC]\textsf{starke Zusammenhangskomponente heißt $S\subseteq Q$
gdw. für alle $q,q'\in S$ gilt $q\rightarrow^{*}q'$}
\end{description}
\begin{itemize}
\item \textsf{SCC heitßt} \textsf{\emph{trivial}} \textsf{wenn $\left|S\right|=1$
und für $q\in S$ gilt $q\nrightarrow q$}
\item \textsf{$\mathcal{L}\neq\emptyset$ wenn Graph von $\ldots$ nicht-trivial
SCC enthält die erreichbar vom Start ist}
\end{itemize}
\end{itemize}
\begin{description}
\item [Aktionen]\textsf{$\mathcal{K}=\left(S,A,\rightarrow,r,AP,\nu\right)$}
\end{description}
\begin{itemize}
\item \textsf{$S,r,AP,\nu$ wie bei Kripkestruktur}
\item \textsf{$A$ sei eine Menge von Aktionen}
\item \textsf{$\rightarrow\subseteq S\times A\times S$}
\item \textsf{Sei $\left(s,a,s'\right)\in\rightarrow$ deterministisch,
so dass sich schreiben lässt $s'=a\left(s\right)$}
\item \textsf{$enabled\left(s\right)=\left\{ a|\exists s':\left(s,a,s'\right)\in\rightarrow\right\} $}
\end{itemize}
\begin{description}
\item [Unabhängigkeit]\textsf{$I\subseteq A\times A$ heißt} \textsf{\emph{Unabhängigkeitsrelation}}
\textsf{für $\mathcal{K}$, falls}
\end{description}
\begin{itemize}
\item \textsf{$\forall a\in A:\left(a,a\right)\notin I$}
\item \textsf{$\forall\left(a,b\right)\in I:\left(b,a\right)\in I$}
\item \textsf{$\forall\left(a,b\right)\in I,s\in S:$} \textsf{\emph{Aktiviertheit}}\textsf{:
$a,b\in enabled\left(s\right)\Rightarrow a\in enabled\left(b\left(s\right)\right)\wedge b\in enabled\left(a\left(s\right)\right)\wedge a\left(b\left(s\right)\right)=b\left(a\left(s\right)\right)$}
\item \textsf{$a$ und $b$ heißen unabhängig, falls $\left(a,b\right)\in I$}
\end{itemize}
\begin{description}
\item [stotter~äquivalenz]\textsf{sind zwei Abläufe einer Kripke Struktur
$\sigma$ und $\rho$, falls es Sequenzen $0=i_{0}<i_{1}<i_{2}<\ldots$
und $0=j_{0}<j_{1}<j_{2}<\ldots$ gibt, so dass für alle $k\ge0$
gilt:}\\
\textsf{$\nu^{-1}\left(\sigma\left(i_{k}\right)\right)=\nu^{-1}\left(\sigma\left(i_{k}+1\right)\right)=\ldots\nu^{-1}\left(\sigma\left(i_{k+1}-1\right)\right)$}\\
\textsf{$=$}\\
\textsf{$\nu^{-1}\left(\rho\left(j_{k}\right)\right)=\nu^{-1}\left(\rho\left(j_{k}+1\right)\right)=\ldots\nu^{-1}\left(\rho\left(j_{k+1}-1\right)\right)$}
\end{description}
\begin{itemize}
\item \textsf{Eine LTL-Formel $\phi$ heißt} \textsf{\emph{stotter-invariant}}\textsf{,
gdw. für alle äquivalenten Abläufe $\sigma$ und $\rho$ gilt\[
\sigma\models\phi\Leftrightarrow\rho\models\phi\]
 }
\item \textsf{Alle Formeln der LTL Logik ohne den X-Operator sind stotter-invariant}
\item \textsf{Zwei Kripke $\mathcal{K}$ und $\mathcal{K}'$ Strukturen
heißen stotter-äquivalent gdw.}

\begin{itemize}
\item \textsf{sie den gleichen Anfangszustand haben}
\item \textsf{für jeden Ablauf $\sigma$ in $\mathcal{K}$ es einen stotter-äquivalenten
Ablauf $\rho$ in $\mathcal{K}'$ gibt und umgekehrt.}
\end{itemize}
\item \textsf{Stotter-invariante Formeln können stotter-äquivalente Kripkestrukturen
nicht unterscheiden}
\end{itemize}
\begin{description}
\item [Sichtbarkeit]\textsf{Eine Aktion $a$ heißt} \textsf{\emph{unsichtbar}}\textsf{,
falls für alle $s,s'\in S$ gilt: Falls $\left(s,a,s'\right)\in\rightarrow$,
dann gilt $\nu^{-1}\left(s\right)=\nu^{-1}\left(s'\right)$.}
\item [Ample~sets]\textsf{$ample\left(s\right)\subseteq enabled\left(s\right)$
ist die Menge an Nachfolgerzuständen die tatsächlich überprüft werden
muss, beim Testen auf Leerheit der Sprache. $\mathcal{K}$ wird also
auf $\mathcal{K}_{R}$ reduziert.}
\end{description}
\begin{itemize}
\item \textsf{$C0$: $ample\left(s\right)=\emptyset$ $\Leftrightarrow$$enabled\left(s\right)=\emptyset$}
\item \textsf{$C1$: Auf jedem Pfad beginnend in $s$ in $\mathcal{K}$
gilt: keine Aktion, die von einer Aktion in $ample\left(s\right)$
abhängt, kann vor einer Aktion in $ample\left(s\right)$ ausgeführt
werden.}\\
\textsf{Eine Aktion $b$, die von einer Aktion $a\in ample\left(s\right)$
abhängt, d.h. $\left(a,b\right)\notin I$, kann erst nach der Ausführung
einer Aktion $c\in ample\left(s\right)$ ausgeführt werden.}
\item \textsf{$C2:$ Falls $ample\left(s\right)\subsetneq enabled\left(s\right)$,
sind alle Aktionen in $ample\left(s\right)$ unsichtbar}
\item \textsf{$C3$: Für alle Zyklen in $\mathcal{K}_{R}$gilt: falls $a\in enabled\left(s\right)$
für einen Zustand im Zyklus, dann $a\in ample\left(s'\right)$ für
einen Zustand $s'$ im Zyklus}
\end{itemize}

\section{Korrektheit Sequentieller Systeme}

\textsf{Alle volgenden Sysmbole müssen eindeutig zuordbar sein $\Leftrightarrow$
alle Mengen sind disjunkt. Bei $\subset$ ist die gleichheit} \textsf{\emph{nicht}}
\textsf{ausgeschlossen}

\begin{description}
\item [Sorten]\textsf{$S=\left(s_{1},\ldots,s_{n}\right)$ wie Liste von
Datentypen}
\item [Signatur]\textsf{$\Sigma=\left(\Sigma_{ws}\right)_{ws\in S^{*}S}$
Angabe über Fuktionssymbole mit dazugehörigen Stelligkeiten und Sorten.}\\
\textsf{$0$-stellig $=$ Konstante}
\item [Variablensymbole]\textsf{$\mathcal{V}=\left(\mathcal{V}_{s}\right)_{s\in S}$}
\end{description}
\begin{itemize}
\item \textsf{$\mathcal{V}\left(\phi\right)$ Menge aller Variablen Symbole
in $\phi$}
\item \textsf{$\mathcal{V}_{f}\left(\phi\right)\subset\mathcal{V}\left(\phi\right)$
Menge aller freien Variablen Symbole in $\phi$, also die nicht abquantifizierten}
\end{itemize}
\begin{description}
\item [Terme]\textsf{$\mathcal{T}\left(\Sigma,\mathcal{V}\right)\subset\left(\mathcal{V}\cup\Sigma\right)^{*}$
Menge der syntaktisch korrekten Terme aus den angegebenen Funktionen
und Variablen}
\item [Grundterme]\textsf{$\mathcal{T}\left(\Sigma\right)$ Terme ohne
Variablen}
\item [sensible]\textsf{Signatur hat von jeder Sorte mindestens ein Konstantensymbol}
\item [$\Sigma$-Algebra]\textsf{ist paar $A=\left(\mathcal{A},\alpha\right)$
mit}

\begin{description}
\item [Trägermengen]\textsf{$\mathcal{A}=\left(\mathcal{A}_{s}\right)_{s\in S}$}
\item [Deutungsfunktionen]\textsf{$\alpha=\left(\alpha_{f}\right)_{f\in\Sigma}$
die Signatur von $f$ respektiert}
\end{description}
\item [Deutung]\textsf{$A:\mathcal{T}\left(\Sigma\right)\rightarrow_{S}\mathcal{A}$
bei gegebener $\Sigma$-Algebra $A$}
\item [Formeln]\textsf{$\mathcal{F}\left(\Sigma,\mathcal{V}\right)\subset\left(\mathcal{V}\cup\Sigma\cup\left\{ \equiv,\neg,\wedge,\forall\right\} \right)^{*}$}
\end{description}
\begin{itemize}
\item \textsf{Sprache wird auch um andere gewohnte boolsche Operatoren erweitert}
\item \textsf{$\mathcal{F}_{g}$ Menge der geschlossenen Formeln, enthalten}
\textsf{\emph{keine}} \textsf{freien Variablen}
\end{itemize}
\begin{description}
\item [Atomare~Formeln]\textsf{$\mathcal{AT}\left(\Sigma,\mathcal{V}\right)\ni t_{1}\equiv t_{2}$
mit $t_{1},t_{2}\in\mathcal{T}\left(\Sigma,\mathcal{V}\right)$}
\item [pränexe~Normalform]\textsf{ist eine Formel $\phi$ wenn alle Quantoren
$\left(\forall,\exists\right)$ ganz links stehen.}
\item [universelle~Formeln]\textsf{wenn pränex und alle Quantoren $\forall$}\\
\textsf{$\mathcal{F}_{\forall}\left(\Sigma,\mathcal{V}\right)$ ist
Menge aller solcher Formeln über geg. Signatur}
\item [Gleichung]\textsf{siehe Atomate Formel $\mathcal{E}\left(\Sigma,\mathcal{V}\right)=\mathcal{AT}\left(\Sigma,\mathcal{V}\right)$}
\item [universelle~Gleichung]\textsf{universelle Formel, die hinter den
Quantoren nur nich genau ein $=$ steht}\\
\textsf{$\mathcal{E}_{\forall}\left(\Sigma,\mathcal{V}\right)$ ist
die Menge aller solcher universelller Geichungen}
\item [Allabschluss]\textsf{für ein $e\in\mathcal{E}\left(\Sigma,\mathcal{V}\right)$
ist $\forall e$ die Gleichung, in der alle freien Variablen abquantifiziert
wurden. Analog für Formelmengen.}
\item [$\Sigma$-Interpretation]\textsf{ist ein Paar $I=\left(A,\mathfrak{a}\right)$
mit der $\Sigma$-Algebra $A$ und $\mathfrak{a}:\mathcal{V}\rightarrow_{S}\mathcal{A}$.}
\item [Deutung]\textsf{von Formel: $\alpha$ auf Funktionen und $\mathfrak{a}$
auf Variablen rekursiv anwenden. Atomare Formeln liefern bool. Dieses
mit Boolschen Funktionen verknüpfen.}\\
\textsf{$I\models_{Alg\left(\Sigma\right)}\phi$ $\Leftrightarrow$
die $\Sigma$-Interpretation $I$ erfüllt eine Formel $\phi\in\mathcal{F}\left(\Sigma,\mathcal{V}\right)$
gdw. die Auswertung true liefert.}

\begin{description}
\item [erfüllbar]\textsf{ist $\phi$ gdw. es einer $\Sigma$-Interpreation
$I$ gibt die Formel $\phi$ erfüllt}
\item [allgemeingültig]\textsf{ist $\phi$ gdw. jede $\Sigma$-Interpreation
$I$ die Formel $\phi$ erfüllt}
\end{description}
\item [folgt]\textsf{$\Phi\models_{\mathcal{F}\left(\Sigma,\mathcal{V}\right)}\phi$
$\Leftrightarrow$ eine Formel $\phi$ folgt aus einer Formelmenge
$\Phi$, gdw. alle Interpretationen die $\Phi$ wahr machen, auch
$\phi$ wahr machen.}
\item [Folgerungen]\textsf{$\Phi^{\models\mathcal{F}\left(\Sigma,\mathcal{V}\right)}$
ist die Menge aller Folgerungen aus $\Phi$}

\begin{description}
\item [allgemeingültig]\textsf{wenn $\emptyset\models_{\mathcal{F}\left(\Sigma,\mathcal{V}\right)}\phi$}
\end{description}
\item [äquivalent]\textsf{$\phi_{1}\approx\phi_{2}$ gdw. $\phi_{1}\leftrightarrow\phi_{2}$
allgeimeingültig}
\item [Theorie]\textsf{$Th\left(A\right):=\left\{ \phi\in\mathcal{F}_{g}\left(\Sigma,\mathcal{V}\right)|A\models\phi\right\} $
zu gegebener $\Sigma$-Algebra $A$}
\end{description}
\begin{itemize}
\item \textsf{ist angeschlossen und vollständig $\phi$ oder $\neg\phi$sind
(nicht)enthalten in $Th\left(A\right)$}
\item \textsf{$Th\left(A\right)\subset Th\left(B\right)\Rightarrow Th\left(A\right)=Th\left(B\right)$}
\end{itemize}
\begin{description}
\item [Substitution]\textsf{$\sigma:\mathcal{V}\rightarrow_{S}\mathcal{T}\left(\Sigma,\mathcal{V}\right)$}
\end{description}
\begin{itemize}
\item \textsf{rekursiv erweitern für gesamte Terme}
\end{itemize}
\begin{description}
\item [Grundsubstitution]\textsf{$\sigma\left(x\right)\in\mathcal{T}\left(\Sigma,\mathcal{V}\right)\cap\left\{ x\right\} $
für alle $x\in\mathcal{V}$}
\item [Substitutionlemma]\textsf{$\mathfrak{a}\left(\sigma\left(t\right)\right)=\mathfrak{a}\left[x_{1}/\mathfrak{a}\left(t_{1}\right),\ldots,x_{n}/\mathfrak{a}\left(t_{n}\right)\right]\left(t\right)$}
\end{description}
\begin{itemize}
\item \textsf{$A\models\forall l\equiv r\Rightarrow A\models\sigma\left(l\right)\equiv\sigma\left(r\right)$
für bel. Substitution $\sigma$}
\end{itemize}
\begin{description}
\item [Klasse~der~$\Sigma$-Algebren]\textsf{$\textrm{Alg}_{\Sigma}$}
\end{description}
\begin{itemize}
\item \textsf{Für $\Phi\subset\mathcal{F}_{g}\left(\Sigma,\mathcal{V}\right)$
ist $\textrm{Mod}_{\Sigma}\left(\Phi\right)\subset\textrm{Alg}_{\Sigma}$
die Klasse aller $\Sigma$-Algebren $A$ mit $A\models\Phi$}
\end{itemize}
\begin{description}
\item [$\Sigma$-Homomorphismus]\textsf{Für $A,B$ $\Sigma$-Algebren ist
$h:\mathcal{A}\rightarrow_{S}\mathcal{B}$ ein Homomorphismus wenn\[
h_{s}\left(\alpha_{f}\left(a_{1},\ldots,a_{n}\right)\right)=\beta_{f}\left(h_{s_{1}}\left(a_{1}\right),\ldots,h_{s_{n}}\left(a_{n}\right)\right)\]
}
\end{description}
\begin{itemize}
\item \textsf{$id^{A}:A\rightarrow A$ ist Homomorphismus}
\item \textsf{Verkettung von Homomorphismen ist wieder Homomorphismus}
\item \textsf{$h\left(A\left(t\right)\right)=B\left(t\right)$ für alle
$t\in\mathcal{T}\left(\Sigma\right)$}
\end{itemize}
\begin{description}
\item [Äquivalenzrelation]\textsf{ist $\sim\in M\times M$ wenn}

\begin{description}
\item [reflexiv]\textsf{$m\sim m$}
\item [symmetrisch]\textsf{$m\sim n\Leftrightarrow n\sim m$}
\item [transitiv]\textsf{$m\sim n\wedge n\sim k\Rightarrow m\sim k$}
\end{description}
\end{description}
\begin{itemize}
\item \textsf{Für Mengen $M,N$ und $f:M\rightarrow N$ ist $\sim_{F}$
definiert durch $m_{1}\sim_{F}m_{2}\Leftrightarrow F\left(m_{1}\right)=F\left(m_{2}\right)$
eine Äquivalenzrelation}
\item \textsf{Äquivalenzklassen sind disjunkte Zerlegung der Gesamtmenge}
\end{itemize}
\begin{description}
\item [Äquivalenzklasse]\textsf{$\left[m\right]_{\sim}=\left\{ n\in M|n\sim m\right\} \subset2^{M}$}
\item [Quotientenmenge]\textsf{$M/_{\sim}=\left\{ \left[m\right]_{\sim}\in2^{M}|m\in M\right\} $}
\item [$\Sigma$-Isomorphismus]\textsf{ist eine bijektiver Homomorphismus}
\end{description}
\begin{itemize}
\item \textsf{$A\simeq_{\Sigma}B$ sind zwei $\Sigma$-Algebren, wenn ein
isomorphismus zwischen ihnen exisitert}
\item \textsf{$\simeq_{\Sigma}$ ist Äquivalenzrelation}
\item \textsf{Isomorphe Algebren haben gleiche Theorie}
\end{itemize}
\begin{description}
\item [Abstrakter~Datentyp]\textsf{für eine Signatur $\Sigma$ ist eine
Klasse $\textrm{C}\subset\textrm{Alg}_{\Sigma}$ von $\Sigma$-Algebren,
die unter Isomorphie abgeschlossen ist, d.h. es gilt für alle $A,B\in\textrm{Alg}_{\Sigma}$}
\end{description}
\begin{itemize}
\item \textsf{$A\in\textrm{C}\Rightarrow\left(A\simeq_{\Sigma}B\Rightarrow B\in\textrm{C}\right)$}

\begin{description}
\item [monomorph]\textsf{heißt $C$ falls $A\in\textrm{C}\Rightarrow\left(B\in\textrm{C}\Rightarrow A\simeq_{\Sigma}B\right)$}
\item [polymorph]\textsf{andernfalls}
\end{description}
\end{itemize}
\begin{description}
\item [initial]\textsf{ist eine $\Sigma$-Algebra $A\in\textrm{Alg}_{\Sigma}$
gdw. gilt: Für jede $\Sigma$-Algebra $B$ existiert} \textsf{\emph{genau
ein}} \textsf{$\Sigma$-Homomorphismus von $A$ nach $B$.}
\end{description}
\begin{itemize}
\item \textsf{gilt $A\simeq_{\Sigma}B$ ist auch $B$ initial}
\end{itemize}
\begin{description}
\item [Termalgebren]\textsf{Sei $\Sigma$ eine Signatur bzgl. einer Sortenmenge
$S$. Dann ist die Termalgebra $T_{\Sigma}=\left(\mathcal{T}\left(\Sigma\right),\tau\right)$
definiert durch \[
\tau_{f}\left(t_{1},\ldots,t_{n}\right):=ft_{1}\ldots t_{n}\]
}
\end{description}
\begin{itemize}
\item \textsf{Diese Termalgebra ist inital in der Klasse aller $\Sigma$-Algebren}
\end{itemize}
\begin{description}
\item [Kongruenzrelation]\textsf{ist $\approx\subset\left(\mathcal{A}_{s}\times\mathcal{A}_{s}\right)_{s\in S}$
wenn:}
\end{description}
\begin{itemize}
\item \textsf{$\approx_{s}$ ist Äquivalenzrelation}
\item \textsf{Kongruenzeigenschaft}\\
\textsf{$a_{1}\approx_{s_{1}}a_{1}'\wedge\ldots\wedge a_{n}\approx_{s_{n}}a_{n}'\Rightarrow\alpha_{f}\left(a_{1},\ldots,a_{n}\right)\approx_{s}\alpha_{f}\left(a_{1}',\ldots,a_{n}'\right)$}

\begin{description}
\item [Kongruenzklasse]\textsf{$\left[a\right]_{\approx_{s}}$ analog Äquivalenzklasse}
\item [Quotientenmenge]\textsf{$\mathcal{A}_{s}/_{\approx_{s}}$ analog
$\ldots$}
\end{description}
\end{itemize}
\begin{description}
\item [Quotientenalgebra]\textsf{ist eine $\Sigma$-Algebra zu gegebenen
$A$ und $\approx$: $A/_{\approx}:=\left(\mathcal{A}/_{\approx},\tilde{\tilde{\alpha}}\right)$
mit \[
\tilde{\tilde{\alpha}}_{f}\left(\left[a_{1}\right]_{\approx_{s_{1}}},\ldots,\left[a_{n}\right]_{\approx_{s_{n}}}\right):=\left[\alpha_{f}\left(a_{1},\ldots,a_{n}\right)\right]_{\approx_{s}}\]
}
\item [Quotiententermalgebra]\textsf{Für eine $\Sigma$-Algebra $A$ sei
$\approx_{A}\subset\mathcal{T}\left(\Sigma\right)\times\mathcal{T}\left(\Sigma\right)$
für alle $t_{1},t_{2}\in\mathcal{T}\left(\Sigma\right)$ definiert
durch\[
t_{1}\approx_{A}t_{2}\Leftrightarrow A\left(t_{1}\right)=A\left(t_{2}\right)\]
die Quotiententermalgebra von $A$ ist dann definiert als $T_{\Sigma}/_{\approx_{A}}=\left(\mathcal{T}\left(\Sigma\right)/_{\approx_{A}},{{\approx_{A}\atop \tau}}\right)$}
\end{description}
\begin{itemize}
\item \textsf{Für Variablenbelegung $\mathfrak{t}$ und Term $t$ gilt $\mathfrak{t}\left(t\right)=\left[t\right]_{\approx_{A}}$}
\end{itemize}
\begin{description}
\item [kanonische~Termalgebra]\textsf{heißt $A\left(\mathcal{A},\alpha\right)$
gdw.: $\mathcal{A}\subset\mathcal{T}\left(\Sigma\right)$ und $\forall t\in A:A\left(t\right)=t$}
\item [Teilsignatur]\textsf{ist eine Signatur, bei der einige Funktionssymbole
weggleassen wurden}
\item [Erzeugte~$\Sigma$-Algebra]\textsf{Seien $\Sigma^{c}$ und $\Sigma$
$S$-Signaturen mit $\Sigma^{c}\subset\Sigma$ und sei $A=\left(\mathcal{A},\alpha\right)$
eine $\Sigma$-Algebra. Dann ist $A$ durch $\Sigma^{c}$} \textsf{\emph{erzeugt}}
\textsf{gdw. gilt: $\forall s\in S,a\in\mathcal{A}_{s}:\exists q\in\mathcal{T}\left(\Sigma_{s}^{c}\right):a=A\left(q\right)$}
\end{description}
\begin{itemize}
\item \textsf{bei erzeugter Algebra sind alle Trägermengen abzählbar}
\item \textsf{$A$ initial $\Rightarrow$ $A$ erzeugt}
\item \textsf{$A$ erzeugt $\Rightarrow$ $A\simeq_{\Sigma}T_{\Sigma}/_{\approx_{A}}$}
\item \textsf{Sei $h:A\rightarrow B$ Homomorphismus ist eindeutig, falls
$A$ erzeugt}
\item \textsf{erzeugte Algebren mit gleicher Theorie sind isomorph}
\end{itemize}
\begin{description}
\item [frei]\textsf{erzeugt wenn zusätzlich gilt $\forall s\in S,q_{1},q_{2}\in\mathcal{T}\left(\Sigma_{s}^{c}\right):A\left(q_{1}\right)=A\left(q_{2}\right)\Rightarrow q_{1}=q_{2}$}\\
\textsf{$\textrm{Gen}_{\Sigma}\subset\textrm{Alg}_{\Sigma}$ bezeichnet
die Klasse aller erzeugten $\Sigma$-Algebren}
\end{description}
\begin{itemize}
\item \textsf{(frei) erzeugtheit vererbt sich durch Isomorphie und Quotiententermalgebra
bildung}
\item \textsf{alle Konstruktoren werden als injektive Funktionen gedeutet}
\item \textsf{Es existiert eine isomorphe kanonische Termalgebra $T_{A}$
zu $A$}
\end{itemize}
\begin{description}
\item [Redukt]\textsf{ist Reduzierte Algebra zu kleinerer Signatur}
\end{description}
\begin{itemize}
\item \textsf{$A$ durch $\Sigma^{c}\subset\Sigma$ erzeugt und sei $A^{c}$
das $\Sigma^{c}$ Redukt von $A$ }\\
\textsf{$A$ freu erzeugt durch $\Sigma^{c}\Leftrightarrow A^{c}\simeq_{\Sigma^{c}}T_{\Sigma^{c}}$}
\end{itemize}
\begin{description}
\item [Expansion]\textsf{ist vollständige Algebra zu großer Signatur}
\item [Kongruenz~aus~Relation]\textsf{Sei $A$ eine $\Sigma$-Algebra,
und $R=\subset\left(\mathcal{A}_{s}\times\mathcal{A}_{s}\right)$.
Es existiert eine kleinste Kongruenzrelation $\approx_{R}$ die $R$
noch enthält}
\item [Kongruenz~aus~Gleichung]\textsf{Für $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right)$
ist \begin{eqnarray*}
R_{E}: & = & \left\{ \left(\theta\left(l\right),\theta\left(r\right)\right)\in\mathcal{T}\left(\Sigma\right)\times\mathcal{T}\left(\Sigma\right)|\right.\\
 &  & \left.l\equiv r\in E\wedge\theta\textrm{ ist Substitution}\right\} \end{eqnarray*}
und $\approx_{E}:=\approx_{R_{E}}$}
\end{description}
\begin{itemize}
\item \textsf{Für alle $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right)$gilt
$T_{\Sigma}/_{\approx_{E}}\models\forall E$}
\item \textsf{Sei $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right).$Dann
ist $T_{\Sigma}/_{\approx_{E}}$ initial in $\textrm{Mod}_{\Sigma}\left(\forall E\right)$}
\end{itemize}
\begin{description}
\item [Vorgehen]\textsf{Gegeben sei $S$, $\Sigma^{c}\subset\Sigma$ und
$E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right)$, so dass $T_{\Sigma/_{\approx_{E}}}$
eine durch $\Sigma^{c}$ freu erzeugte Quotiententermalgebra ist.}
\end{description}
\begin{itemize}
\item \textsf{Wir erweitern $S$ zu $S'$, $\Sigma^{c}$ zu $\Sigma^{c'}$,
$\Sigma^{d}$ zu $\Sigma^{d'}$und $E$ zu $E'\subset\mathcal{E}'\left(\Sigma',\mathcal{V}\right)$}
\item \textsf{Wir benötigen Gleichungen nur, wenn wir $\Sigma^{d}$ um ein
neues Funktionssymbol $f$ zu $\Sigma^{d'}$ erweitern.}
\item \textsf{Solch eine Gleichungsmenge $E'\backslash E$ muß garantieren,
daß $T_{\Sigma'}/_{\approx_{E'}}$ durch $\Sigma^{c}$ frei erzeugt
ist, d.h. für alle $q_{i}\in\mathcal{T}\left(\Sigma^{c}\right)$ein
$q\in\mathcal{T}\left(\Sigma^{c}\right)$mit \[
T_{\Sigma'}/_{\approx_{E'}}\left(fq_{1}\ldots q_{n}\right)\in\left[q\right]_{\approx_{E'}}\]
 existiert und für alle $q\in\mathcal{T}\left(\Sigma^{c}\right)$
\[
\mathcal{T}\left(\Sigma^{c}\right)\cap\left[q\right]_{\approx_{E'}}=\left\{ q\right\} \]
 gilt. Wir nennen solche Gleichungsmengen $E'\backslash E$} \textsf{\emph{zulässig.}}
\item \textsf{${{E\atop \tau}}_{f}\left(q_{1},\ldots,q_{n}\right):=q$ gdw.
${{\approx_{E}\atop \tau}}_{f}\left(\left[q_{1}\right]_{\approx_{E}},\ldots,\left[q_{n}\right]_{\approx_{E}}\right)=\left[q\right]_{\approx_{E}}$
definiert eine frei erzeugte kanonische Termalgebra $T_{\Sigma,E}=\left(\mathcal{T}\left(\Sigma^{c}\right),{{E\atop \tau}}\right)$
für die gilt $T_{\Sigma,E}\simeq_{\Sigma}T_{\Sigma}/_{\approx_{E}}$}
\end{itemize}
\begin{description}
\item [structure]\textsf{struct <= $cons_{1}\left(sel_{1,1}:sct_{1,1},\ldots,sel_{1,n_{1}}:sct_{1,n_{1}}\right),\ldots$}
\end{description}
\begin{itemize}
\item \textsf{$sct_{i,h}\in\left(S\backslash\left\{ bool\right\} \right)\cup\left\{ struct\right\} $
für alle $i\in\left\{ 1,\ldots,k\right\} $ und alle $h\in\left\{ 1,\ldots,n_{i}\right\} $.
($sct=struct$)}
\item \textsf{$n_{i}\ge0$ für alle $\left\{ 1,\ldots,k\right\} $}
\item \textsf{Anzahl der Konstruktoren: $k\ge1$}
\end{itemize}
\begin{description}
\item [Axiome]\textsf{$EQ_{struct}$}
\end{description}
\begin{itemize}
\item \textsf{Gleichheit von Konstanten $eq_{struct}\left(cons_{i},cons_{i}\right)\equiv true$}
\item \textsf{Gleichheit von längeren Konstruktoren (geschachtelt, allquantifiziert)
$eq_{struct}\left(cons_{i}\left(\ldots\right),cons_{i}\left(\ldots\right)\right)\equiv eq\left(eq\left(\ldots\right)\right)$}
\item \textsf{Nichgleichheit bei führenden Konstruktoren $eq_{struct}\left(cons_{i}\left(\ldots\right),cons_{j}\left(\ldots\right)\right)\equiv false$}
\item \textsf{Falsch angewendete Selektoren liefern Beispielterm (Konstante)}
\item \textsf{Selektoren $\forall x_{1}:struct_{i,1}\ldots.sel_{i,h}\left(cons_{i}\left(\ldots\right)\right)\equiv x_{h}$}
\item \textsf{$if_{struct}\left(true,x,y\right)\equiv x$}\\
\textsf{$if_{struct}\left(false,x,y\right)\equiv y$}
\end{itemize}
\begin{description}
\item [function]\textsf{$proc\left(x_{1}:struct_{1},\ldots,x_{k}:struct_{k}\right):struct<=R_{proc}$}
\end{description}
\begin{itemize}
\item \textsf{$x_{i}$ Parameter vom Typ $struct_{i}$}
\item \textsf{name $Proc$ und Rückgabe vom Typ $struct$}
\item \textsf{$R_{proc}$ ist Rumpf und muss sich zu $struct$ auswerten
lassen}
\end{itemize}
\begin{description}
\item [konstruktive~Spec.]\textsf{$S$ ist eine Folge $\left\langle D_{0},\ldots,D_{n}\right\rangle $
von Datenstruktur- und Prozedurdefinitionen.}
\end{description}
\begin{itemize}
\item \textsf{$S\left(0\right)=\left\{ bool\right\} $, $\Sigma\left(0\right)_{bool}^{c}=\left\{ true,false\right\} $,
$\Sigma\left(0\right)_{bool,bool,bool,bool}^{c}=\left\{ if_{bool}\right\} $}
\item \textsf{$S,\Sigma^{c},\Sigma^{d},E,\mathcal{V}$ sind Funktionen von
$i$ $\rightarrow$ nummer der konstruktionsiteration }
\item \textsf{$\left\langle D_{0},\ldots,D_{n}\right\rangle \oplus D=\left\langle D_{0},\ldots,D_{n},D\right\rangle $}
\end{itemize}
\begin{description}
\item [zulässige~Spec.]\textsf{Eine Konstruktive Spezifikation $S=\left\langle D_{0},\ldots,D_{n}\right\rangle $
ist zulässig, gdw. die $\Sigma\left(n\right)$-Algebra $T_{\Sigma\left(n\right)}/_{\approx_{E_{n}}}$
frei erzeugt durch $\Sigma\left(n\right)^{c}$ ist}
\end{description}
\begin{itemize}
\item \textsf{Datenstrukturdefinitionen sind automatisch zulässig in Verifun}
\end{itemize}
\begin{description}
\item [prozedur~Relation]\textsf{für gegebenes $proc$ ist\[
>_{proc}\subset\left(\mathcal{T}\left(\Sigma^{c}\right)_{struct_{1}}\times\ldots\times\mathcal{T}\left(\Sigma^{c}\right)_{struct_{n}}\right)^{2}\]
$\left(q_{1},\ldots,q_{n}\right)>_{proc}\left(q_{1}',\ldots,q_{n}'\right)$
gdw. beim Aufruf von $proc\left(q_{1},\ldots,q_{n}\right)$ wird $proc\left(q_{1}',\ldots,q_{n}'\right)$
rekursiv aufgerufen}
\end{description}
\begin{itemize}
\item \textsf{Eine Prozedur terminiert und damit ist ihre Definition zulässig,
gdw. $>_{proc}$ fundiert ist.}
\end{itemize}
\begin{description}
\item [Fundierte~Relation]\textsf{Eine Relation $\succ\subset M\times M$
heißt fundiert gdw. es gibt keine unendliche Folgen $m_{0},m_{1},\ldots$
mit $m_{i}\succ m_{i+1}$ für alle $i\in\mathbb{N}$}
\end{description}

\end{document}