\relax

\@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}}

\@writefile{toc}{\contentsline {section}{\numberline {2}Coalgebraic Sequent Calculus}{I}}

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

\@writefile{toc}{\contentsline {subsection}{\numberline {2.2}A generic sequent calculus for coalgebraic modal logics}{II}}

\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Branching or finishing propositional sequent rules}}{II}}

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

\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Linear propositional sequent rules}}{II}}

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

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

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

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

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

\@writefile{toc}{\contentsline {section}{\numberline {3}Optimisations}{V}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Normalisation}{VI}}

\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces Normalisation rules}}{VI}}

\newlabel{fig:normalisation}{{5}{VI}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Simplification by Tautologies}{VI}}

\@writefile{toc}{\contentsline {subsubsection}{Propositional Simplification}{VI}}

\@writefile{lof}{\contentsline {figure}{\numberline {6}{\ignorespaces Propositional tautologies used for simplification}}{VII}}

\newlabel{fig:propTauts}{{6}{VII}}

\@writefile{toc}{\contentsline {subsubsection}{Modal Simplification}{VII}}

\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Modal tautologies for simplification}}{VII}}

\newlabel{fig:modTauts}{{7}{VII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Semantic Branching}{VII}}

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

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

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

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

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

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

\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Controlled Backtracking}{IX}}

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

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

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

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

\@writefile{toc}{\contentsline {subsection}{\numberline {3.5}Maximal Application of Modal Rules}{XII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.6}Proof-tree Trimming}{XII}}

\@writefile{lof}{\contentsline {figure}{\numberline {11}{\ignorespaces Admissability of restriction to maximal application of modal rules}}{XIII}}

\newlabel{fig:admisRes}{{11}{XIII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.7}Caching}{XIII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {3.8}Heuristics}{XIV}}

\@writefile{toc}{\contentsline {subsubsection}{Propositional expansion first}{XIV}}

\@writefile{toc}{\contentsline {subsubsection}{Classic Heuristics}{XIV}}

\@writefile{toc}{\contentsline {subsubsection}{Modal Heuristics}{XIV}}

\@writefile{toc}{\contentsline {section}{\numberline {4}Global Caching Algorithm}{XV}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}The proof graph and transitions}{XV}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}The Algorithm}{XVI}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Improving the algorithm}{XVI}}

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

\newlabel{fig:propagation}{{12}{XVIII}}

\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Removing Caching}{XIX}}

\@writefile{toc}{\contentsline {section}{\numberline {5}Implementation}{XIX}}

\@writefile{toc}{\contentsline {section}{\numberline {6}Conclusion}{XIX}}

\@writefile{toc}{\contentsline {section}{\numberline {7}Appendix (\& old stuff)}{XIX}}

\bibstyle{myabbrv}

\bibdata{coalgml}