\section{Finishing COOL}
\subsection*{Dummy}

\begin{frame}{Where we left (TODO)}
  \begin{itemize}
  \item actually implementing deferral tracking
  \item deciding when some deferral can be considered ``finished''
  \item \dots
  \item finding ``right'' heuristic for when to try and close the tableaux
  \item fixing all the bugs
  \end{itemize}
\end{frame}

\begin{frame}{Extra nodes}
  \begin{itemize}
  \item Different set of deferrals create different Nodes
  \item Exponential increase in Nodes
  \end{itemize}
\end{frame}

\begin{frame}
  TODO: graphviz der $p\#q\#$ formel
\end{frame}

\begin{frame}{Propagation}
  \begin{itemize}
  \item COOL works in rounds
    \begin{itemize}
    \item One further solution from each Core (propositional)
    \item All possible modal steps
    \end{itemize}
  \item Check for satisfiability after \#{}OpenStates rounds\pause
  \item Ideas
    \begin{itemize}
    \item Creating cycles forces earlier propagation
    \item Use \#{}OpenStates steps, not rounds
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  TODO: auswertungen mit ``jedes'' mal propagieren, current magic, nie propagieren
\end{frame}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "../vortrag"
%%% TeX-engine: luatex
%%% TeX-PDF-mode: t
%%% End: 
