1
\section{Finishing COOL
}
4 \begin{frame
}{Where we left (TODO)
}
6 \item Actually implementing deferral tracking
7 \item Deciding when some deferral can be considered ``finished''
9 \item Finding ``right'' heuristic for when to try and close the tableau
10 \item Fixing all the bugs
14 \begin{frame
}{Extra nodes
}
16 \item Different set of deferrals create different nodes
17 \item Exponential increase in number of nodes
21 \begin{frame
}{Propagation
}
23 \item COOL works in rounds
25 \item One further state for each core (propositional, minisat)
26 \item All possible modal steps (coalgebraic step)
28 \item Check for (un)satisfiability after \#
{}OpenStates rounds
\pause
31 \item Creating cycles forces earlier propagation
32 \item Use \#
{}OpenStates steps, not rounds
38 TODO: auswertungen mit ``jedes'' mal propagieren, current magic, nie propagieren
43 %%% TeX-master: "../vortrag"
44 %%% TeX-engine: luatex