X-Git-Url: https://git.siccegge.de//index.cgi?p=talk%2Fcoalgebraic-mu-calculus-cool-2.git;a=blobdiff_plain;f=chapters%2Ffinishingcool.tex;fp=chapters%2Ffinishingcool.tex;h=be9565a1c8646a460822fed346a05bb57fe2a65d;hp=1b747e923d8dbf2021c4d0113d328663c2815851;hb=b358bccd3f36b7e4a1ddf8c8122755d91d000340;hpb=c23d4f4bb88ea0a9799ea81f40b780201ada016f

diff --git a/chapters/finishingcool.tex b/chapters/finishingcool.tex
index 1b747e9..be9565a 100644
--- a/chapters/finishingcool.tex
+++ b/chapters/finishingcool.tex
@@ -3,33 +3,29 @@
 
 \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