\contentsline {section}{\numberline {1}Introduction}{2}
\contentsline {section}{\numberline {2}Tree Automata, Clauses}{6}
\contentsline {section}{\numberline {3}The {\tt h1} Tool Suite through Examples}{10}
\contentsline {subsection}{\numberline {3.1}A Toy, Introductory Example}{10}
\contentsline {subsection}{\numberline {3.2}The Dreadsbury Mansion Murder Mystery Example}{12}
\contentsline {subsection}{\numberline {3.3}Computing with Tree Automata}{14}
\contentsline {subsubsection}{\numberline {3.3.1}Visualizing Tree Automata}{16}
\contentsline {subsubsection}{\numberline {3.3.2}Computing Intersections of Tree Automata}{16}
\contentsline {subsubsection}{\numberline {3.3.3}Checking Tree Automata for Emptiness, Testing Membership}{19}
\contentsline {subsubsection}{\numberline {3.3.4}Converting Alternating to Non-Deterministic Tree Automata}{21}
\contentsline {subsubsection}{\numberline {3.3.5}Purging Tree Automata}{24}
\contentsline {subsubsection}{\numberline {3.3.6}Determinizing Tree Automata}{24}
\contentsline {subsubsection}{\numberline {3.3.7}Computing Unions, Transitive Closures}{29}
\contentsline {subsubsection}{\numberline {3.3.8}Complete Deterministic Tree Automata, Taking Complements}{35}
\contentsline {subsection}{\numberline {3.4}The Needham-Schroeder Symmetric Key Protocol Example}{39}
\contentsline {section}{\numberline {4}The {\tt h1} Prover}{45}
\contentsline {subsection}{\numberline {4.1}How to Use {\tt h1}}{45}
\contentsline {subsection}{\numberline {4.2}Theoretical Background}{50}
\contentsline {subsection}{\numberline {4.3}Principle of Operation}{50}
\contentsline {section}{\numberline {5}Explaining and Checking Proofs: {\tt h1trace}, {\tt h1logstrip}}{50}
\contentsline {section}{\numberline {6}Model-Checking Clause Sets and Explaining the Absence of Proofs with {\tt h1mc}}{50}
\contentsline {subsection}{\numberline {6.1}Theoretical Background}{50}
\contentsline {section}{\numberline {7}Determinizing Tree Automata with {\tt pldet}}{50}
\contentsline {section}{\numberline {8}Converting XML Deterministic Tree Automata to Prolog Notation with {\tt auto2pl}}{50}
\contentsline {section}{\numberline {9}Cleaning and Extracting Automata with {\tt plpurge}}{50}
\contentsline {section}{\numberline {10}Converting Tree Automata and Prolog Programs to TPTP Files}{50}
\contentsline {section}{\numberline {11}Applying Morphisms to $\mathcal H_1$ Clause Sets with {\tt tptpmorph}}{50}
\contentsline {section}{\numberline {12}Solving Presburger Arithmetic Formulas with {\tt linauto}}{50}
\contentsline {section}{\numberline {13}Displaying Automata with {\tt pl2gastex}}{50}
\contentsline {section}{\numberline {14}Log Files and {\tt h1getlog}}{53}
\contentsline {section}{\numberline {15}Bugs}{53}
\contentsline {section}{Concept Index}{55}
\contentsline {section}{Command Index}{56}
