chapters/finishingcool.tex

   1 \section{Finishing COOL}
   2 \subsection*{Dummy}
   3
   4 \begin{frame}{Where we left (TODO)}
   5   \begin{itemize}
   6   \item Actually implementing deferral tracking
   7   \item Deciding when some deferral can be considered ``finished''
   8   \item \dots
   9   \item Finding ``right'' heuristic for when to try and close the tableau
  10   \item Fixing all the bugs
  11   \end{itemize}
  12 \end{frame}
  13
  14 \begin{frame}{Extra nodes}
  15   \begin{itemize}
  16   \item Different set of deferrals create different nodes
  17   \item Exponential increase in number of nodes
  18   \end{itemize}
  19 \end{frame}
  20
  21 \begin{frame}{Propagation}
  22   \begin{itemize}
  23   \item COOL works in rounds
  24     \begin{itemize}
  25     \item One further state for each core (propositional, minisat)
  26     \item All possible modal steps (coalgebraic step)
  27     \end{itemize}
  28   \item Check for (un)satisfiability after \#{}OpenStates rounds\pause
  29   \item Ideas
  30     \begin{itemize}
  31     \item Creating cycles forces earlier propagation
  32     \item Use \#{}OpenStates steps, not rounds
  33     \end{itemize}
  34   \end{itemize}
  35 \end{frame}
  36
  37 \begin{frame}
  38   TODO: auswertungen mit ``jedes'' mal propagieren, current magic, nie propagieren
  39 \end{frame}
  40
  41 %%% Local Variables:
  42 %%% mode: latex
  43 %%% TeX-master: "../vortrag"
  44 %%% TeX-engine: luatex
  45 %%% TeX-PDF-mode: t
  46 %%% End: