\relax 
\citation{NNS:H1}
\newlabel{sec:intro}{{1}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{2}}
\citation{SS:TPTP}
\citation{Coq74}
\citation{Selinger:LACPV}
\citation{JGL:JFLA04}
\citation{ComonBoudet:Presburger}
\newlabel{sec:theory}{{2}{6}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Tree Automata, Clauses}{6}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Recognizing the lists of even natural numbers}}{8}}
\newlabel{fig:listeven}{{1}{8}}
\newlabel{eq:pop}{{1}{8}}
\newlabel{eq:definite}{{2}{8}}
\citation{NNS:H1}
\citation{3French:oneclause}
\citation{NNS:H1}
\citation{JGL:H1}
\newlabel{eq:goal}{{3}{9}}
\citation{NNS:H1}
\citation{JGL:H1}
\newlabel{eq:alt}{{4}{10}}
\newlabel{sec:examples}{{3}{10}}
\@writefile{toc}{\contentsline {section}{\numberline {3}The {\tt  h1} Tool Suite through Examples}{10}}
\newlabel{sec:h1:ex}{{3.1}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}A Toy, Introductory Example}{10}}
\@writefile{lol}{\contentsline {lstlisting}{test1.p}{10}}
\citation{Pelletier:75pbs}
\@writefile{lol}{\contentsline {lstlisting}{h1\textunderscore test1\textunderscore err}{11}}
\newlabel{sec:h1:expb55}{{3.2}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}The Dreadsbury Mansion Murder Mystery Example}{12}}
\@writefile{lol}{\contentsline {lstlisting}{butler1\textunderscore err}{13}}
\@writefile{lol}{\contentsline {lstlisting}{butler3\textunderscore err}{13}}
\@writefile{lol}{\contentsline {lstlisting}{butler5\textunderscore err}{14}}
\newlabel{sec:h1:excompl}{{3.3}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3}Computing with Tree Automata}{14}}
\@writefile{lol}{\contentsline {lstlisting}{listeven.p}{15}}
\@writefile{lol}{\contentsline {lstlisting}{tree3plus2.p}{15}}
\@writefile{lol}{\contentsline {lstlisting}{tree3plus2.model.pl}{16}}
\newlabel{sec:h1:excompl:vis}{{3.3.1}{16}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.1}Visualizing Tree Automata}{16}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Trees with leaves equal to $nil$ or to $3n+2$, $n\in \mathbb  {N}$}}{16}}
\newlabel{fig:tree3plus2_model}{{2}{16}}
\newlabel{sec:h1:excompl:inter}{{3.3.2}{16}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.2}Computing Intersections of Tree Automata}{16}}
\@writefile{lol}{\contentsline {lstlisting}{list\textunderscore even\textunderscore inter\textunderscore tree3plus2.model.pl}{17}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Trees with leaves equal to $nil$ or to $3n+2$, which are lists of even natural numbers at the same time}}{18}}
\newlabel{fig:interex}{{3}{18}}
\newlabel{sec:h1:excompl:empty}{{3.3.3}{19}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.3}Checking Tree Automata for Emptiness, Testing Membership}{19}}
\@writefile{lol}{\contentsline {lstlisting}{h1\textunderscore inter2\textunderscore err}{19}}
\@writefile{lol}{\contentsline {lstlisting}{h1\textunderscore inter3\textunderscore err}{20}}
\@writefile{lol}{\contentsline {lstlisting}{h1\textunderscore inter4\textunderscore err}{20}}
\@writefile{lol}{\contentsline {lstlisting}{h1\textunderscore inter5\textunderscore err}{20}}
\@writefile{lol}{\contentsline {lstlisting}{h1\textunderscore inter6\textunderscore err}{20}}
\@writefile{lol}{\contentsline {lstlisting}{rinter.model.pl}{21}}
\newlabel{sec:h1:excompl:nondet}{{3.3.4}{21}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.4}Converting Alternating to Non-Deterministic Tree Automata}{21}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Lists starting with a number at least $3$ as recognized in state $q$ of Figure\nobreakspace  {}3\hbox {}}}{22}}
\newlabel{fig:rinterex}{{4}{22}}
\@writefile{lol}{\contentsline {lstlisting}{rinter\textunderscore nd.model.pl}{23}}
\newlabel{sec:h1:excompl:purge}{{3.3.5}{24}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.5}Purging Tree Automata}{24}}
\newlabel{sec:h1:excompl:det}{{3.3.6}{24}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.6}Determinizing Tree Automata}{24}}
\newlabel{eq:auto:det}{{5}{24}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces Eliminating intersection nodes from Figure\nobreakspace  {}4\hbox {}}}{25}}
\newlabel{fig:rinter_ndex}{{5}{25}}
\@writefile{lof}{\contentsline {figure}{\numberline {6}{\ignorespaces Purging the automaton of Figure\nobreakspace  {}5\hbox {}}}{26}}
\newlabel{fig:rinter_nd_purgedex}{{6}{26}}
\@writefile{lol}{\contentsline {lstlisting}{nondetex}{26}}
\@writefile{lol}{\contentsline {lstlisting}{rinter\textunderscore d.xml}{26}}
\@writefile{lol}{\contentsline {lstlisting}{rinter\textunderscore d.pl}{28}}
\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Determinizing the automaton of Figure\nobreakspace  {}6\hbox {}}}{29}}
\newlabel{fig:rinter_dex}{{7}{29}}
\newlabel{sec:h1:excompl:union}{{3.3.7}{29}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.7}Computing Unions, Transitive Closures}{29}}
\@writefile{lol}{\contentsline {lstlisting}{list\textunderscore even\textunderscore union\textunderscore tree3plus2.model.pl}{30}}
\@writefile{lol}{\contentsline {lstlisting}{list\textunderscore even\textunderscore union\textunderscore tree3plus2\textunderscore d.pl}{30}}
\@writefile{lof}{\contentsline {figure}{\numberline {8}{\ignorespaces Trees with leaves equal to $nil$ or to $3n+2$, or which are lists of even natural numbers}}{31}}
\newlabel{fig:unionex}{{8}{31}}
\@writefile{lol}{\contentsline {lstlisting}{rinter\textunderscore d\textunderscore plus.model.pl}{33}}
\@writefile{lof}{\contentsline {figure}{\numberline {9}{\ignorespaces Determinizing the automaton of Figure\nobreakspace  {}8\hbox {}}}{34}}
\newlabel{fig:union_dex}{{9}{34}}
\newlabel{sec:h1:excompl:neg}{{3.3.8}{35}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {3.3.8}Complete Deterministic Tree Automata, Taking Complements}{35}}
\@writefile{lol}{\contentsline {lstlisting}{agatha.model.pl}{36}}
\@writefile{lof}{\contentsline {figure}{\numberline {10}{\ignorespaces Why Agatha killed herself}}{37}}
\newlabel{fig:agatha_model}{{10}{37}}
\@writefile{lof}{\contentsline {figure}{\numberline {11}{\ignorespaces Why Agatha killed herself, deterministically}}{38}}
\newlabel{fig:agathad}{{11}{38}}
\newlabel{sec:h1:exns}{{3.4}{39}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}The Needham-Schroeder Symmetric Key Protocol Example}{39}}
\citation{Blanchet:Prolog}
\citation{NNS:H1}
\citation{NNS:H1}
\citation{JGL:H1}
\newlabel{sec:h1}{{4}{45}}
\@writefile{toc}{\contentsline {section}{\numberline {4}The {\tt  h1} Prover}{45}}
\newlabel{sec:h1:options}{{4.1}{45}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}How to Use {\tt  h1}}{45}}
\citation{JGL:H1}
\citation{GLP:VMCAI}
\citation{JGL:H1}
\citation{FSVY:Prolog:types=programs}
\citation{JGL:H1}
\newlabel{sec:h1:theory}{{4.2}{50}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Theoretical Background}{50}}
\newlabel{sec:h1:op}{{4.3}{50}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Principle of Operation}{50}}
\newlabel{sec:h1trace}{{5}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Explaining and Checking Proofs: {\tt  h1trace}, {\tt  h1logstrip}}{50}}
\newlabel{sec:h1mc}{{6}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Model-Checking Clause Sets and Explaining the Absence of Proofs with {\tt  h1mc}}{50}}
\newlabel{sec:h1mc:theory}{{6.1}{50}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}Theoretical Background}{50}}
\newlabel{sec:pldet}{{7}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {7}Determinizing Tree Automata with {\tt  pldet}}{50}}
\newlabel{sec:auto2pl}{{8}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {8}Converting XML Deterministic Tree Automata to Prolog Notation with {\tt  auto2pl}}{50}}
\newlabel{sec:plpurge}{{9}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {9}Cleaning and Extracting Automata with {\tt  plpurge}}{50}}
\newlabel{sec:pl2tptp}{{10}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {10}Converting Tree Automata and Prolog Programs to TPTP Files}{50}}
\newlabel{sec:tptpmorph}{{11}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {11}Applying Morphisms to $\mathcal  H_1$ Clause Sets with {\tt  tptpmorph}}{50}}
\newlabel{sec:linauto}{{12}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {12}Solving Presburger Arithmetic Formulas with {\tt  linauto}}{50}}
\newlabel{sec:autodot}{{13}{50}}
\@writefile{toc}{\contentsline {section}{\numberline {13}Displaying Automata with {\tt  pl2gastex}}{50}}
\bibstyle{abbrvnat}
\bibdata{h1}
\bibcite{Coq74}{{1}{1999--2003}{{Barras et~al.}}{{Barras, Boutin, Cornes, Courant, Filli{\^a}tre, Gim{\'e}nez, Herbelin, Huet, Mu{\~n}oz, Murthy, Parent, Paulin-Mohring, Saibi, and Werner}}}
\bibcite{Blanchet:Prolog}{{2}{2001}{{Blanchet}}{{}}}
\bibcite{ComonBoudet:Presburger}{{3}{1996}{{Boudet and Comon}}{{}}}
\bibcite{3French:oneclause}{{4}{1996}{{Devienne et~al.}}{{Devienne, Leb{\`e}gue, Parrain, Routier, and W{\"u}rtz}}}
\bibcite{FSVY:Prolog:types=programs}{{5}{1991}{{Fr{\"u}hwirth et~al.}}{{Fr{\"u}hwirth, Shapiro, Vardi, and Yardeni}}}
\bibcite{JGL:H1}{{6}{2005}{{Goubault{-}Larrecq}}{{}}}
\newlabel{sec:h1getlog}{{14}{53}}
\@writefile{toc}{\contentsline {section}{\numberline {14}Log Files and {\tt  h1getlog}}{53}}
\newlabel{sec:bugs}{{15}{53}}
\@writefile{toc}{\contentsline {section}{\numberline {15}Bugs}{53}}
\bibcite{JGL:JFLA04}{{7}{2004}{{Goubault-Larrecq}}{{}}}
\bibcite{GLP:VMCAI}{{8}{2005}{{Goubault{-}Larrecq and Parrennes}}{{}}}
\bibcite{NNS:H1}{{9}{2002}{{Nielson et~al.}}{{Nielson, Nielson, and Seidl}}}
\bibcite{Pelletier:75pbs}{{10}{1986}{{Pelletier}}{{}}}
\bibcite{Selinger:LACPV}{{11}{2001}{{Selinger}}{{}}}
\bibcite{SS:TPTP}{{12}{2002}{{Suttner and Sutcliffe}}{{}}}
\@writefile{toc}{\contentsline {section}{Concept Index}{55}}
\@writefile{toc}{\contentsline {section}{Command Index}{56}}
