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