Misc fixes

[talk/coalgebraic-mu-calculus-cool-2.git] / chapters / optimizations.tex

diff --git a/chapters/optimizations.tex b/chapters/optimizations.tex
index 987763482a557232ee5fb10759b70b5793fca000..9de0c1ee21368ba55319081a566077f97144f3ed 100644 (file)
--- a/chapters/optimizations.tex
+++ b/chapters/optimizations.tex
@@ -1,22 +1,21 @@
 \section{Optimizing}
 \subsection*{Dummy}
 
-\begin{frame}{Semnatic Branching}
+\begin{frame}{Semantic Branching}
   \begin{itemize}
-  \item Idea: Add aditional information when considering second
-    alternative of an or: ${\phi \vee \psi}$ becomes ${\phi \vee
-      (¬\phi \wedge \psi)}$
-  \item Do not reexplore branches already known to be unsat already
+  \item Idea: Add additional information when considering second
+    alternative of a disjunction: ${\phi \vee \psi}$ becomes ${\phi
+      \vee (¬\phi \wedge \psi)}$
+  \item Do not re-explore branches already known to be unsatisfiable already
   \end{itemize}
 \end{frame}
 
 \begin{frame}{Non-atomic Negations}
-  TODO: ?
   \begin{itemize}
   \item Consider $\heartsuit\heartsuit\heartsuit{}p \wedge \overline{\heartsuit}\overline{\heartsuit}\overline{\heartsuit}¬p$
   \item Same as $\heartsuit\heartsuit\heartsuit{}p \wedge
     ¬\heartsuit\heartsuit\heartsuit{}p$ and thus obviously unsatisfiable
-  \item Cool normalizes formulas to make best use of Global Caching
+  \item COOL normalizes formulas to make best use of Global Caching
   \end{itemize}
 \end{frame}
 
@@ -35,16 +34,15 @@
   TODO: ?
   \begin{itemize}
   \item Global Caching better with more same formulas
-  \item Preprocessing in Cool currently does not consider
+  \item Preprocessing in COOL currently does not consider
     (propositional) Comutativity, Associativity or Distributivity laws
   \end{itemize}
 \end{frame}
 
-
 \begin{frame}{Removing Edges}
   \begin{block}{Propagation}
     \begin{itemize}
-    \item Runs in $O(edge\cdot nodes)$
+    \item Runs in $\mathcal{O}(\mathit{|edge|}\cdot\mathit{|nodes|})$
     \item Needs to consider all satisfiable nodes
     \item Iterates over all edges
     \end{itemize}