\begin{frame}{Where we left (TODO)}
\begin{itemize}
- \item actually implementing deferral tracking
- \item deciding when some deferral can be considered ``finished''
+ \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
+ \item Finding ``right'' heuristic for when to try and close the tableau
+ \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
+ \item Different set of deferrals create different nodes
+ \item Exponential increase in number of 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
+ \item One further state for each core (propositional, minisat)
+ \item All possible modal steps (coalgebraic step)
\end{itemize}
- \item Check for satisfiability after \#{}OpenStates rounds\pause
+ \item Check for (un)satisfiability after \#{}OpenStates rounds\pause
\item Ideas
\begin{itemize}
\item Creating cycles forces earlier propagation