hoffe bin im richtigen forenteil!
auch nach einigem googeln, kann ich nicht nachvollziehen was im folgendem code schief läuft:
\subsection{Basic Properties}
\begin{frame}
For the BCS, certain properties have to hold.\\
Proving that they do hold will be the task of the proof planner in conjunction with a proover.\\
\begin{enumerate}
\item Reachability: Under suitable conditions $\phi (x)$, any user can get 'ready' : $\forall x.\phi (x) \supset ready(x)$
\item First-order properties: If I am ready and dial a number, i am trying to call that very same number:
$\forall x,y.\box (ready(x) \wedge dial(x,y)) \supset \bigcirc trying(x,y)$
\item Weak until properties: If I am trying to connect y, I will keep trying until I either hear the busy tone or I am ringing y:
$\forall x,y. \box trying(x,y) \supset trying(x,y) W (busytone(x) \vee oringing(x,y))$
\item Within the OCS these properties have to hold only to a limited extent, nobody can connect to someone on his screening list
\end{enumerate}
\end{frame}
Komischer Fakt dazu: mit TexMakerX kann ich die Datei nicht ohne den Fehler kompilieren, wenn ich dann nach speichern die datei mit TexWorks öffne, bekomm ich einfach die passende pdf Datei for free dazu. Also scheint das ja schon irgendwie richtig zu funktionieren, aber andrerseits auch nicht. wenn ihr verstehtt, es wird schon spät (=.
Falls jemand helfen kann, würd ich mich freuen, ansonsten versuch ich mich weiter durchzuwurschteln.
Danke schonmal![/code]
