Add more text

diff --git a/chapters/benchmark.tex b/chapters/benchmark.tex
new file mode 100644 (file)
index 0000000..5342771
--- /dev/null
+++ b/chapters/benchmark.tex
@@ -0,0 +1,13 @@
+\section{Benchmarks}
+\subsection*{Dummy}
+
+\begin{frame}
+  TODO: some representative benchmarks with GMUL/TreeTab/Cool(/MLSolver?)
+\end{frame}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "../vortrag"
+%%% TeX-engine: luatex
+%%% TeX-PDF-mode: t
+%%% End: 

diff --git a/chapters/early.tex b/chapters/early.tex
new file mode 100644 (file)
index 0000000..d557390
--- /dev/null
+++ b/chapters/early.tex
@@ -0,0 +1,22 @@
+\section{``Early'' formulas}
+\subsection*{Dummy}
+
+\begin{frame}
+  \begin{itemize}
+  \item Existing benchmark formulas either require exponential model
+    or have small unfolding
+  \item \emph{early} class of formulas have exponential unfolding but
+    exponetial subgraphs can be dealt with fast
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  TODO construction
+\end{frame}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "../vortrag"
+%%% TeX-engine: luatex
+%%% TeX-PDF-mode: t
+%%% End: 

diff --git a/chapters/finishingcool.tex b/chapters/finishingcool.tex
new file mode 100644 (file)
index 0000000..a90f7b8
--- /dev/null
+++ b/chapters/finishingcool.tex
@@ -0,0 +1,50 @@
+\section{Finishing Cool}
+\subsection*{Dummy}
+
+\begin{frame}{Where we left (TODO)}
+  \begin{itemize}
+  \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
+  \end{itemize}
+\end{frame}
+
+\begin{frame}{Extra nodes}
+  \begin{itemize}
+  \item Different set of deferrals create different Nodes
+  \item Exponential increase in 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
+    \end{itemize}
+  \item Check for satisfiability after \#{}OpenStates rounds\pause
+  \item Ideas
+    \begin{itemize}
+    \item Creating cycles forces earlier propagation
+    \item Use \#{}OpenStates steps, not rounds
+    \end{itemize}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  TODO: auswertungen mit ``jedes'' mal propagieren, current magic, nie propagieren
+\end{frame}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "../vortrag"
+%%% TeX-engine: luatex
+%%% TeX-PDF-mode: t
+%%% End: 

diff --git a/chapters/optimizations.tex b/chapters/optimizations.tex
new file mode 100644 (file)
index 0000000..9877634
--- /dev/null
+++ b/chapters/optimizations.tex
@@ -0,0 +1,67 @@
+\section{Optimizing}
+\subsection*{Dummy}
+
+\begin{frame}{Semnatic 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
+  \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
+  \end{itemize}
+\end{frame}
+
+\begin{frame}{Subset Nodes}
+  \begin{itemize}
+  \item Lemma: If some Node is already satisfiable, all Nodes with
+    subsets of formulas, deferrals are also satisfiable
+  \item Too expensive to check in general\pause
+  \item Might be interesting for Nodes with full focus and its
+    siblings with the same set of formulas
+  \item Cheap but does this happen often?
+  \end{itemize}
+\end{frame}
+
+\begin{frame}{Normalization}
+  TODO: ?
+  \begin{itemize}
+  \item Global Caching better with more same formulas
+  \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 Needs to consider all satisfiable nodes
+    \item Iterates over all edges
+    \end{itemize}
+  \end{block}\pause
+  \begin{itemize}
+  \item Idea: Remove unneeded edges
+  \item Cores are $\exists$-quantified -- all unsatisfiable children
+    may be removed
+  \item States are essentially $\forall$-quantified -- all satisfiable
+    children may be removed
+  \end{itemize}
+\end{frame}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "../vortrag"
+%%% TeX-engine: luatex
+%%% TeX-PDF-mode: t
+%%% End: 

diff --git a/vortrag.tex b/vortrag.tex
index 3b07c62ec4666aa43745955cf59e9226fe75886b..24bf9b2b1eb2d204519a587879c249ebf2a94b91 100644 (file)
--- a/vortrag.tex
+++ b/vortrag.tex
@@ -89,7 +89,7 @@
        \end{tabular}
        \\
        \vspace{0.6cm}
-       2016~\textendash~01~\textendash~19
+       2016~\textendash~04~\textendash~26
 }
 \titlepage
 \end{frame}
@@ -106,16 +106,6 @@
   \tableofcontents{}
 \end{frame}
 
-\begin{frame}{Where we left}
-  \begin{itemize}
-  \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
-  \end{itemize}
-\end{frame}
-
 \input{chapters/finishingcool}
 \input{chapters/early}
 \input{chapters/optimizations}
@@ -130,8 +120,8 @@
     \end{center}
     \vspace*{\fill}
 
-  Download: https://static.siccegge.de/talks/cool-FAU-2016-01-19.pdf\\
-  https://git.siccegge.de/?p=talk/coalgebraic-mu-calculus-cool.git
+  Download: https://static.siccegge.de/talks/cool-FAU-2016-04-26.pdf\\
+  https://git.siccegge.de/?p=talk/coalgebraic-mu-calculus-cool-2.git
 \end{frame}
 
 \end{document}