\relax

\citation{SchroderPattinson09}

\citation{CalinEA09,HausmannSchroder10}

\citation{GoreEA10}

\@writefile{toc}{\contentsline {title}{Optimizing Coalgebraic Modal Logic Reasoning}{I}}

\@writefile{toc}{\authcount {1}}

\@writefile{toc}{\contentsline {author}{Daniel Hausmann\unskip {}}{I}}

\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{I}}

\newlabel{intro}{{1}{I}}

\citation{SchroderPattinson09}

\@writefile{toc}{\contentsline {section}{\numberline {2}Coalgebraic Modal Logic}{II}}

\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Notation}{II}}

\citation{SchroderPattinson09}

\citation{PattinsonSchroder08b,HausmannSchroder10}

\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Branching propositional sequent rule}}{III}}

\newlabel{fig:bpropRules}{{1}{III}}

\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Linear or closing propositional sequent rules}}{III}}

\newlabel{fig:lpropRules}{{2}{III}}

\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces One-step complete, resolution closed modal rules for some coalgebraic modal logics}}{IV}}

\newlabel{fig:modalRules}{{3}{IV}}

\citation{GoreEA10}

\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces One-step complete, resolution closed modal rules for some conditional logics}}{V}}

\newlabel{fig:modalRules2}{{4}{V}}

\@writefile{toc}{\contentsline {section}{\numberline {3}Global Caching Algorithm for Coalgebraic Logics}{V}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}The proof graph and transitions}{VI}}

\citation{GoreEA10}

\citation{HorrocksPatelSchneider99}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}The Algorithm}{VII}}

\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces The global caching algorithm}}{VII}}

\newlabel{fig:globalAlg}{{5}{VII}}

\@writefile{toc}{\contentsline {section}{\numberline {4}Optimisations}{VII}}

\citation{GoreEA10}

\citation{HorrocksPatelSchneider99}

\@writefile{lof}{\contentsline {figure}{\numberline {6}{\ignorespaces Normalisation rules}}{VIII}}

\newlabel{fig:normalisation}{{6}{VIII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Simplification}{VIII}}

\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Examplary tautologies used for simplification}}{IX}}

\newlabel{fig:tauts}{{7}{IX}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Generalized Semantic Branching}{IX}}

\@writefile{toc}{\contentsline {subsubsection}{Propositional Semantic Branching}{IX}}

\@writefile{lof}{\contentsline {figure}{\numberline {8}{\ignorespaces Syntactic vs. Semantic branching on conjunctions}}{IX}}

\newlabel{fig:synSemConj}{{8}{IX}}

\citation{HorrocksPatelSchneider99}

\@writefile{toc}{\contentsline {subsubsection}{Modal Semantic Branching}{X}}

\@writefile{lof}{\contentsline {figure}{\numberline {9}{\ignorespaces Specific semantic branching for examplary modal logics}}{X}}

\newlabel{fig:semBranch}{{9}{X}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Generalized Dependency Directed Backtracking}{X}}

\newlabel{fact:promtrs}{{3}{XI}}

\@writefile{lof}{\contentsline {figure}{\numberline {10}{\ignorespaces Propagation of dependencies over some examplary modal features}}{XI}}

\newlabel{fig:depProp}{{10}{XI}}

\newlabel{lemma:provabilityPropagates}{{4}{XII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Proof Formulas and efficient propagation}{XIII}}

\@writefile{lof}{\contentsline {figure}{\numberline {11}{\ignorespaces The simplification rules for propagation in proof formulas}}{XIV}}

\newlabel{fig:propagation}{{11}{XIV}}

\@writefile{toc}{\contentsline {section}{\numberline {5}Conclusion}{XIV}}

\bibstyle{myabbrv}

\bibdata{coalgml}

\bibcite{CalinEA09}{1}

\bibcite{GoreEA10}{2}

\bibcite{HausmannSchroder10}{3}

\bibcite{HorrocksPatelSchneider99}{4}

\bibcite{PattinsonSchroder08b}{5}

\bibcite{SchroderPattinson09}{6}