\documentclass[12pt]{article}
\usepackage[latin1]{inputenc}
\usepackage[OT1]{fontenc}
\usepackage{fullpage}
\usepackage{graphicx}
\usepackage{url}
\usepackage{amssymb,times}
\usepackage[all]{xypic,xy}
\usepackage{listings}
\usepackage{moreverb}
\usepackage{natbib}
\usepackage{gastex}
\usepackage{multind}
\usepackage{hevea}
%HEVEA\tocnumber
%HEVEA\setcounter{cuttingdepth}{2}

%\lstloadlanguages{csh,prolog}
\usepackage{utils}

\newcommand\lstpl[1]{\lstinputlisting[language=Prolog,basicstyle=\sffamily,breaklines=true,frame=L]{#1}}
%\newcommand\pl[1]{\lstinline[language=Prolog,basicstyle=\sffamily,breaklines=true,frame=L]{#1}}
\newcommand\lstxml[1]{\lstinputlisting[language=XML,basicstyle=\small,breaklines=true,frame=L]{#1}}

\makeindex{indexC}
\makeindex{indexN}
\renewcommand\bold[1]{\textbf{#1}}

\newcommand\nat{\mathbb{N}}
%HEVEA\renewcommand\nat{\mbox{|N}}
\newcommand\knows{\mathtt{knows}}
\newcommand\provided{\mbox{:--}}
%HEVEA\renewcommand\provided{ \mbox{:-} }

\title{The {\tt h1} Tool Suite}
\author{Jean Goubault-Larrecq\\
  \begin{tabular}{c}
    LSV/UMR 8643, CNRS, ENS Cachan \& INRIA Futurs projet SECSI\\
    61 avenue du président-Wilson, F-94235 Cachan Cedex \\
    {\small\tt goubault@lsv.ens-cachan.fr} \\
    Phone: +33-1 47 40 75 68 \quad Fax: +33-1 47 40 75 21
  \end{tabular}
}

\begin{document}
\maketitle

\begin{abstract}
  This describes the theoretical basis and practical usage of the {\tt h1}
  tool suite.  This is a set of tools that allow one to handle tree-regular
  languages in various formats, including deterministic, non-deterministic,
  and alternating finite tree automata, but also various fairly general
  clausal formats, the central one being the $\mathcal H_1$ class due to
  Nielson, Nielson, and Seidl.  Alternatively, this can also be seen as a
  terminating automated theorem prover for the $\mathcal H_1$ class; or as an
  automated theorem prover for general clause sets, which however makes some
  controlled mistakes in the spirit of abstract interpretation: this is
  notably useful in proofs of security protocols.  Other aspects of the {\tt
    h1} tool suite include producing certain forms of automated proofs by
  induction in the Coq proof assistant, deciding Presburger arithmetic, and
  displaying tree automata.
\end{abstract}

\begin{latexonly}
  \tableofcontents
\end{latexonly}

\section{\label{sec:intro}Introduction}

The {\tt h1} tool suite is a toolchest for handling finite tree
automata, in various forms.  There are basically three forms, from
most constrained to least constrained:
\begin{enumerate}
\item as deterministic bottom-up tree automata;
\item as alternating tree automata;
\item as pure Prolog programs (sets of Horn clauses) in the $\mathcal H_1$
  class \citep{NNS:H1}.
\end{enumerate}

The global architecture is given in the following figure.  Some things are
still missing from it, and we will add them progressively later.  The inner
dashed box forms the {\em core\/} of the {\tt h1} tool suite.  The outer
dashed box is the {\tt h1} tool suite itself.

\begin{center} % 60%
%BEGIN IMAGE
  \includegraphics[scale=0.95]{h1.1.eps}
%END IMAGE
%HEVEA\imageflush
\end{center}
The main thing to understand is that the {\tt h1} tool suite includes tools to
convert between all three formats of tree automata, forming the core of the
{\tt h1} tool suite.  The tools {\tt h1}, {\tt pldet}, {\tt auto2pl}, {\tt
  pl2tptp} are used to navigate between all three formats.

In the {\tt h1} tool suite, {\em deterministic tree automata\/} are
represented in files in XML format.

{\em Alternating tree automata\/} are represented as Horn clauses, in
Prolog notation; in particular, you can run them in any Prolog implementation
(whatever the use of this may be).

Finally, {\em $\mathcal H_1$ clause sets\/} are represented in TPTP format.
TPTP (a Thousand Problems for Theorem Provers) is a publicly available
repository used to test automated theorem provers, due to \citet{SS:TPTP}. The
{\tt h1} tool suite handles TPTP input files that contain only clauses. This
allows you to use any automated, clausal theorem prover in place of the {\tt
  h1} prover if you so wish.  The {\tt h1} prover, one of the tools of the
{\tt h1} tool suite, is an automated theorem prover.  In addition to searching
for proofs, it is also able to produce counter-models and describe them as
alternating tree automata; {\tt h1} is described in Section~\ref{sec:h1}.

Additional tools operate on such counter-models and proofs.  They form
the rest of the {\tt h1} tool suite.  As far as proofs are concerned,
the {\tt h1} tool keeps a trace of all proof steps it did in a {\em
  trace log\/}.  This trace log is in a proprietary format that the
{\tt h1trace} and {\tt h1logstring} tools can work on.  (Don't assume
anything on this format, it may change in the future.)  This is
pictured in the following figure.

\begin{center} % 60%
%BEGIN IMAGE
  \includegraphics[scale=0.95]{h1.2.eps}
%END IMAGE
%HEVEA\imageflush
\end{center}

The purpose of {\tt h1trace} is to explain the proofs found by {\tt
  h1}, both to humans, as a proof in natural deduction in text format,
and to machines, as a formal proof, in Coq notation.  Coq is a proof
assistant developed in the LogiCal team at INRIA Futurs \citep{Coq74}.
% Since proof traces in {\tt .log} format, as produced by {\tt h1} and
% read by {\tt h1trace} are huge, they are output by {\tt h1} in {\tt
%   gzip}-compressed format.  You may use the standard tool {\tt zcat}
% in place of {\tt cat} to read such compressed files.  More in
% Section~\ref{sec:h1trace}.

The {\tt h1} tool is also able to work on general clause sets, not just in the
$\mathcal H_1$ format.  In this case, {\tt h1} will output a proof candidate,
which however may fail to be a proof.  In case this is a wrong proof, {\tt
  h1trace} will do its best to explain the wrong proof to humans.  This can be
used to design a true proof.

%The {\tt h1trace} tool is described in Section~\ref{sec:h1trace}.

%!!!

In case a prover does not find a proof of some given query, you usually have
no choice but to trust it that there is indeed no proof. In case {\tt h1} does
not find a proof of some given query, it outputs a model.  This model can be
independently checked by the {\tt h1mc} model-checking tool; {\tt h1mc} takes
as input both a description of the model $\mathcal M$, as an alternating tree
automaton, and a trace log obtained from some given clause set $S$, and checks
whether the clauses in $S$ all hold in the model $\mathcal M$.  This is a way
of getting confident that there is indeed no proof of the initial query, i.e.,
that your query is wrong.  More useful is the fact that {\tt h1mc} can give
you an explanation, based on $\mathcal M$, why you query is wrong.  As with
{\tt h1trace}, this explanation can be made for humans, in text format, or in
Coq format, to be checked independently by the Coq proof assistant.  This is
important in security protocols for instance, where a proof of secrecy
consists in showing that there is no proof of the fact that the intruder can
get hold of a given secret.  This was shown by \citet{Selinger:LACPV}, see
\citet{JGL:JFLA04}.  Adding {\tt h1mc} gives you the following picture of the
{\tt h1} tool suite.

\begin{center} % 60%
%BEGIN IMAGE
  \includegraphics[scale=0.95]{h1.3.eps}
%END IMAGE
%HEVEA\imageflush
\end{center}

The {\tt h1mc} tool is described in Section~\ref{sec:h1mc}.

% and also to produce formal proofs of both the proved goals and
%the fact that the unproved goals are indeed unprovable, in Coq notation.

Additionally, various tools are provided.  First, there are two
conversion utilities, {\tt auto2pl}, which converts deterministic tree
automata in XML format into Prolog format (Section~\ref{sec:auto2pl});
and {\tt pl2tptp}, which converts alternating tree automata in Prolog
format into TPTP format (Section~\ref{sec:pl2tptp}).  Since every
deterministic tree automaton is a particular case of an alternating
tree automaton, and every alternating tree automaton is a particular
case of an $\mathcal H_1$ clause set (see Section~\ref{sec:theory}),
these two utilities entail no loss of information.  In particular, to
convert deterministic tree automata into $\mathcal H_1$ clause sets,
just run {\tt auto2pl} on the former, getting an intermediate file
which you then convert to $\mathcal H_1$ clause sets using {\tt
  pl2tptp}.

Then, there are miscellaneous utilities. The first, {\tt plpurge},
extracts the part of a tree automaton that is relevant to certain
final states.  In other words, it reads a tree automaton in Prolog
format, and eliminates all states and transitions that do not reach
any final state.  This cleaning step is useful to help understand the
structure of automata computed by {\tt h1}, in particular as a
preparation to calling {\tt pl2gastex}.  The {\tt plpurge} tool is
described in Section~\ref{sec:plpurge}.  The second, {\tt tptpmorph},
applies certain kinds of morphisms to languages represented as
$\mathcal H_1$ clause sets. This is described in
Section~\ref{sec:tptpmorph}.  The need for it should become apparent
in conjunction with {\tt linauto}, which implements
\citet{ComonBoudet:Presburger}'s algorithm for deciding
quantifier-free Presburger formulae by converting them to automata.
While {\tt linauto} only deals with {\em quantifier-free\/} formulae,
existential quantification can be dealt with by using {\tt tptpmorph},
and universal quantification can be implemented using existential
quantification and complementation.  Complementation can be
implemented by determinization (using {\tt pldet}) and using {\tt
  auto2pl} with the {\tt -negate} option.  The {\tt linauto} tool is
described in Section~\ref{sec:linauto}.

Finally, {\tt pl2gastex} is a utility that converts alternating tree
automata to a sequence of gas\TeX{} macros, which can then be used in
conjunction with \LaTeX{} to display them on screen or include them in
documents.  A former attempt of a tree automaton visualizer is
provided with {\tt autodot}.  The latter converts deterministic tree
automata to files in {\tt dot} format; {\tt dot} can then be applied
to these files to display them graphically.  This is only useful for
relatively small automata, and is far from perfect for tree automata
that are not just word automata.  Don't expect too much from {\tt
  pl2gastex} and {\tt autodot} on anything else but small automata.
The {\tt autodot} utility is obsolescent: basically, it never gives
satisfying output.  The {\tt pl2gastex} utility is more satisfactory,
but not perfect.  See Section~\ref{sec:autodot}.

At this point the picture of the {\tt h1} tool suite is complete---up to the
fact that I did not talk about some minor extensions yet, and that more
extensions may be added in the future.
%Typically h1getlog.

\begin{center} % 60%
%BEGIN IMAGE
  \includegraphics[scale=0.95]{h1.4.eps}
%END IMAGE
%HEVEA\imageflush
\end{center}



\section{\label{sec:theory}Tree Automata, Clauses}

Automata on finite words are a very classical data structure to represent sets
of words---possibly infinite sets.  Not all sets of words can be described
this way; such special sets are called {\em regular\/} languages.  Regular
languages are reasonably expressive, and all the basic operations are
computable on them: testing for membership, for vacuity, computing unions,
intersections, complements notably.

An example of automaton is shown below.  This is just a directed
graph.  Vertices are traditionally called {\em states\/}, and edges
are called {\em transitions\/}.  Two other components are needed.
First, we need an {\em initial state\/}: in the example, we assume
this is $q_{init}$.  Second, we need {\em final states\/}.  The
convention is that final states are circled; here, the only final
state is $q_{init}$.
\begin{center}
%BEGIN IMAGE
  \includegraphics{auto.eps}
%END IMAGE
%HEVEA\imageflush
\end{center}

Let us play a game.  You start at the initial state $q_{init}$, then
you must follow some transitions (whichever you wish, you may even
repeat the same transition as long as you wish), until you reach a
final state.  While traveling around, collect the letters that label
the transitions: this gives you a sequence of letters, i.e., a {\em
  word\/}. (One exception, though: the $\epsilon$ symbols means ``no
letter'', and you should just go through the corresponding transition
without collecting any letter at all.) The fact that you reached the
final state is how you decide that the automaton {\em recognized\/}
the word.

For example, starting from $q_{init}$, you may go up the $a$
transition, then come back along the $\epsilon$ transition.  Since
you've reached a final state, namely $q_{init}$ (which is both initial
and final), the word $a$ is recognized by the automaton.  Or you may
have decided to start from $q_{init}$, go up the $a$ transition, turn
once inside the $b$ loop, then come back through the
$\epsilon$-transition: the word $ab$ is recognized.  In fact, you
might have looped as many times as you wished, so any word $ab^n$, $n
\in \nat$, is recognized, too.

There is no need to stop when you reach a final state.  For example, we may
travel along $a$, then $b$ twice, then along $\epsilon$, then again along $a$, then
$b$ three times, then $\epsilon$, showing that $ab^2ab^3$ is recognized.  While we
are at it, since $q_{init}$ is already final, the empty word (with no letter)
is also recognized.  We write $\epsilon$ for the empty word, as is traditional.

To wrap up the example, the above automaton recognizes exactly the language
$(a b^*)^*$, that is the set of all words on the alphabet $\{a,b\}$ which are
concatenations of words $a b^n$, $n\in \nat$.  It turns out that this is just
the set of words that, if non-empty, start with $a$.

Alternatively, we can describe this same set of words as a set of Horn
clauses, i.e., as a very simple Prolog program.  To this end, create a fresh
predicate symbol $q$ for each state $q$.  The meaning of $q(t)$ is that the
word $t$ should be {\em recognized at $q$\/}, i.e., there is a trip along the
transitions in the automaton, starting from the initial state, and ending
exactly on the state $q$, along which the letters collected  form the word
$t$.  We also encode words as terms: $\epsilon$ will be a constant denoting the empty
word, and we add each letter $\ell$ at the end of word $t$ by writing the term $\ell
(t)$; this means in particular that each letter is now viewed as a unary
function symbol.  The automaton above then gets described as a Prolog program
with one clause for each transition, plus one to say that the empty word is
recognized at the initial state:
\begin{eqnarray*}
  q_{init} (\epsilon) &   & q_1 (a (X)) \provided q_{init} (X) \\
  q_1 (b (X)) \provided q_1 (X) &   & q_{init} (X) \provided q_1 (X)
\end{eqnarray*}
You may ask Prolog whether the word $ab^2$ is recognized at $q_{init}$
by submitting the query
\[
?q_{init} (b (b (a (\epsilon))))
\]
and it will answer ``yes''.  Prolog will also answer the query
\[
?q_{init} (b (b (a (b (\epsilon)))))
\]
by ``no'', meaning that $bab^2$ is not in the language.

Prolog, as a notation, is fine, as we shall see.  Prolog, as a tool to check
properties, is ill-suited: on the more complex clauses we shall encounter
below, Prolog would loop infinitely in general; {\tt h1} on the other hand is
meant to return, always, on its input clauses.

The notion of automata, on words, can be generalized to automata on
first-order terms, a.k.a., {\em tree automata}.  These are very
similar structures, except they recognize sets of ground terms.  The
automaton of Figure~\ref{fig:listeven}, to take an example, recognizes
the set of all lists of even natural numbers at state
$q_{\mathrm{list-even}}$.  To be precise, it recognizes the set of all
terms ${\tt cons} (t_1, \allowbreak {\tt cons} (t_2, \allowbreak
\ldots, \allowbreak {\tt cons} (t_n, \allowbreak {\tt nil})
\allowbreak \ldots))$, where each $t_i$ is of the form ${\tt S}^{n_i}
({\tt O})$, $n_i$ even.  Note that the transition ${\tt O}$ (up left)
starts from no state, while the transition ${\tt cons} (\_, \_)$
(middle) starts from a pair of states, $q_{\mathrm{even}}$ and
$q_{\mathrm{list-even}}$.
\begin{figure}[htbp]
\caption{\label{fig:listeven}Recognizing the lists of even natural numbers}
\begin{center}
%BEGIN IMAGE
  \includegraphics{listeven.eps}
%END IMAGE
%HEVEA\imageflush
\end{center}
\end{figure}

To define the semantics of tree automata, the simplest is just to describe
their translation to Horn clauses.  Each transition again gives rise to
exactly one clause:
\begin{eqnarray*}
  q_{\mathrm{even}} ({\tt O}) & q_{\mathrm{even}} ({\tt S} (X)) \provided
  q_{\mathrm{odd}} (X) & q_{\mathrm{odd}} ({\tt S} (X)) \provided
  q_{\mathrm{even}} (X) \\
  & q_{\mathrm{list-even}} ({\tt cons} (X, Y)) \provided q_{\mathrm{even}}
  (X), q_{\mathrm{list-even}} (Y) & q_{\mathrm{list-even}} ({\tt nil})
\end{eqnarray*}
There is no need to define initial states in tree automata; e.g., ${\tt O}$ is
recognized at $q_{\mathrm{even}}$, using the transition $q_{\mathrm{even}}
({\tt O})$, of arity $0$.

In general, a {\em tree automaton\/} is any finite set $S$ of clauses of the
form
\begin{eqnarray}
  \label{eq:pop}
  P (f (X_1, \ldots, X_n)) & \provided & P_1 (X_1), \ldots, P_n (X_n)
\end{eqnarray}
where $X_1$, \ldots, $X_n$ are pairwise distinct variables.  When $n=0$, we
retrieve initial clauses such as $q_{\mathrm{even}} ({\tt O})$.  When $n$ is
restricted to be at most $1$, tree automata are just ordinary, word automata
(without $\epsilon$-transitions).

A set of ground terms is called {\em regular\/} if and only if it is exactly
the set of terms $t$ such that $t$ is recognized at $P$ in some tree automaton
$S$ (i.e., such that $P (t)$ follows logically from the clauses in $S$).

The format of clauses (\ref{eq:pop}) is very particular.  First, clauses
(\ref{eq:pop}) are definite clauses.  Formally, {\em definite clause\/} are
implications of the form
\begin{equation}
  \label{eq:definite}
  P (t) \provided P_1 (t_1), \ldots, P_n (t_n)
\end{equation}
where $P (t)$, $P_1 (t_1)$, \ldots, $P_n (t_n)$ is an unordered set of atoms.  (An
{\em atom\/} is just a predicate $P$ applied to some term $t$; read ``$P$
holds of $t$'', or ``$t$ is recognized at $P$''.)  If $n=0$, this is called a
{\em fact}, and is often written just $P (t)$.

Any set $S$ of definite clauses has a {\em least Herbrand model\/}.  A
{\em Herbrand model\/} is just a collection of ground atoms $P (t)$.
The least Herbrand model $\mathcal H (S)$ of $S$ can be described as
follows.  First, it contains all ground instances of the facts in $S$.
Then, while there is a ground instance $P (t \sigma) \provided P_1
(t_1 \sigma), \ldots, P_n (t_n \sigma)$ of a clause $P (t) \provided
P_1 (t_1), \ldots, P_n (t_n)$ in $S$, and $P_1 (t_1 \sigma)$, \ldots,
$P_n (t_n \sigma)$ are in $\mathcal H (S)$, then add $P (t \sigma)$ to
$\mathcal H (S)$.  This procedure does not terminate in general, but
enumerates $\mathcal H (S)$.

In particular, any tree automaton has a least Herbrand model.  It turns out
that the ground atom $P (t)$ is in the least Herbrand model $\mathcal H (S)$
if and only if $t$ is recognized at $P$ in the tree automaton $S$.  Therefore,
we may generalize the notion of a term $t$ being recognized at some predicate
$P$ in any set of definite clauses, by requiring that $P (t)$ is in $\mathcal
H (S)$.

A {\em goal clause\/} is an implication of the form
\begin{equation}
  \label{eq:goal}
  \bot \provided P_1 (t_1), \ldots, P_n (t_n)
\end{equation}
where $\bot$ is meant to denote false.  A {\em Horn clause\/} is a definite or a
goal clause.
%\end{definition}
%  We shall simply say clause instead of Horn clause, since we shall only
 %  consider Horn clauses in this paper.
We shall also write $P (t)$ instead of $P (t) \provided$ when $n=0$, and
$\bot$ instead of $\bot \provided$.

Not any set $S$ of Horn clauses has a model.  If it has one, that is, if $S$
is {\em satisfiable\/}, then it again has a least Herbrand model $\mathcal H
(S)$.  Again, we say that $t$ is recognized at $P$ in $S$ if and only if $P
(t)$ is in $\mathcal H (S)$.

Then it can be shown that the ground term $t$ is recognized at $P$ in
the set $S$ of definite clauses if and only if $S$ plus the goal
clause $\bot \provided P (t)$ is {\em unsatisfiable\/} (i.e., not
satisfiable); that $P$ is {\em empty\/} in $S$, i.e., that $P$
recognizes no term in $S$, if and only if $S$ plus the clause $\bot
\provided P (X)$ is unsatisfiable, where $X$ is a variable.  And there
are automated means, called automated theorem provers, to check the
unsatisfiability of clause sets.  Unfortunately, they do not always
terminate.  The {\tt h1} tool always terminates, but only deals with
so-called $\mathcal H_1$ clauses \citep{NNS:H1}.

We have said above that tree automata clauses (\ref{eq:pop}) were very
particular, because they were definite clauses, and in particular they
always have a least Herbrand model.  They are also particular in that
the {\em head\/} (the atom at the left of $\provided$) is restricted
to be of the form $P (t)$ with $t$ itself of the form $f (X_1, \ldots,
X_n)$, where $X_1$, \ldots, $X_n$ must be distinct variables; and in
that there is no function symbol at all in the {\em body\/} (the set
of atoms at the right of $\provided$).

If you do not restrict the form of Horn clauses (\ref{eq:definite})
and (\ref{eq:goal}), then any prover that operates on them is forced
to relinquish either termination, soundness, or completeness.  This is
because the satisfiability of Horn clauses is {\em undecidable\/}
\citep{3French:oneclause}.  Most automated theorem provers in
existence are {\em sound\/}, i.e., if they deduce a contradiction from
$S$ then $S$ is unsatisfiable, and {\em complete\/}, i.e., if $S$ is
unsatisfiable then they can derive a contradiction from $S$.
Therefore they have to fail to terminate sometimes.  On the other
hand, {\tt h1} is complete and terminates, but is only sound on the
subset of so-called $\mathcal H_1$-clauses.

The {\em $\mathcal H_1$-clauses} are exactly the Horn clauses, except
that definite clauses (\ref{eq:pop}) are restricted to have a head of
the form $P (X)$, where $X$ is a variable, or $P (f (X_1, \ldots, X_n))$,
where $X_1$, \ldots, $X_n$ are distinct variables.  While this is not the
definition \citet{NNS:H1}, this is equivalent to it, see
\citet{JGL:H1}.

On general Horn clauses, {\tt h1} applies an abstraction function
which makes it still a terminating and complete prover, but one which
is unsound in general.  So you might want to see {\tt h1} as a
counter-model finder rather than a prover.  In some cases, though,
{\tt h1} produces unsound ``proofs'' that may be indicative of actual
proofs.

Remember that {\tt h1} is sound, complete, and terminating on
$\mathcal H_1$ clauses.  Note that automata clauses are a special case
of $\mathcal H_1$ clauses.  In fact, when {\tt h1} terminates,
starting from a set $S$ of $\mathcal H_1$ clauses, there are two
possible outcomes:
\begin{itemize}
\item a contradiction has been derived; then $S$ is unsatisfiable.
\item no contradiction was derived; then $S$ is satisfiable.
\end{itemize}
In the latter case, {\tt h1} also produces a model of $S$, in the form of an
{\em alternating tree automaton}, i.e., a set of clauses of the form
\begin{eqnarray}
  \label{eq:alt}
  P (f (X_1, \ldots, X_n)) & \provided & B_1 (X_1), \ldots, B_n (X_n)
\end{eqnarray}
where $B_i (X_i)$ is a {\em block\/}, i.e., a list of atoms $P_{i1}
(X_i), \ldots, P_{in_i} (X_i)$.  Note that tree automata clauses are a
special case of alternating tree automata clauses (take $n_i=1$ for
each $i$), while alternating tree automata clauses are special
$\mathcal H_1$ clauses (with no function symbol in the body, the head
is of the form $P (f (X_1, \ldots, X_n))$ and not $P (X)$, and every
variable free in the body is among $X_1, \ldots, X_n$).

From a theoretician's perspective, this means that $\mathcal H_1$
clauses are not more expressive than alternating tree automata
clauses.  And it is well-known that alternating tree automata are not
more expressive than plain tree automata: the languages defined by
satisfiable $\mathcal H_1$ clause sets are just, again, the regular
tree languages.  However, $\mathcal H_1$ offers considerably more
freedom in describing such languages than just using tree automata,
because of the general form of $\mathcal H_1$ clauses.

The paper that introduced $\mathcal H_1$ is \citet{NNS:H1}.  For some
background theory on the way {\tt h1} works, deciding $\mathcal H_1$
and converting $\mathcal H_1$ clause sets to tree automata by
resolution techniques, and abstracting general clause sets to
$\mathcal H_1$ clause sets, see \citet{JGL:H1}.

% clauses; H1 clauses; alternating tree automata; non-deterministic TA;
% deterministic TA.

% complementation is Prolog negation.  Can be computed on tree automata.

% also, word automata (because of linauto).

\section{\label{sec:examples}The {\tt h1} Tool Suite through Examples}

The {\tt h1} prover is the core of the {\tt h1} tool suite, and we
shall explain the tool suite by running {\tt h1} on several examples.

The {\tt h1} prover is invoked by calling {\tt h1} with a sequence of
flags, ended by a file name.  The file name should contain a set of
clauses in TPTP clause format.  Such files conventionally end with the
{\tt .p} extension---but there is no obligation.  Also, giving a
single dash {\tt -} as file name forces {\tt h1} to read the input
clause set from standard input.


\subsection{\label{sec:h1:ex}A Toy, Introductory Example}


Examples are given in the distribution package.  Here is a very small
one (file \url{test1.p}):

%BEGIN IMAGE
\lstinputlisting[language=tptp,frame=L]{test1.p}
%END IMAGE
%HEVEA\imageflush

%\begin{verbatim}
%input_clause (clause1, conjecture,
%             [++p(a)]).
%input_clause (clause2, conjecture,
%             [--p(X), ++p(f(X))]).
%input_clause (clause3, conjecture,
%             [--p(f(f(X)))]).
%\end{verbatim}
This contains three clauses.  Each clause is introduced by the keyword
\lstinline[language=tptp]{input_clause}.  The first argument,
\lstinline[language=tptp]{clause1},
\lstinline[language=tptp]{clause2}, or
\lstinline[language=tptp]{clause3} above, is the name of the clause.
Names are used in sundry ways, mainly for explanation and
documentation purposes.  It is good practice to give each clause a
different name, but the tools of the {\tt h1} tool suite should work
even when several clauses have the same name.

The second argument can be the keyword
\lstinline[language=tptp]{conjecture} or
\lstinline[language=tptp]{axiom}; {\tt h1} just does not care: write
what you prefer here.

Finally, the third argument, enclosed between square brackets, is the
clause itself.  It is a list of literals, separated by commas.  Each
literal starts with a sign, \lstinline[language=tptp]{++} for positive
literals, \lstinline[language=tptp]{--} for negative literals.  The
clauses above are, in a more traditional notation:
\begin{eqnarray*}
  & p(a) & \\
  & ¬ p (X) \lor p (f (X)) & \\
  & ¬ p (f (f (X)))
\end{eqnarray*}
This example is in fact a set of Horn clauses, which would be written
in Prolog notation:
\begin{eqnarray*}
  p (a) && \\
  p (f (X)) & \provided & p (X) \\
  \bot & \provided & p (f (f (X)))
\end{eqnarray*}

Launch {\tt h1} on this file, \url{test1.p}, by typing
\verbatimtabinput{h1_test1}
You will get the answer
\lstinputlisting[frame=l]{h1_test1_err}
%\begin{lstlisting}[frame=l]{}
%*** Derived: clause3 ***
%\end{lstlisting}
which means that a contradiction was found, using the clause named
\lstinline:clause3: in the last step.  In other words, in the present
example, it says that a fact of the form $p (f (f (t)))$, matching the
body of \lstinline:clause3:, can be deduced from the definite clauses
(here, \lstinline:clause1: and \lstinline:clause2:)

So far, so good, this is typically the least you could expect from a
theorem prover.

However, {\tt h1} also produced two more files, \url{test1.log}
and \url{test1.model.pl}.  If you're curious, look at
\url{test1.log}, by running
% \index{indexN}{zcat@{\tt zcat}}
% \verbatimtabinput{zcat_test1}
\index{indexN}{less@{\tt less}}
\verbatimtabinput{cat_test1}
% We get
% \lstinputlisting[language=tptp,frame=L]{../test1.log}

Oh well, it is long, but it is not meant to be read by a human reader!
If you're perspicuous enough, you'll find some meaning buried inside
this.  However, this is really meant as a log file, from which {\tt
  h1trace} can extract a (mostly) readable proof
(Section~\ref{sec:h1trace}), and which {\tt h1mc} can use to get some
essential information it needs (Section~\ref{sec:h1mc}).



\subsection{\label{sec:h1:expb55}The Dreadsbury Mansion Murder Mystery Example}

Here is a more complicated example, due to Len Schubert.  This is
problem~55 of \citet{Pelletier:75pbs}.
%, as reformulated by \citet{Satchmo}:
\begin{quote}
  Someone in Dreadsbury Mansion killed Aunt Agatha.  Agatha, the
  butler, and Charles live in Dreadsbury Mansion, and are the only
  ones to live there.  A killer always hates, and is no richer than
  his victim.  Charles hates noone that Agatha hates.  Agatha hates
  everybody except the butler.  The butler hates everyone not richer
  than Aunt Agatha.  The butler hates everyone whom Agatha hates.
  Noone hates everyone.  Who killed Agatha?
\end{quote}

The problem is formalized in file \url{butler-puzzle.p}.  The clauses
are as follows.  First, ``Agatha, the butler, and Charles live in
Dreadsbury Mansion, and are the only ones to live there.'':
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:agatha_in_mansion: & \mathtt{in\_mansion} (agatha) && \\
  \lstinline[language=tptp]:charles_in_mansion: & \mathtt{in\_mansion} (charles) && \\
  \lstinline[language=tptp]:butler_in_mansion: & \mathtt{in\_mansion} (butler) &&
\end{array}
\]
Then, ``A killer always hates, and is no richer than his victim.'',
that is, if $X$ killed $Y$, then it must be the case that $X$ hates
$Y$, and on the other hand that $X$ is not richer than $Y$:
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:killer_hates_victim: & \mathtt{hates} (X,Y) & \provided & \mathtt{killed} (X,Y) \\
  \lstinline[language=tptp]:killer_no_richer: & \mathtt{not\_richer} (X,Y) & \provided & \mathtt{killed} (X,Y)
\end{array}
\]
Next, ``Charles hates noone that Agatha hates.''  In other words, it
is impossible that Charles and Agatha hate the same person $X$:
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:charles_hates_noone_agatha_hates: & \bot & \provided &
  \mathtt{hates} (charles,X), \mathtt{hates} (agatha,X)
\end{array}
\]
To write ``Agatha hates everybody except the butler.'', we just say
that Agatha hates herself and Charles:
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:Agatha_hates_herself: & \mathtt{hates} (agatha, agatha) && \\
  \lstinline[language=tptp]:Agatha_hates_charles: & \mathtt{hates} (agatha, charles) &&
\end{array}
\]
Now, ``The butler hates everyone not richer than Aunt Agatha.'':
\[
\setlength\arraycolsep{2pt}
\begin{array}{lrcl}
  \lstinline[language=tptp]:butler_hates_everyone_not_richer_than_agatha: &
  \mathtt{hates} (butler, X) & \provided & \mathtt{not\_richer} (X, agatha)
\end{array}
\]
Then, ``The butler hates everyone whom Agatha hates.'':
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:butler_hates_everybody_agatha_hates: &
  \mathtt{hates} (butler, X) & \provided & \mathtt{hates} (agatha, X)
\end{array}
\]
Next, ``Noone hates everyone.'', which we formulate as ``noone
hates Agatha, Charles, and the butler'':
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:noone_hates_everyone: &
  \bot & \provided & \mathtt{hates} (X,agatha), \mathtt{hates} (X,butler), \mathtt{hates} (X, charles)
\end{array}
\]
Finally, we explore who may have killed Aunt Agatha.  To do this, we
shall enumerate the potential murderers, and use the C preprocessor
{\tt cpp} to replace the macro identifier {\tt WHO} in the following
clause by each resident of Dreadsbury Mansion:
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:WHO_killed_agatha: &
  \mathtt{killed} (\lstinline[language=tptp]:WHO:, agatha)
\end{array}
\]
Let us test whether the butler killed Agatha.  Run \url{butler-puzzle.p}
 through {\tt cpp} with {\tt WHO} equal to {\tt
  butler}, and feed the output to {\tt h1}; {\tt h1} reads from
standard input when given {\tt -} as file name:
\index{indexN}{cpp@{\tt cpp}}
\verbatimtabinput{butler1}
You get the output:
\lstinputlisting[frame=l]{butler1_err}
In other words, the butler cannot have killed Agatha (contrarily to
proper conventions in popular whodunnit mysteries), because this would
contradict the fact that noone hates everyone.

More information can be gotten from the trace file \url{h1out.log}.
(Running {\tt h1} on file $\langle$file$\rangle$.p produces a trace file
$\langle$file$\rangle$.log.  If no input file is given, as here, the trace file
is called \url{h1out.log}.)  We shall explain how to use this trace
file in Section~\ref{sec:h1trace}.  For now, just run
\index{indexN}{h1trace@{\tt h1trace}}
\verbatimtabinput{butler2}
and open the file {\tt dummy}.  You'll see that the first lines say:
\begin{lstlisting}[frame=l]{}
  . #false(noone_hates_everyone)  [noone_hates_everyone].
  using assumption #false(noone_hates_everyone) :-
       hates(X1,charles), hates(X1,butler), hates(X1,agatha).
    {X1=butler}
\end{lstlisting}
In other words, assuming the butler killed Agatha would involve that
the butler hates everyone, which is impossible.  The rest of file {\tt
  dummy} is a tree-like proof that indeed the butler hates everyone,
i.e., hates Agatha, Charles, and himself in this case.

So did Charles kill Agatha instead?
\index{indexN}{cpp@{\tt cpp}}
\verbatimtabinput{butler3}
No, this would contradict the fact that Charles hates noone that
Agatha hates.  In this case, Charles hates Agatha, and Agatha hates
herself, whence the contradiction.
\lstinputlisting[frame=l]{butler3_err}

There is only one possibility remaining: that Agatha killed herself.
\index{indexN}{cpp@{\tt cpp}}
\verbatimtabinput{butler4}
and indeed, {\tt h1} does not complain: assuming Agatha killed herself
leads to no contradiction.  The file \url{h1out.model.pl} describes
the least model of this clause set.

This could have been found automatically by a simple {\tt sh} script,
listing all possible murderers of Aunt Agatha.
\index{indexN}{cpp@{\tt cpp}}\index{indexN}{grep@{\tt grep}}
\verbatimtabinput{butler5}
Since somebody killed Agatha, it must be herself.
\lstinputlisting[frame=l]{butler5_err}

The point of this example is that, first, the clauses are clearly not
(alternating tree) automata clauses; and second, that they are
$\mathcal H_1$ clauses.  Check this by running {\tt h1} with the {\tt
  -check-h1 2} option%
\index{indexN}{check-h1@{\tt -check-h1}}%
:
\index{indexN}{cpp@{\tt cpp}}\index{indexN}{check-h1@{\tt -check-h1}}
\verbatimtabinput{butler6}
This makes {\tt h1} run as above, except it would have failed if any
of the input clauses where not in $\mathcal H_1$.  By default, {\tt
  h1} runs as {\tt h1 -check-h1 0}, which does not check anything, but
computes an approximation, see Section~\ref{sec:h1:exns}.

That the clauses of \url{butler-puzzle.p} are in the $\mathcal H_1$
class may seem surprising.  After all, $\mathcal H_1$ clauses are
required to use only {\em unary\/} predicates, i.e., all predicate
letters $P$ can only take one argument.  This is certainly not the
case of the $\mathtt{hates}$, $\mathtt{killed}$, and
$\mathtt{not\_richer}$ predicates above, which are all binary!

The trick here is that, when {\tt h1} sees an $n$-ary predicate $P
(t_1, \ldots, t_n)$ in its input, it converts it first to $P (f_P
(t_1, \ldots, t_n))$ for some fresh $n$-ary function symbol $f_P$.
(Different occurrences of $P$ correspond to the same symbol $f_P$.)
This makes $P$ unary, and does not change the semantics of clauses in
any essential way.  Under the hood, {\tt h1} typically builds $f_P$ by
prepending a sharp sign \verb/#/ in front of the name of $P$,
guaranteeing that no clash occurs with any function symbol you may
have used.  Don't count on it, though, as this may change in future
releases.  Also, the {\tt h1} tools try to hide this kludge as much as
they can, and will happily parse and print $n$-ary predicate symbols.

We shall return to this example in Section~\ref{sec:h1:excompl:neg}.


\subsection{\label{sec:h1:excompl}Computing with Tree Automata}


Assume that we wish to compute the intersection of the languages
$\mathcal L_1$ of all lists of even natural numbers, and $\mathcal
L_2$ of all trees with binary nodes labeled with $cons$, and whose
leaves are either $nil$ or natural numbers of the form $3n+2$,
$n\in\nat$.

We have already seen what an automaton recognizing $\mathcal L_1$
looked like, see Figure~\ref{fig:listeven}.  In TPTP format, this is
file \url{listeven.p}:

%BEGIN IMAGE
\lstinputlisting[language=tptp,frame=L]{listeven.p}
%END IMAGE
%HEVEA\imageflush

The language $\mathcal L_2$ is described by the predicate (final
state) \lstinline[language=tptp]{tree_3n_plus_2}.  Look at file \url{tree3plus2.p}:

%BEGIN IMAGE
\lstinputlisting[language=tptp,frame=L]{tree3plus2.p}
%END IMAGE
%HEVEA\imageflush

By the way, we can convert any automaton in TPTP format into Prolog
format by running {\tt h1} with the {\tt -no-trim} %
\index{indexN}{trim@{\tt -no-trim}}%
option: \verbatimtabinput{tree3plus2} Normally, {\tt h1}'s default is
to use the {\tt -trim} %
\index{indexN}{trim@{\tt -trim}}%
option, which trims away all clauses that are obviously not needed for
deriving a contradiction.  (See Section~\ref{sec:h1:options} for more
information on {\tt -trim} and {\tt -no-trim}.)  In this case,
trimming would just eliminate all clauses!  Since we are not looking
for a contradiction, we just run {\tt h1} without trimming, and get a
model in \url{tree3plus2.model.pl}:

%BEGIN IMAGE
\lstpl{tree3plus2.model.pl}
%END IMAGE
%HEVEA\imageflush

In other words, {\tt h1} can be used to convert any set of $\mathcal
H_1$ clauses into an equivalent alternating tree automaton by running
it
with the {\tt -no-trim} %
\index{indexN}{trim@{\tt -no-trim}}%
option and looking into the generated model file, ending in {\tt
  .model.pl}.



\subsubsection{\label{sec:h1:excompl:vis}Visualizing Tree Automata}


Before we compute the intersection of $\mathcal L_1$ and $\mathcal
L_2$, let us visualize the automaton defining $\mathcal L_2$.  This is
accomplished using {\tt pl2gastex}%
\index{indexN}{pl2gastex@{\tt pl2gastex}}%
, see Figure~\ref{fig:tree3plus2_model}.  For more information on {\tt
  pl2gastex}, and how to read such pictures precisely, see
Section~\ref{sec:autodot}.

\begin{figure}[htbp]
\caption{\label{fig:tree3plus2_model}Trees with leaves equal to $nil$ or to $3n+2$, $n\in \nat$}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt}
  \small
  \input{tree3plus2_model}
%END IMAGE
%HEVEA\imageflush
\end{center}
\end{figure}

\subsubsection{\label{sec:h1:excompl:inter}Computing Intersections of Tree Automata}

Now compute the intersection.  Build a file, say
\url{list_even_inter_tree3plus2.p}, by concatenating the clauses from
\url{listeven.p} and from \url{tree3plus2.p}, and add the so-called
{\em intersection\/} clause
\begin{eqnarray*}
  q (X) & \provided & \mathtt{list\_even} (X), \mathtt{tree\_3n\_plus\_2} (X)
\end{eqnarray*}
meaning that $q$ holds of all terms that are both lists of even
numbers, and trees as recognized at
\lstinline[language=tptp]{tree_3n_plus_2}.  Just run the following
commands: \verbatimtabinput{h1_inter} Because of the intersection
clause above, the resulting clause set is not an alternating tree
automaton as we have defined it.  However, run {\tt h1 -no-trim} %
\index{indexN}{trim@{\tt -no-trim}}%
on it:
\begin{verbatim}
h1 -no-trim list_even_inter_tree3plus2.p
\end{verbatim}
and look at the generated alternating tree automaton.  This is
obtained, as usual, in a file named
\url{list_even_inter_tree3plus2.model.pl}:

%BEGIN IMAGE
\lstpl{list_even_inter_tree3plus2.model.pl}
%END IMAGE
%HEVEA\imageflush

Graphically, this is the alternating tree automaton of
Figure~\ref{fig:interex}.

\begin{figure}[htbp]
  \caption{\label{fig:interex}Trees with leaves equal to $nil$ or to $3n+2$, which are lists of even natural numbers at the same time}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt}
  \small
  \input{list_even_inter_tree3plus2_model}
%END IMAGE
%HEVEA\imageflush
\end{center}  
\end{figure}

Note the presence of new nodes labeled $\land$ in
Figure~\ref{fig:interex}.  They represent intersections of languages.
Indeed, there are two ways one can construct an element of
$\mathtt{q}$.  First, there is $nil$.  Second, there are terms of the
form $cons$ applied to two arguments $X_1$ and $X_2$, where $X_1$ is
recognized {\em both\/} at \lstinline[language=tptp]{tree_3n_plus_2}
and at \lstinline[language=tptp]{even}, and $X_2$ is recognized {\em
  both\/} at \lstinline[language=tptp]{tree_3n_plus_2} and at
\lstinline[language=tptp]{list_even}.

The alternating tree automaton above recognizes (at $q$) the terms in
the intersection of $\mathcal L_1$ and $\mathcal L_2$.  One should
observe that computing intersections of two languages by concatenating
the clause sets defining each and adding an intersection clause is
rather cavalier.  It is only correct here because the two files
\url{listeven.p} and \url{tree3plus2.p} share no predicate symbol.
In general, one might allow shared predicate symbols, provided they
have the same semantics in each file.  For example, it is legal for
the two files to both use the predicate
\lstinline[language=tptp]{even} provided it denotes the set of even
natural numbers in both.  Otherwise, strange things may happen (an
over-approximation will be computed).

\subsubsection{\label{sec:h1:excompl:empty}Checking Tree Automata for Emptiness, Testing Membership}

It may not be completely obvious whether such an alternating tree
automaton is empty or not.  (To say the least.  The problem is
DEXPTIME-complete.)  Let us see whether the intersection state
\lstinline[language=tptp]{q} is empty or not.  In general, given a
satisfiable set $S$ of Horn clauses (e.g., definite clauses, in
particular alternating tree automata clauses), the language of terms
recognized at state $P$ in $S$ is empty if and only if $S$ plus the
clause $\bot \provided P (X)$ is satisfiable.  Running:
\index{indexN}{log@{\tt -log-out}}%
\verbatimtabinput{h1_inter2} %
yields \lstinputlisting[frame=l]{h1_inter2_err} meaning that there are
indeed terms recognized at state $q$ in the intersection.

We have kept a trace of the derivation in the log file
\url{list\_even\_inter\_tree3plus2.log}.  We can then use {\tt
  h1trace} %
\index{indexN}{h1trace@{\tt h1trace}}%
to get a mostly readable proof of the fact that $q$ is non-empty; in
particular, to have an example of a term recognized at $q$:
\verbatimtabinput{list_even_inter_tree3plus2.trace} In fact, the empty
list $nil$ is recognized at $q$ (\verb/{X1=nil}/ at line 4 above).
How to read such proofs will be explained in
Section~\ref{sec:h1trace}.

%!!! explain proof

Let us test membership of some ground term.  Is the list $cons (s (s
(o)), nil)$ consisting of just the natural number $2$ in the
intersection?  In general, given $S$ as above, a ground term $t$ is
recognized at state $P$ if and only if $S$ plus the clause $\bot
\provided P (t)$ is satisfiable.  \verbatimtabinput{h1_inter3} yields
\lstinputlisting[frame=l]{h1_inter3_err} So $cons (s (s (o)), nil)$ is
in the intersection.

On the other hand, the list $cons (s (s (s (s (o)))), nil)$ containing
just the natural number $4$ is {\em not\/} in the intersection.  Run
\verbatimtabinput{h1_inter4} and you'll get
\lstinputlisting[frame=l]{h1_inter4_err} (no message at all).  Indeed,
$cons (s (s (s (s (o)))), nil)$ is a list of even natural numbers, but
not a tree whose numeric leaves are of the form $3n+2$, $n\in \nat$.

We can do more this way.  Is there a term of the form $cons (s (X),
X)$, with the same $X$, in the intersection?  Run
\verbatimtabinput{h1_inter5} and you'll get
\lstinputlisting[frame=l]{h1_inter5_err} (no message at all).
So there is none.

Is there a list whose first element is at least $3$ in the
intersection?  Run \verbatimtabinput{h1_inter6} and you'll get
\lstinputlisting[frame=l]{h1_inter6_err} So there is one.  We don't
know which.  However, we may use {\tt h1trace} as above to have an
idea (left as an exercise!).

Another possibility to have an idea of which lists whose first element
is at least $3$ in the intersection is to build the automaton
recognizing all solutions, by running%
\index{indexN}{trim@{\tt -no-trim}}%
\verbatimtabinput{h1_inter7}%
The resulting automaton, in file \url{rinter.model.pl}, is:

%BEGIN IMAGE
\lstpl{rinter.model.pl}
%END IMAGE
%HEVEA\imageflush

And graphically, this is the automaton of Figure~\ref{fig:rinterex}.

\begin{figure}[htbp]
  \caption{\label{fig:rinterex}Lists starting with a number at least $3$ as recognized in state $q$ of Figure~\ref{fig:interex}}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt} \small \input{rinter_model}
%END IMAGE
%HEVEA\imageflush
\end{center}  
\end{figure}


\subsubsection{\label{sec:h1:excompl:nondet}Converting Alternating to Non-Deterministic Tree Automata}


All right, this starts being a tad intricate.  In general, alternating
tree automata are not that easy to read.  We may eliminate
intersection nodes $\land$, and get a {\em non-deterministic\/} tree
automaton instead by using the {\tt -no-alternation} %
\index{indexN}{alternation@{\tt -no-alternation}}%
option to {\tt h1}.  Either use
\index{indexN}{trim@{\tt -no-trim}}%
\index{indexN}{alternation@{\tt -no-alternation}}%
\begin{center}
  {\tt h1 -no-trim -no-alternation}  
\end{center}
instead of {\tt h1 -no-trim} (this will produce a non-deterministic,
i.e., not an alternating tree automaton, in \url{rinter.model.pl}), or
simply run
\index{indexN}{model@{\tt -model}}%
\begin{center}
  {\tt h1 -no-trim -model}
\end{center}
on \url{rinter.model.pl} to eliminate intersection nodes.  Just as
\begin{center}
  {\tt h1 -no-trim}
\end{center}
can be used to conv
ert an $\mathcal H_1$ clause set
into an equivalent alternating tree automaton,
\index{indexN}{trim@{\tt -no-trim}}%
\index{indexN}{alternation@{\tt -no-alternation}}%
\begin{center}
  {\tt h1 -no-trim -no-alternation}
\end{center}
converts an $\mathcal H_1$ clause set, or an alternating tree
automaton, into an equivalent non-deterministic tree automaton.  Run
\index{indexN}{pl2tptp@{\tt pl2tptp}}%
\index{indexN}{trim@{\tt -no-trim}}%
\index{indexN}{alternation@{\tt -no-alternation}}%
\verbatimtabinput{h1_inter8}%
This yields the following automaton in file \url{rinter_nd.model.pl}.

%BEGIN IMAGE
\lstpl{rinter_nd.model.pl}
%END IMAGE
%HEVEA\imageflush

Using {\tt pl2gastex} %
\index{indexN}{pl2gastex@{\tt pl2gastex}} on the output
\url{rinter_nd.model.pl}, we arrive at the non-deterministic tree
automaton of Figure~\ref{fig:rinter_ndex}.  This should be more
readable.  The final state is $\mathtt{q}$.  Note that the result
still contains two copies of the automata recognizing respectively all
lists of even numbers, and all trees with leaves of the form $nil$ or
$3n+2$, which are not needed any longer.

\begin{figure}[htbp]
  \caption{\label{fig:rinter_ndex}Eliminating intersection nodes from Figure~\ref{fig:rinterex}}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.55pt}
  \small
  \input{rinter_nd_model}
%END IMAGE
%HEVEA\imageflush
\end{center}  
\end{figure}

The automaton of Figure~\ref{fig:rinter_ndex}, i.e., in file
\url{rinter_nd.model.pl}, uses new states such as
\verb/__inter_even_and_one__mod__3/ (which recognizes all terms which
are both even numbers and numbers of the form $3n+1$).  In general,
these new states are named
\[
\verb/__inter_/P_1\verb/_/P_2\verb/_/\ldots\verb/_/P_n
\] and are meant to recognize all terms that are recognized
at $P_1$ and at $P_2$ and \ldots{} and at $P_n$ at the same time.  They
appear as $P_1 \cap P_2 \cap \ldots \cap P_n$ under {\tt pl2gastex}%
\index{indexN}{pl2gastex@{\tt pl2gastex}}%
.

\subsubsection{\label{sec:h1:excompl:purge}Purging Tree Automata}

Well, Figure~\ref{fig:rinter_ndex} should be more readable\ldots{} but
there is some junk here.  First, there are two sub-automata,
disconnected from the rest, defining the predicates \verb/zero_mod_3/,
\verb/one_mod_3/, \verb/two_mod_3/, \verb/tree_3n_plus_2/, and
\verb/odd/, \verb/even/, \verb/list_even/.  They do not contribute at
all to the definition of the language of \verb/r/.  Second, there are
also spurious states such as \verb/q/, or \verb/__aux_1/ (drawn as a
small state 
%BEGIN IMAGE
\begin{picture}(4,4)(0,0)
  \node[Nadjust=wh](block5)(3,1){$\scriptstyle\oldstylenums{1}$}
\end{picture}
%END IMAGE
%HEVEA\imageflush
or
%BEGIN IMAGE
\begin{picture}(4,4)(0,0)
  \node[Nadjust=wh](block5)(3,1){$\scriptstyle a$}
\end{picture}
%END IMAGE
%HEVEA\imageflush
).  Use {\tt plpurge} to purge the automaton of
Figure~\ref{fig:rinter_ndex} from all spurious states, by running
\index{indexN}{plpurge@{\tt plpurge}}%
\verbatimtabinput{h1_inter9}

\begin{figure}[htbp]
  \caption{\label{fig:rinter_nd_purgedex}Purging the automaton of Figure~\ref{fig:rinter_ndex}}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.55pt}
  \small
  \input{rinter_nd_purged}
%END IMAGE
%HEVEA\imageflush
\end{center}
\end{figure}

Hence we see that the relation $\mathtt{r}$ is simply the relation
relating all numbers that are both odd and equal to $2$ modulo $3$
(state $\mathtt{odd} \cap \mathtt{two\_mod\_3}$) to all objects that are
both lists of even numbers and trees of with leaves equal to $nil$ or
$3n+2$ (state $\mathtt{list\_even} \cap \mathtt{tree\_3n\_plus\_2}$).

Looking a bit more in depth, the numbers that are both odd and equal
to $2$ modulo $3$ are $5$, $11$, $17$, \ldots, in other words the numbers
that are equal to $5$ modulo $6$.  And the objects that are both lists
of even numbers and trees of with leaves equal to $nil$ or $3n+2$ are
just lists of numbers equal to $2$ modulo $6$.

\subsubsection{\label{sec:h1:excompl:det}Determinizing Tree Automata}

Looking at Figure~\ref{fig:rinter_nd_purgedex}, we realize that taking
the successor, i.e., applying the $\mathtt{s}$ function to a term
recognized at $\mathtt{odd} \cap \mathtt{one\_mod\_3}$, yields a term that
is recognized both at $\mathtt{even} \cap \mathtt{two\_mod\_3}$ and at
$\mathtt{even} \cap \mathtt{tree\_3n\_plus\_2}$.  This is a form of {\em
  non-determinism\/}: we may want to travel to either state, not
knowing which will eventually lead to acceptance.

To cater for this, we may {\em determinize\/} our tree automata.  This
produces an equivalent deterministic tree automaton, i.e., a set of
Horn clauses of the form
\begin{eqnarray}
  \label{eq:auto:det}
  P (f (X_1, \ldots, X_n)) & \provided & P_1 (X_1), \ldots, P_n (X_n)
\end{eqnarray}
where $X_1$, \ldots, $X_n$ are pairwise distinct variables, and where there
is {\em at most\/} one such clause for each $(n+1)$-tuple $(f, P_1, \ldots,
P_n)$.  The automaton of Figure~\ref{fig:rinter_nd_purgedex} is not
deterministic because it contains the two clauses

%BEGIN IMAGE
\lstpl{nondetex}
%END IMAGE
%HEVEA\imageflush

By definition, a deterministic tree automaton can also be seen as a
partial function $I_f$ from tuples of predicates to predicates, one
for each $f$.  I.e., $I_f (P_1, \ldots, P_n) = P$ if there is a,
necessarily unique, clause of the form (\ref{eq:auto:det}).

%!!! complete automata; models.

To determinize the automaton \url{rinter_nd.purged.pl} of
Figure~\ref{fig:rinter_nd_purgedex}, run%
\index{indexN}{pldet@{\tt pldet}}%
\verbatimtabinput{h1det} This produces a deterministic tree automaton
in file \url{rinter_d.xml}:

%BEGIN IMAGE
\lstxml{rinter_d.xml}
%END IMAGE
%HEVEA\imageflush

The format will be explained in more detail in Section~\ref{sec:pldet}.

We can then convert this deterministic tree automaton into Prolog
notation, since every deterministic tree automaton is a particular
case of a non-deterministic tree automaton (itself a particular case
of an alternating tree automaton).  Use {\tt auto2pl} %
\index{indexN}{auto2pl@{\tt auto2pl}}%
this way:
\verbatimtabinput{h1detpl}

This produces a file \url{rinter\_d.pl}, which is probably slightly
more readable than the XML file above:

%BEGIN IMAGE
\lstpl{rinter_d.pl}
%END IMAGE
%HEVEA\imageflush

Now draw the resulting automaton in Figure~\ref{fig:rinter_dex}, using
{\tt pl2gastex}%
\index{indexN}{pl2gastex@{\tt pl2gastex}}%
:
\verbatimtabinput{h1detg}

\begin{figure}[htbp]
  \caption{\label{fig:rinter_dex}Determinizing the automaton of Figure~\ref{fig:rinter_nd_purgedex}}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.55pt} \small \input{rinterd}
%END IMAGE
%HEVEA\imageflush
\end{center}
\end{figure}

The automaton of Figure~\ref{fig:rinter_dex} is not too big.  But
beware: determinizing tree automata may produce automata that are
exponentially larger in the general case.  In fact, {\tt pldet} may
just take forever on some alternating, or even non-deterministic tree
automata.


\subsubsection{\label{sec:h1:excompl:union}Computing Unions, Transitive Closures}

We have seen how to compute intersections of tree automata in
Section~\ref{sec:h1:excompl:inter}.  Computing unions is just as easy.
Say that you want to compute the union of the sets of lists of even
numbers (\url{listeven.p}) and of the trees whose leaves are $nil$ or
$3n+2$, $n\in \nat$.  That is, instead of computing the intersection of
the languages $\mathcal L_1$ and $\mathcal L_2$ introduced at the
beginning of Section~\ref{sec:h1:excompl}, we compute their union.  As
before, build a file, say \url{list_even_union_tree3plus2.p}, by
concatenating the clauses from \url{listeven.p} and from
\url{tree3plus2.p}, but this time add the two clauses
\begin{eqnarray*}
  q (X) & \provided & \mathtt{list\_even} (X) \\
  q (X) & \provided & \mathtt{tree\_3n\_plus\_2} (X)
\end{eqnarray*}
so that the fresh state $q$ recognizes the terms that are recognized
by either the state \lstinline[language=tptp]{list_even} or by
\lstinline[language=tptp]{tree_3n_plus_2}.  Concretely, run the
following commands: \verbatimtabinput{h1_union}
Now run {\tt h1 -no-trim} %
\index{indexN}{trim@{\tt -no-trim}}%
as above: \verbatimtabinput{h1_union2} We get an equivalent
alternating tree automaton in the file
\url{list_even_union_tree3plus2.model.pl}:

%BEGIN IMAGE
\lstpl{list_even_union_tree3plus2.model.pl}
%END IMAGE
%HEVEA\imageflush

Graphically, this is the alternating tree automaton of
Figure~\ref{fig:unionex}, again obtained using {\tt pl2gastex}.

\begin{figure}[htbp]
  \caption{\label{fig:unionex}Trees with leaves equal to $nil$ or to $3n+2$, or which are lists of even natural numbers}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt}
  \small
  \input{list_even_union_tree3plus2_model}
%END IMAGE
%HEVEA\imageflush
\end{center}  
\end{figure}

This can be determinized again.  Run {\tt pldet} %
\index{indexN}{pldet@{\tt pldet}}%
and {\tt auto2pl} %
\index{indexN}{auto2pl@{\tt auto2pl}}%
: \verbatimtabinput{h1detu} and you get

%BEGIN IMAGE
\lstpl{list_even_union_tree3plus2_d.pl}
%END IMAGE
%HEVEA\imageflush

As you may see, the determinized automaton is much larger this time,
and {\tt pl2gastex} now has real trouble trying to draw it.  (See
Figure~\ref{fig:union_dex}.)  We use {\tt twopi} as graph layout
engine here instead of {\tt neato} and run:
\index{indexN}{twopi@{\tt twopi}}%
\verbatimtabinput{pl2gdetu}

\begin{figure}[htbp]
  \caption{\label{fig:union_dex}Determinizing the automaton of Figure~\ref{fig:unionex}}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt}
  \small
  \input{list_even_union_tree3plus2_model_d}
%END IMAGE
%HEVEA\imageflush
\end{center}  
\end{figure}


The trick we have used to compute intersections and unions, namely
concatenating files and adding new clauses (provided the concatenated
files agree on the semantics of predicates), can also be used to
compute other combinations of tree languages.  A particularly
interesting one is the computation of {\em transitive closures\/} of
relations defined by tree automata (or, more generally, by $\mathcal
H_1$ clause sets).

For the purpose of illustration, imagine you want to compute the
transitive closure of the binary relation $\mathtt{r}$ defined in
\url{rinter_d.pl} (drawn in Figure~\ref{fig:rinter_dex},
Section~\ref{sec:h1:excompl:det}).  Just create a fresh binary
predicate symbol $\mathtt{r}^+$, and add the clauses
\begin{eqnarray*}
  \mathtt{r}^+ (X, Y) & \provided & \mathtt{r} (X, Y)\\
  \mathtt{r}^+ (X, Z) & \provided & \mathtt{r} (X, Y), \mathtt{r} (Y, Z)
\end{eqnarray*}
Concretely, run
\index{indexN}{pl2tptp@{\tt pl2tptp}}%
\verbatimtabinput{h1_tc}
Compute an equivalent non-deterministic tree automata by%
\index{indexN}{trim@{\tt -no-trim}}%
\index{indexN}{alternation@{\tt -no-alternation}}%
\verbatimtabinput{h1_tc2}
You get

%BEGIN IMAGE
\lstpl{rinter_d_plus.model.pl}
%END IMAGE
%HEVEA\imageflush

Since the clauses defining $\mathtt{r}^+$, i.e.,
\verb/r_plus/, are the same as those defining $\mathtt{r}$, the
transitive closure of $\mathtt{r}$ is $\mathtt{r}^+$ itself here:
$\mathtt{r}$ was already transitive.  (Exercise: why?)

\subsubsection{\label{sec:h1:excompl:neg}Complete Deterministic Tree Automata, Taking Complements}

We observed in Section~\ref{sec:h1:excompl:det} that a deterministic
tree automaton could be seen as a partial function $I_f$ from tuples
of predicates to predicates, one for each function symbol $f$.

A {\em complete deterministic\/} tree automaton is a set of Horn clauses of
the form (\ref{eq:auto:det}), i.e.,
\begin{eqnarray*}
  P (f (X_1, \ldots, X_n)) & \provided & P_1 (X_1), \ldots, P_n (X_n)
\end{eqnarray*}
where $X_1$, \ldots, $X_n$ are pairwise distinct variables, and where there
is {\em exactly\/} one such clause for each $(n+1)$-tuple $(f, P_1, \ldots,
P_n)$ (instad of {\em at most\/} one such clause for incomplete
automata).

Any deterministic tree automaton can be completed to a complete one,
by adding a {\em catch-all\/} state $\mathtt{\_\_all}$ %
\index{indexN}{all@{\tt \_\_all}}%
\index{indexN}{top@{\tt $\top$}|see{\tt \_\_all}}%
(shown as $\top$ by {\tt pl2gastex})%
\index{indexN}{pl2gastex@{\tt pl2gastex}}%
, to which all missing transitions are directed.  Precisely, if there
is an $(n+1)$-tuple $(f, P_1, \ldots, P_n)$ such that there is not clause
as above, then add the clause
\begin{eqnarray*}
  \mathtt{\_\_all} (f (X_1, \ldots, X_n)) & \provided & P_1 (X_1), \ldots, P_n (X_n)
\end{eqnarray*}
This must also be done whenever any one of $P_1$, \ldots, $P_n$ is the
catch-all state $\mathtt{\_\_all}$.

The function $I_f$ is then total.  The collection of all such $I_f$
defines a finite model, whose set of values is that of all predicates.
A value satisfies a predicate $P$ if and only if it is $P$, seen as a
value.

In fact, finite models and complete deterministic tree automata are
exactly the same notion.  You might want to ponder this.

As an example, let us return to the Dreadsbury mansion murder mystery
(Section~\ref{sec:h1:expb55}).  As we have seen, the only to have
possibly killed Aunt Agatha is Aunt Agatha herself.  We have proved
this by showing that the set of clauses in \url{butler-puzzle.p} (and
explained in Section~\ref{sec:h1:expb55}) with {\tt WHO} defined as
$agatha$ was satisfiable.

Since this set is satisfiable, it has a model.  Well, {\tt h1}
computes such a model, in the guise of an alternating tree automaton.
Run \verbatimtabinput{butler_model} and you'll get it in file
\url{agatha.model.pl} (see Figure~\ref{fig:agatha_model}):%
\index{indexN}{trim@{\tt -no-trim}}%

%BEGIN IMAGE
\lstpl{agatha.model.pl}
%END IMAGE
%HEVEA\imageflush

\begin{figure}[htbp]
\caption{\label{fig:agatha_model}Why Agatha killed herself}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt}
  \small
  \input{agatha_model}
%END IMAGE
%HEVEA\imageflush
\end{center}
\end{figure}

All right, this does not look like a model at all (much less an
explanation!), but remember there is a complete deterministic tree
automaton that is equivalent to it.  We know how to compute an
equivalent deterministic tree automaton, using {\tt pldet} %
\index{indexN}{pldet@{\tt pldet}}%
and {\tt auto2pl}%
\index{indexN}{auto2pl}%
, viz.
\verbatimtabinput{butler_model_det}
Using {\tt pl2gastex}%
\index{indexN}{pl2gastex@{\tt pl2gastex}}%
, as usual, produces a visual representation of it, see
Figure~\ref{fig:agathad};

\begin{figure}[htbp]
\caption{\label{fig:agathad}Why Agatha killed herself, deterministically}
\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.6pt}
  \small
  \input{agathad}
%END IMAGE
%HEVEA\imageflush
\end{center}
\end{figure}

So Agatha killed herself, Agatha is the only one not to be richer than
Agatha, Agatha hates herself and Charles, the butler hates Agatha and
Charles, and Charles hates noone.

Let us now produce the corresponding {\em complete\/} deterministic
tree automaton.  This can be done using {\tt auto2pl}%
\index{indexN}{auto2pl@{\tt auto2pl}}%
, which we have already seen, using the {\tt -complete 1} %
\index{indexN}{complete@{\tt -complete}}%
option.  Be warned, though, that complete deterministic tree automata
are large: with $n$ states (included the catch-all states), {\em
  any\/} function taking $k$ arguments will contribute $n^k$ clauses,
never less---and do not forget that any $k$-ary predicate symbol $P$
with $k\geq 2$ creates an invisible function symbol $f_P$, which will
contribute $n^k$ clauses as well.  Anyway, run
\index{indexN}{sort@{\tt sort}}%
\verbatimtabinput{butler_model_c} and you'll get the resulting
complete deterministic tree automaton in file \url{agatha_c.pl}.

%!!! talk about sort; gprolog.

%!!! complementation!
%!!! talk about reserved predicate names: __all, __not_, __aux_, __inter_, possibly #q<n>.

%!!!


%{\tt -no-resolve} option.  This
%disables any reasoning activity from {\tt h1}.  Using the {\tt -log-out}
%additionally will output the trace file to {\tt stdout}.  We can then
%feed this to {\tt h1getlog processed} to retrieve the set of clauses
%input to {\tt h1}, in Prolog notation.  That is, run
%\verbatimtabinput{tree3plus2} and you will get the desired clause set
%in Prolog notation in file \url{tree3plus2.pl}:
%\lstpl{tree3plus2.pl}

%This may seem contorted.  (If you want to use this trick often, make
%it a shell script!)  In fact, the above command line does something
%more general: it uses {\tt h1} to build an over-approximation of the
%original set of clauses, see Section~\ref{sec:h1:exns} for more
%information and examples.  Since \url{tree3plus2.p} is already a tree
%automaton, hence in $\mathcal H_1$, {\tt h1} does not need to compute
%any approximation, and will just output the original clause set.  (The
%use of {\tt sort} is not necessary, except if you want to feed it to
%Prolog, which prefers to have all clauses defining the same predicate
%grouped together.)


%!!! say that complementation is done through auto2pl instead.

%!!!
% give an example inside H1.
% say that the answers are exact here, and we can check this by calling -check-h1 1 or 2.

%!!! encode set constraints.

\subsection{\label{sec:h1:exns}The Needham-Schroeder Symmetric Key Protocol Example}


Try another example, \url{nspriv.p}, an encoding of the
Needham-Schroeder symmetric key protocol, together with three queries.
We do not mean that this is the only possible description of this
protocol, and only use this example as a motivation for using {\tt h1}
with more complex clause sets.
%  This is as follows:
%\lstinputlisting[language=tptp,frame=L]{../nspriv.p}

Here are the clauses of \url{nspriv.p}, in Prolog notation.  We have
shown the name of the clause on the left.  First, we define a
predicate $\knows$ that is meant to recognize all messages that a
malevolent intruder is able to build.  The first clauses say that
attackers can build any list of messages provided it knows each
message in the list, and conversely that it can build any message that
appears at any position in a list it knows:
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:intruder_knows_nil: & \knows (nil) && \\
  \lstinline[language=tptp]:intruder_can_take_first_components: & \knows (M_1) & \provided & \knows (cons (M_1, M_2)) \\
  \lstinline[language=tptp]:intruder_can_take_second_components: & \knows (M_2) & \provided & \knows (cons (M_1, M_2)) \\
  \lstinline[language=tptp]:intruder_can_build_pairs: & \knows (cons (M_1, M_2)) & \provided & \knows (M_1), \knows (M_2)
\end{array}
\]
Lists such as $[M_1, M_2, \ldots, M_n]$ are encoded, very classically,
as terms $cons (M_1, \allowbreak cons (M_2, \allowbreak \ldots
\allowbreak cons (M_n, \allowbreak nil) \ldots))$, whence the clauses
above.  Using a binary symbol $crypt$ to denote encryption, i.e.,
$crypt (M, K)$ denotes the result of encrypting $M$ using key $K$, we
may also write the following two important rules, stating that the
intruder can always encrypt any message it knows using any message it
knows, used as a key; and conversely, that the intruder can always
decrypt a message if he has the right key.
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:intruder_can_encrypt: & \knows (crypt (M, K)) & \provided & \knows (M), \knows (K) \\
  \multicolumn{2}{l}{\lstinline[language=tptp]:intruder_can_decrypt_if_has_private_key:} && \\
  & \knows (M) & \provided &
  \knows (crypt (M, key (pub, K))), \\
  &&& \knows (key (prv, K)) \\
  \multicolumn{2}{l}{\lstinline[language=tptp]:intruder_can_decrypt_if_has_public_key:} && \\
  & \knows (M) & \provided &
  \knows (crypt (M, key (prv, K))), \\
  &&& \knows (key (pub, K)) \\
  \multicolumn{2}{l}{\lstinline[language=tptp]:intruder_can_decrypt_if_has_symmetric_key:} && \\
  & \knows (M) & \provided &
  \knows (crypt (M, key (sym, X))), \\
  &&& \knows (key (sym, X))
\end{array}
\]
The last three clauses state how the intruder may decrypt a message of
the form $crypt (M, Z)$.  We assume that keys come into three
varieties, public keys of the form $key (pub, K)$ where $K$ is
typically the name of the agent holding this public key; private keys
of the form $key (prv, K)$ where $K$ is the name of the agent holding
this private key; and symmetric keys of the form $key (sym, X)$, where
$X$ is arbitrary.  The last three clauses state that you may decrypt a
message encrypted with a public key $key (pub, K)$ provided you know
the corresponding private key $key (prv, X)$; that you may decrypt a
message encrypted with a private key provided you know the
corresponding public key; and that you may decrypt a message encrypted
with a symmetric key provided you know the latter.

We also assume that there is an operation $s$ that builds a new
message $s (M)$ from an old $M$, in bijection with $M$; while we can
compute $s (M)$ from $M$ and recover $M$ from $s (M)$, the point is
that $M$ and $s (M)$ always differ.
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:intruder_can_compute_successors: &
  \knows (s (M)) & \provided & \knows (M) \\
  \lstinline[language=tptp]:intruder_can_compute_predecessors: &
  \knows (M) & \provided & \knows (s (M))
\end{array}
\]

In the Needham-Schroeder symmetric key protocol, Alice and Bob
communicate with a trusted server to get a common private key that
only they know, not the intruder.  Alice can always start a session of
the protocol and send the server a triple containing Alice's identity
$alice$, Bob's identity $bob$, and a nonce, that is, a fresh message
for this session.  Following \citet{Blanchet:Prolog}, we encode this
nonce as a function symbol applied to all parameters currently known,
say $noncea (alice, \allowbreak bob)$---the function symbol $noncea$
applied to Alice's identity $alice$ and Bob's identity $bob$.  Now we
assume a worst-case intruder model, where any communication can be
diverted by the intruder.  The net effect is that, from a security
viewpoint, what Alice does by sending a message consists exactly in
making it known to the intruder:
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:alice_sends_message_1_to_server: &
  \knows ( & cons ( & alice, \\
  && cons ( & bob, \\
  && cons ( & noncea (alice, bob), \\
  && & nil))))
\end{array}
\]
If the server ever receives such a message, i.e., a message of the
form $cons (A, \allowbreak cons (B, \allowbreak cons (Na, \allowbreak
nil)))$ for some arbitrary messages $A$, $B$, and $Na$ (the server has
no way of checking that Alice indeed sent the right message, and can
only check the message it receives contains three fields), then it
should send out (to Alice, but we have already seen this was
irrelevant from a security point of view) the message $crypt ([Na, B,
K_{ab}, crypt ([K_{ab}, A], K_{bs})], K_{as})$, where $K_{ab}$ is some
fresh key to be used by Alice and Bob, $K_{as}$ is a long-term key
shared between Alice and the server, and $K_{bs}$ is a long-term key
shared between Bob and the server.

Just like sending a message consists exactly in making it known to the
intruder, receiving a message is modeled by stating that the intruder
was able to build this message.  We shall therefore write a clause
saying that, if $\knows [A, B, Na]$ then $\knows\; crypt ([Na, B,
K_{ab}, \allowbreak crypt ([K_{ab}, A], \allowbreak K_{bs})],
\allowbreak K_{as})$.  Note that we are effectively saying that, from
the angle of security, the actions of the server amount to adding new
capabilities to the intruder: if the intruder knows a message matching
what the server expects, it can build the message that the server will
answer, even though it may not know the long-term keys $K_{as}$ and
$K_{bs}$.

Now we encode $K_{as}$ as the term $key (sym, cons (A, cons (server,
nil)))$, and $K_{bs}$ as the term $key (sym, cons (B, cons (server,
nil)))$; note that $A$ and $B$ are variables here, representing the
fact that the server will find these keys by looking up tables by the
identities of $A$, resp.\ $B$.  In current sessions, we encode
$K_{ab}$ by the term $key (sym, current\_session (A, B, Na))$.  The
key $K_{ab}$ as generated during older sessions is encoded by the term
$key (sym, old\_session (A, B, Na))$.  Separating current from old
sessions means we have to write two clauses:
\[
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:server_answers_A_with_encrypted_packet:}  \\
  & \knows (crypt ( & cons ( & Na, \\
  && cons ( & B, \\
  && cons ( & key (sym, current\_session (A, B, Na)), \\
  && cons ( & crypt (cons (key (sym, current\_session (A, B, Na)), \\
  && & \qquad \qquad cons (A, nil)), \\
  && & \qquad \qquad key (sym, cons (B, cons (server, nil)))), \\
  && & nil)))), \\
  && key ( & sym, cons (A, cons (server, nil))))) \\
  && & \qquad
  \quad\provided\quad \knows (cons (A, cons (B, cons (Na, nil)))) \\
  \multicolumn{4}{l}{\lstinline[language=tptp]:intruder_knows_previous_server_messages:}  \\
  & \knows (crypt ( & cons ( & Na, \\
  && cons ( & B, \\
  && cons ( & key (sym, old\_session (A, B, Na)), \\
  && cons ( & crypt (cons (key (sym, old\_session (A, B, Na)), \\
  && & \qquad \qquad cons (A, nil)), \\
  && & \qquad \qquad key (sym, cons (B, cons (server, nil)))), \\
  && & nil)))), \\
  && key ( & sym, cons (A, cons (server, nil))))) \\
  && & \qquad
  \quad\provided\quad \knows (cons (A, cons (B, cons (Na, nil))))
\end{array}
\]

All right, now, when Alice receives the message from the server, she
should send the part encrypted with $K_{bs}$ to Bob.  The idea is that
while Alice can decrypt the whole message, which is encrypted with
$K_{as}$, only Bob can decrypt the sub-message that is encrypted with
$K_{bs}$.  The message that Alice receives from the server should be
$crypt ([Na, B, K_{ab}, crypt ([K_{ab}, A], K_{bs})], K_{as})$,
however she can only check that it is of the form $crypt ([Na, B,
K_{ab}, Msg)$ for some sub-messages $K_{ab}$ and $Msg$ (which may be
totally unrelated to what the server actually sent).  She can however
check that $Na$ is the nonce $noncea (alice, bob)$ that she created
earlier (see above, clause
\lstinline[language=tptp]:alice_sends_message_1_to_server:), and that
$B$ really is Bob's identity $bob$.  So Alice expects a message of the
form $crypt ([noncea (alice, \allowbreak bob), \allowbreak bob,
\allowbreak K_{ab}, \allowbreak Msg], \allowbreak K_{as})$.  As we
have said before, for Alice to receive this message, the intruder must
send it to Alice, so the intruder must be able to build it.  Once
Alice receives this, it extract the sub-message $Msg$ and forwards it
to Bob---in fact adding it to the set of messages known to the
intruder:
\[
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:alice_gets_server_message_and_forwards_submessage_to_bob:} \\
  & \knows (Msg) & \provided\quad
  \knows (crypt ( & cons (noncea (alice, bob), \\
  &&& cons (bob, \\
  &&& cons (Kab, \\
  &&& cons (Msg, nil)))), \\
  &&& key (sym, cons (alice, cons (server, nil)))))
\end{array}
\]
We use an auxiliary predicate $\mathtt{alice\_key}$ meant to recognize
all possible values of $Kab$ above.  This is the key as seen by Alice.
%Note that we now check that the key, instead of being any key
%$K_{ab}$, is of the form $key (Mode, current\_session (X, Y, N)$.  In
%other words, we only record the keys as received in the current
%session, not older sessions, in $\mathtt{alice\_key}$.
\[
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:alice_gets_server_message_and_stores_current_session_key:} \\
  \qquad 
  & \multicolumn{3}{l}{\mathtt{alice\_key} (Kab)} \\
  && \provided\quad
  \knows (crypt ( & cons (noncea (alice, bob), \\
  &&& cons (bob, \\
  &&& cons (Kab, \\
  &&& cons (Msg, nil)))), \\
  &&& key (sym, cons (alice, cons (server, nil)))))
\end{array}
\]

Let's see what Bob does in this protocol.  First, Bob expects to
receive the sub-message $Msg$ above.  Cutting it short, Bob decrypts
it, gets $K_{ab}$, then sends a confirmation challenge $crypt (N_b,
K_{ab})$, where $N_b$ is a fresh nonce.  As before, $N_b$ is modeled
as a function symbol $nonceb$ applied to all relevant variables.
\[
\setlength\arraycolsep{2pt}
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge:} \\
  \quad & \knows (crypt (nonceb (Kab, A, B), Kab)
  & \provided &
  \knows (crypt (cons (Kab, cons (A, nil)), \\
  &&& \qquad\qquad\quad key (sym, cons (B, server, nil))))))
\end{array}
\]
On receiving this challenge, Alice tries to decrypt it with its own
version of the key $K_{ab}$, and sends back $N_b+1$:
\[
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:alice_answers_confirmation_challenge:} \\
  \qquad
  & \knows (crypt (s (Nb), Kab)) & \provided &
  \mathtt{alice\_key} (Kab), \knows (crypt (Nb, Kab))
\end{array}
\]
Bob then checks that it indeed gets the confirmation message above
with the right value for $Nb$.  If so, we store the key $Kab$ in the
predicate $\mathtt{bob\_key}$:
\[
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:agent_B_checks_confirmation_from_A:} \\
  \qquad
  & \mathtt{bob\_key} (Kab) & \provided &
  \knows (crypt (s (nonceb (Kab, A, B)), Kab))
\end{array}
\]
This terminates the description of the protocol.  Let us now describe
additional things the intruder know.  First, the intruder is assumed
to know the identities of all agents.  We also list who we think are
agents.  Note that the intruder itself is considered an agent, and has
its own identity $intruder$.
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:alice_is_an_agent: &
  \mathtt{agent} (alice) && \\
  \lstinline[language=tptp]:bob_is_an_agent: &
  \mathtt{agent} (bob) && \\
  \lstinline[language=tptp]:server_is_an_agent: &
  \mathtt{agent} (server) && \\
  \lstinline[language=tptp]:intruder_is_an_agent: &
  \mathtt{agent} (intruder) && \\
  \lstinline[language=tptp]:intruder_knows_all_agents: &
  \knows (X) & \provided & \mathtt{agent} (X)
\end{array}
\]
We also posit that the intruder knows all public keys (\ldots{}
because this is what we mean for them to be public!), and its own
private key.  We also assume that older sessions are so old that the
intruder eventually managed to crack all old sessions key.  This is
slightly pessimistic.  But it is precisely the purpose of changing
session keys to prevent intruders from gaining anything from cracking
old session keys.
\[
\begin{array}{lrcl}
  \lstinline[language=tptp]:intruder_knows_every_public_key: &
  \knows (key (pub, X)) && \\
  \lstinline[language=tptp]:intruder_knows_own_private_key: &
  \knows (key (prv, intruder)) && \\
  \lstinline[language=tptp]:intruder_knows_all_previous_session_keys: &
  \knows (key (sym, old\_session (A, B, Na))) &&
\end{array}
\]
This is all, at last.

Let us now ask a few queries.  The first asks whether the intruder may
know the key $K_{ab}$ as it was generated by the server.  The second
asks whether the intruder may know any key that Alice accepted as
being a key $K_{ab}$ at the end of the protocol.  The third asks
whether the intruder may know any key that Bob accepted as being
$K_{ab}$ at the end of the protocol.
\[
\begin{array}{lrcl}
  \multicolumn{4}{l}{\lstinline[language=tptp]:intruder_knows_session_key_generated_by_server:} \\
  \qquad &
  \bot & \provided &
  \knows (key (sym, current\_session (alice, bob, Na))) \\
  \multicolumn{4}{l}{\lstinline[language=tptp]:intruder_knows_session_key_as_seen_by_alice:} \\
  \qquad &
  \bot & \provided &
  \mathtt{alice\_key} (key (Mode, current\_session (X, Y, N))), \\
  &&& \knows (key (Mode, current\_session (X, Y, N))) \\
  \multicolumn{4}{l}{\lstinline[language=tptp]:intruder_knows_session_key_as_seen_by_B:} \\
  \qquad &
  \bot & \provided &
  \knows (crypt (s (nonceb (Kab, A, B)), Kab)), \knows (Kab)
\end{array}
\]

Now launch {\tt h1} on \url{nspriv.p}:
\begin{verbatim}
h1 nspriv.p
\end{verbatim}
You should get
\begin{lstlisting}[frame=l]{}
*** Derived: intruder_knows_session_key_as_seen_by_B ***
\end{lstlisting}
This means in short that {\tt h1} believes that this clause set is
unsatisfiable; in terms of protocols, that there is an attack.  You
cannot actually be sure that this is indeed an attack, i.e., that this
clause set is indeed unsatisfiable, because this clause set is not in
the $\mathcal H_1$ format.  (You should not conclude from this that
cryptographic protocols always produce clause sets outside $\mathcal
H_1$, see \citet{NNS:H1}.)

In this case, and contrarily to the example of
Section~\ref{sec:h1:expb55}, {\tt h1} computes an {\em
  approximation\/} of the input clause set $S$ as a clause set $S_1$,
and reasons on $S_1$ instead.  Check it using the {\tt -check-h1 2} %
\index{indexN}{check-h1@{\tt -check-h1}}%
option:
\begin{verbatim}
h1 -check-h1 2 nspriv.p
\end{verbatim}
and you'll get the list of all clauses in \url{nspriv.p} that are not
in $\mathcal H_1$:
\begin{lstlisting}[frame=l]{}
Warning: clause server_answers_A_with_encrypted_packet has
  non-linear head, variable A occurs repeatedly.
Warning: clause intruder_knows_previous_server_messages has
  non-linear head, variable A occurs repeatedly.
Warning: clause agent_B_gets_forwarded_submessage_and_\
                     \sends_confirmation_challenge
  has non-linear head, variable Kab occurs repeatedly.
Warning: clause alice_answers_confirmation_challenge has two
  non-sibling variables in the head that are connected
  in the body, Nb and Kab.
Stop.
\end{lstlisting}
Note also that {\tt h1} gives you an explanation of what's going
wrong.  For further explanation of what linear terms, sibling
variables and connected variables are, see \citet{NNS:H1} or
\citet{JGL:H1}.

The {\tt -check-h1 1} %
\index{indexN}{check-h1@{\tt -check-h1}}%
option runs the same checks.  However, it still proceeds with checking
the (un)satisfiability of the approximated clause set $S_1$, even when
the approximation is not exact, i.e., when the original clause set $S$
is not in $\mathcal H_1$.

The approximated clause set $S_1$ is always in the class $\mathcal
H_1$, and always implies $S$ logically.  In particular, if {\tt h1}
does not find any contradiction, i.e., if $S_1$ is satisfiable, then
$S$ is satisfiable, too.  In terms of cryptographic protocols, if {\tt
  h1} tells you that your protocol has no attack, then you can be sure
of it.  (That is, up to the accuracy of your model, written as
clauses.)

In our case, {\tt h1} found a purported attack, i.e., a purported
contradiction.  It turns out that \url{nspriv.p} is indeed
contradictory.  In fact, in most cases where {\tt h1} thinks a clause
set is contradictory, it is indeed contradictory.  (Although, as
usual, your mileage may vary.)

We terminate this example by mentioning the {\tt
  -all}\index{indexN}{all@{\tt -all}} option.

The answer
\begin{lstlisting}[frame=l]{}
*** Derived: intruder_knows_session_key_as_seen_by_B ***
\end{lstlisting}
above means that {\tt h1} found a (purported) contradiction first, and
second that, in order to derive the empty clause $\bot$, {\tt h1}
required the clause
\lstinline[language=tptp]:intruder_knows_session_key_as_seen_by_B:.
Is this the only query that fails?  Remember we have asked three
queries.  One way of checking this is to remove the
\lstinline[language=tptp]:intruder_knows_session_key_as_seen_by_B:
clause from \url{nspriv.p} and run {\tt h1} again.  There is a simpler
option: run {\tt h1} with the {\tt -all} %
\index{indexN}{all@{\tt -all}}%
option.  Once a contradiction has been found, instead of stopping just
like any other prover, {\tt h1 -all} will continue, trying to find
contradictions using other queries.

On the example, running
\begin{verbatim}
h1 -all nspriv.p
\end{verbatim}
you will get the same answer as above:
\begin{lstlisting}[frame=l]{}
*** Derived: intruder_knows_session_key_as_seen_by_B ***
\end{lstlisting}
In other words, no other query fails.  In terms of security, this
means that while Bob's key $K_{ab}$ is not secure, those of Alice and
the server definitely are.  This may seem paradoxical, however the
attack that {\tt h1} just found is one where the intruder deceives Bob
into accepted an old, cracked key from an older session.  This key is
not the key that the server produced.  It is also old, meaning that it
will be detected as not being new by Alice's use of the nonce $N_a$.

We have just proved that Alice and the server were in fact safe in
this protocol, while Bob is not.

%!!! say that most options have +option/-option formats.

The {\tt -no-resolve} %
\index{indexN}{resolve@{\tt -no-resolve}}%
option can be used to disable the reasoning facilities of {\tt h1}
altogether.  Then {\tt h1 -no-resolve} will just compute an
approximation of the input clause set, and store it into the log file.
For example,
\index{indexN}{resolve@{\tt -no-resolve}}
\begin{verbatim}
h1 -no-resolve nspriv.p
\end{verbatim}
runs without any output, and creates the log file \url{nspriv.log.gz}.
As we have already said, it is not really instructive to look at this
file directly.
% with {\tt zcat}.
However, you can extract from it the approximated clause set by
running:
% \begin{verbatim}
% zcat nspriv.log.gz | h1getlog processed | pl2tptp -
% \end{verbatim}
\begin{verbatim}
h1getlog processed nspriv.log | pl2tptp -
\end{verbatim}
This will output the approximated clause set on {\tt stdout}: {\tt
  h1getlog} with the {\tt processed} option will extract the
approximate clauses and print them in Prolog format.  Then {\tt
  pl2tptp} with the {\tt -} argument (meaning {\tt stdin}) will convert
these from Prolog format to TPTP format.

All this can be done in a simpler way, by using the {\tt
  -log-out} %
\index{indexN}{log@{\tt -log-out}}%
option to {\tt h1}.  Then {\tt h1} will output its log file
%, uncompressed,
to {\tt stdout}.  You can then pipe it to {\tt h1getlog} and {\tt
  pl2tptp}, as follows.  \index{indexN}{resolve@{\tt -no-resolve}}
\begin{verbatim}
h1 -log-out -no-resolve nspriv.p | h1getlog processed | pl2tptp -
\end{verbatim}

%!!! describe how to get just the abstraction... does not work: the gzip -c subprocess of h1 does not terminate before zcat is launched. Arg.

%test1.model.pl

% abstraction process.


\section{\label{sec:h1}The {\tt h1} Prover}

Most of the features of {\tt h1} are explained in
Section~\ref{sec:examples}.  We explain the structure of the {\tt h1}
command line in Section~\ref{sec:h1:options}, then turn to the
theoretical basis of {\tt h1} in Section~\ref{sec:h1:theory}.  We
refine this description in Section~\ref{sec:h1:op}, by stating the
precise rules used by {\tt h1}.

\subsection{\label{sec:h1:options}How to Use {\tt h1}}


The {\tt h1} tool recognizes the following options.  As in all Unix
tools, options start with a minus sign {\tt -}.  Some options are
flags, which can be toggled between an active state and a deactivated
state.  In this case, the convention used in {\tt h1} and other tools
of the {\tt h1} suite is to have {\tt -}$\langle$option$\rangle$
activate the option, while {\tt -no-}$\langle$option$\rangle$
deactivates it.

The options recognized by the {\tt h1} prover are:
\begin{itemize}
\item\aname{it_h1_h}{\tt -h}\index{indexN}{h@{\tt -h}|bold} %
  prints help.  This is basically a terse summary of the current
  explanation.
\item\aname{it_h1_v}{{\tt -v}$\langle n\rangle$}\index{indexN}{v@{\tt -v}|bold} %
  (with no space between {\tt -v} and $\langle n\rangle$) sets the verbosity level
  to the integer $n$.  Also, {\tt -v} sets the verbosity level to $1$.
  The default is $0$ (run silently).
  
  While other tools of the {\tt h1} suite understand verbosity as a
  way of printing more or less comments on {\tt stderr}, the {\tt h1}
  prover itself prints these comments into the log file.  That is,
  into $\langle$filename$\rangle${\tt.log.gz} if run as {\tt $\langle$filename$\rangle$}, into
  \url{h1out.log.gz} if run without a file, i.e., as {\tt h1 -}, and
  on {\tt stdout} if the {\tt -log-out} %
  \index{indexN}{log@{\tt -log-out}}%
  option is activated.
  
  This can be useful to examine how {\tt h1} proceeds to derive new
  clauses and to remove redundant clauses while it is reasoning.
  
  At verbosity level $1$, i.e., with {\tt -v1} or {\tt -v}, {\tt h1}
  adds comments of the form {\tt \% |-} $\langle$clause$\rangle$ to say which
  clauses are being derived, and added to the queue of clauses waiting
  to be processed.  Normally, {\tt h1} only lists clauses it is
  currently processing.  At verbosity level $1$, {\tt h1} also signals
  which clauses are useless, in the sense that a simple reachability
  test on predicate symbols showed that they could not participate in
  any derivation of the empty clause.
  
  At verbosity level $2$, i.e., with {\tt -v2}, {\tt h1} also gives
  information on its strategy for selecting clauses to be processed,
  lists the clauses it removes, because they are redundant in some or
  the other way.
  
  In any case, run {\tt h1 -v1 nspriv.p} or {\tt h1 -v2 nspriv.p},
  followed by the command %{\tt zcat nspriv.log.gz | less}
  {\tt less nspriv.log} to see
  concrete examples of such comments.
  
  The {\tt -v} options are only active if some log file is output at
  all, that is, if {\tt -log} %
  \index{indexN}{log@{\tt -log}}%
  or {\tt -log-out} %
  \index{indexN}{log@{\tt -log-out}}%
  is in effect.  (By default, {\tt -log} is active.)
\item\aname{it_h1_check-h1}{{\tt -check-h1} $\langle n\rangle$} %
  \index{indexN}{check-h1@{\tt -check-h1}|bold}%
  enables or disables $\mathcal H_1$ format checking.  If $n=0$, no
  check is done at all (default).  Clauses outside $\mathcal H_1$ are
  approximated as in Section~\ref{sec:h1:exns}, using a slightly more
  clever variant of the approximation algorithm of \citet{JGL:H1}.  If
  $n=1$, warnings are printed as to which clauses are not in $\mathcal
  H_1$, and what the problem is, then {\tt h1} proceeds approximating
  all clauses.  If $n=2$, the same warnings are printed; however, if
  any warning has been emitted, then {\tt h1} will stop and refuse to
  solve the given clause set.
\item\aname{it_h1_all}{{\tt -first}, {\tt -all}}%
  \index{indexN}{first@{\tt -first}|bold}%
  \index{indexN}{all@{\tt -all}|bold}%
  : by default, {\tt h1} works as any prover, and stops on finding the
  first contradiction ({\tt -first}).  With the {\tt -all} option,
  {\tt h1} will report all goal clauses through which a contradiction
  can be found.  See Section~\ref{sec:h1:exns} for an example.
  
  The way {\tt h1} does it is by replacing every goal clause $\bot
  \provided P_1 (t_1), \ldots, P_n (t_n)$, of name $\langle$name$\rangle$, by a
  definite clause $q_{\langle\mathrm{name}\rangle} \provided P_1 (t_1), \ldots, P_n
  (t_n)$ for a special nullary predicate symbol $q_{\langle\mathrm{name}\rangle}$,
  called a {\em signalling symbol}.  With the {\tt -first} option, as
  soon as {\tt h1} derives a signalling symbol, it prints its name
  inside \verb/*** Derived:/ and \verb/***/ and stops.  With the {\tt
    -all} option, {\tt h1} prints the names of all signalling symbols
  that can be derived.
\item\aname{it_h1_log}{{\tt -log}, {\tt -log-out}, {\tt -no-log}}%
  \index{indexN}{log@{\tt -log}|bold}%
  \index{indexN}{log@{\tt -no-log}|bold}%
  \index{indexN}{log@{\tt -log-out}|bold}%
  : by defaut, {\tt h1} outputs a trace of what it is doing into a log
  file ({\tt -log}).  If {\tt h1} was called on file
  $\langle$filename$\rangle${\tt .p}, then the trace will be in
  %$\langle$filename$\rangle${\tt.log.gz}
  $\langle$filename$\rangle${\tt.log}.  If {\tt h1} was given {\tt -}
  as input file (i.e., if {\tt h1} reads from standard input), then
  this file will be %\url{h1out.log.gz}.
  \url{h1out.log}.  If {\tt -log-out} is given instead of {\tt -log},
  this trace is output %, uncompressed,
  on {\tt stdout}.  If {\tt -no-log} is given, then no trace is
  produced at all.

  It may be that the log file is too big.  On several versions of the
  Linux operating system, trying to produce a log file of more than 2
  Gb will fail badly.
%   The reason why the trace is compressed by default is because it may
%   be huge.  So huge in fact that I've seen cases where it went above
%   the 2 Gb file size limit on Unix files.
  To see a rather extreme
  example, run
\begin{verbatim}
memtime h1 -progress Fabrice/alice_full1.p
\end{verbatim}
  \index{indexN}{progress@{\tt -progress}}%
  This is a 459 clause example, generated automatically from the
  static analysis by an early and faulty version of the Csur static
  analyzer \citep{GLP:VMCAI} of a small C implementation of the
  Needham-Schroeder public-key protocol ({\em not\/} the same as the
  symmetric-key protocol of Section~\ref{sec:h1:exns}).  Beware that
  this will take quite some time, and some disk space!  On the machine
  I'm using to write this text (an 1.4 Ghz Pentium IV class machine
  running RedHat Linux .6.9-1.6\_FC2), it takes 33 minutes, and 264 Mb
  main memory.
%memtime:
%1953.96 user, 12.26 system, 2207.45 elapsed -- Max VSize = 270064KB, Max RSS = 268836KB

  However, you risk having the following output instead:
\begin{verbatim}
Killed [25]
1372.43 user, 12.62 system, 1414.11 elapsed -- Max VSize = 240624KB, Max RSS = 239348KB
\end{verbatim}
  This is what happens when the log file exceeds its maximum allowed
  size.  To avert this, run:
\begin{verbatim}
memtime h1 -progress -log-out Fabrice/alice_full1.p >alice_full1.log
\end{verbatim}
  This outputs the log file to {\tt stdout}; then the Unix shell knows
  how to record this in a file almost as large as you wish.

  \url{Fabrice/alice\_full1.p} is the largest example we can deal
  with.  Note however that the time and space used by {\tt h1} are
  more related to the structure than to the size of the input problem;
  e.g., \url{Fabrice/alice\_full3.p} is about the same size (458
  clauses) and apparently very similar, but is shown satisfiable in a
  matter of seconds by {\tt h1}.
  
  You may want to run
\begin{verbatim}
watch h1mon h1.pgr
\end{verbatim}
\index{indexN}{watch@{\tt watch}}%
\index{indexN}{h1mon@{\tt h1mon}}%
\index{indexN}{h1.pgr@{\tt h1.pgr}}%
in parallel, to see how {\tt h1} progresses on
\url{Fabrice/alice\_full1.p}.  (See Section~\ref{sec:h1:op}.)
%Derived clauses: 871600 (51111 splitting defs, 673 ne facts)
%Dealt with, not subsumed: 273374
%Subsumed clauses [forward] : 598212 (of which 569595 automata clauses)
%Subsumed clauses [backward]: 16794 (of which 16204 automata clauses)
%Frozen clauses: 1458118, awaken: 9811.
%Fully defined predicate symbols: 507
%  Backward subsumed clauses because of fully defined symbols: 0
%  Subsumed parent clauses because of fully defined symbols: 109804
%Abbreviations: 1273
%Ground facts: 0
%Pruned clauses: 0
%Automata clauses: 90115
  
  To cut it short, \url{Fabrice/alice\_full1.p} will be detected as
  (possibly) unsatisfiable by {\tt h1}, and will generate the
  %compressed
  log file \url{Fabrice/alice\_full1.log}.  This is 2.73 Gb large.
  Early versions of {\tt h1} instead compressed the log file on the
  file using {\tt gzip}, resulting in a log file of only 94.5 Mb.
  However, this resulted in strange asynchrony-related bugs that
  affected the overall behavior of the {\tt h1} tool suite.
%   This is not much compared to the uncompressed file, which is a bit
%   more than 40 million lines long, and $2.67$ Gb long.  These figures
%   are obtained by running
% \begin{verbatim}
% zcat Fabrice/alice_full1.log.gz | wc -c -l
% \end{verbatim}
% \index{indexN}{zcat@{\tt zcat}}
%   which itself runs in about 20 s.
  
\item\aname{it_h1_model}{{\tt -model}, {\tt -no-model}}%
  \index{indexN}{model@{\tt -model}|bold}%
  \index{indexN}{model@{\tt -no-model}|bold}%
  : by default, {\tt h1} outputs a candidate model of the input clause
  set, as a set of Horn clauses, into file
  $\langle$filename$\rangle${\tt.model.pl}, if {\tt h1} was called on file
  $\langle$filename$\rangle$.p, or into \url{h1out.model.pl} if {\tt h1} expects
  its input from standard input.
  
  The {\tt h1} prover is {\em always\/} able to output a candidate
  model, even if the input clause set is unsatisfiable, and therefore
  has no model.  It is just that, in this case, the candidate model is
  no model: {\tt h1mc} will then complain, and state which clauses are
  not satisfied in the candidate model.  See Section~\ref{sec:h1mc}.
  
  To understand what this candidate model may be, especially in the
  case where there is no model, see Section~\ref{sec:h1:theory}: the
  candidate model is just the subset of all alternating automaton
  clauses, and universal clauses of the final, saturated clause set
  that {\tt h1} eventually computes.
  
\item\aname{it_h1_progress}{{\tt -progress}, {\tt -no-progress}}%
  \index{indexN}{progress@{\tt -progress}|bold}%
  \index{indexN}{progress@{\tt -no-progress}|bold}%
  : by default, this is deactivated ({\tt -no-progress}).  If
  activated with {\tt -progress}, a kludge is enabled that allows one
  to monitor {\tt h1}'s progress: a special file {\tt h1.pgr} is
  created and written into as {\tt h1} goes forward.  Each time {\tt
    h1} adds a clause, subsumes a clause, or does anything of the
  kind, it adds a conventional character to {\tt h1.pgr}.  Using {\tt
    h1mon h1.pgr} at any time while {\tt h1} is running will give you
  instantaneous statistics about how many operations {\tt h1} has
  performed until now.  See Section~\ref{sec:h1:op} for more
  explanations.  Using {\tt watch} in combination with {\tt h1mon}, as
  in {\tt watch h1mon h1.pgr}, is particularly useful here.%
  \index{indexN}{watch@{\tt watch}}%
  \index{indexN}{h1mon@{\tt h1mon}}%
  \index{indexN}{h1.pgr@{\tt h1.pgr}}
  
\item\aname{it_h1_resolve}{{\tt -resolve}, {\tt -no-resolve}}%
  \index{indexN}{resolve@{\tt -resolve}|bold}%
  \index{indexN}{resolve@{\tt -no-resolve}}%
  .  By default ({\tt -resolve}), {\tt h1} computes an $\mathcal H_1$
  approximation of the given clause set, then saturates the latter by
  a form of resolution.  The {\tt -no-resolve} disables the resolution
  engine, so that {\tt h1 -no-resolve} merely produces the $\mathcal
  H_1$ approximation into the log file (see \ahrefloc{it_h1_log}{{\tt
      -log}} option).  This is useful to just see what the
  approximated clauses actually are.  To actually see these clauses,
  run {\tt h1getlog processed} on the log file.  See \ref{sec:h1:exns}
  for an example.
  
\item\aname{it_h1_trim}{{\tt -trim}, {\tt -no-trim}}%
  \index{indexN}{trim@{\tt -trim}|bold}%
  \index{indexN}{trim@{\tt -no-trim}|bold}%
  .  By default ({\tt -trim}), {\tt h1} does a quick preprocessing
  phase ({\em trimming\/}) to eliminate some clauses that are
  obviously not needed to derive a contradiction.  This is based on
  following dependencies between predicate symbols.  E.g., if $P (t)
  \provided P_1 (t_1), \allowbreak \ldots, \allowbreak P_n (t_n)$ is an
  input clause, we say that $P$ depends on $P_1$, \ldots, $P_n$.  A
  predicate symbol $P$ is needed if and only if there is a goal clause
  of the form $\bot \provided \ldots, P (t), \ldots$, or if some needed predicate
  symbol depends on $P$, inductively.  By default, {\tt h1} removes
  all clauses headed by unneeded predicate symbols.
  
  This is useful to avoid {\tt h1} being clogged by useless clauses.
  Consider any set of definite clauses (i.e., without any goal
  clause).  While this set of clauses is (obviously!) satisfiable,
  {\tt h1} may lose quite some time saturating it by resolution.
  Trimming will just eliminate all clauses, and {\tt h1} will conclude
  right away that the set of clauses is (obviously, indeed)
  satisfiable.
  
  This may seem an extreme example.  However, this is also an example
  of why disabling trimming might be the desired option instead.  If
  you use {\tt h1} as a tree automaton tool, as in
  Section~\ref{sec:h1:excompl}, you will probably want precisely to
  feed {\tt h1} with just definite clauses, no goal clause, and expect
  {\tt h1} to output some compiled alternating tree automaton
  computing the same languages.  To obtain this result, use {\tt
    -no-trim}%
  \index{indexN}{trim@{\tt -no-trim}}%
  .
  
\item\aname{it_h1_path-refine}{{\tt -path-refine} $\langle n\rangle$}%
  \index{indexN}{path-refine@{\tt -path-refine}|bold}%
  .  Another trick that {\tt h1} uses to speed resolution up is to
  precompute a rather crude over-approximation of the least Herbrand
  model of the input clause set.  See Section~\ref{sec:h1:theory}.
  This consists essentially in computing the sets of paths through
  atoms in the least Herbrand model, truncated to some fixed length.
  The {\tt -path-refine} option allows one to specify what the cutoff
  length should be.  By default, it is $3$.
  
\item\aname{it_h1_alternation}{{\tt -alternation}, {\tt -no-alternation}}%
  \index{indexN}{alternation@{\tt -alternation}|bold}%
  \index{indexN}{alternation@{\tt -no-alternation}|bold}%
  .  By default ({\tt -alternation}), {\tt h1} produces an alternating
  tree automaton as model in the model file (see \ahrefloc{it_h1_model}{{\tt
      -model}} option%
  \index{indexN}{model@{\tt -model}}%
  ).  With the {\tt -no-alternation} option, {\tt h1} produces a
  non-deterministic tree automaton.  This is in general bigger than
  the corresponding alternating tree automaton, so that {\tt h1} may
  take more time saturating clauses with the {\tt -alternation}
  option.  See Section~\ref{sec:h1:excompl:nondet}.

\item\aname{it_h1_no-deep-abbrv}{{\tt -deep-abbrv}, {\tt -no-deep-abbrv}}%
  \index{indexN}{deep-abbrv@{\tt -deep-abbrv}|bold}%
  \index{indexN}{deep-abbrv@{\tt -no-deep-abbrv}|bold}%
  .  By default ({\tt -deep-abbrv}), {\tt h1} uses a rule called {\em
    abbreviation of deep terms\/}, which accelerates resolution,
  sometimes spectacularly.  This rule has the following effect.  Given
  some clause $H \Leftarrow P_1 (t_1), \ldots, P_n (t_n)$ such that, say, $t_i$ is
  {\em deep\/}, i.e., $t_i$ is neither a variable nor a function
  applied to variables.  Then list the free variables of $t_i$, say
  $X_1$, \ldots, $X_k$, create a fresh predicate symbol $Q$, and replace
  the above clause by
  \begin{eqnarray*}
    H & \Leftarrow & P_1 (t_1), \ldots, P_{i-1} (t_{i-1}), Q (X_1, \ldots, X_k), P_{i+1} (t_{i+1}), \ldots, P_n (t_n) \\
    Q (X_1, \ldots, X_k) & \Leftarrow & P_i (t_i)
  \end{eqnarray*}
  In fact, $Q$ needs not be fresh: if we apply the same rule on the
  same $P_i$ and the same $t_i$, we generate the same $Q$.  Using {\tt
    -no-deep-abbrv} disables this rule.  The only use we know of
  disabling it is measuring how much proof search is sped up by the
  deep abbreviation rule.

\item\aname{it_h1_no-sort-simplify}{{\tt -sort-simplify}, {\tt -no-sort-simplify}}%
  \index{indexN}{sort-simplify@{\tt -sort-simplify}|bold}%
  \index{indexN}{sort-simplify@{\tt -no-sort-simplify}|bold}%
  .  By default ({\tt -sort-simplify}), {\tt h1} uses a rule called
  {\em sort simplification\/}, which originates from the SPASS prover.
  This is moderately useful in general, but does not seem to be really
  costly.  The idea is as follows.  Assume the current set of clauses
  is $S$.  Amongst these, let $S_a$ be the set of alternating automata
  clauses.  These can be seen as {\em sort declarations\/}.  E.g., the
  alternating automaton clause $P (f (X_1, X_2, X_3)) \Leftarrow P_1 (X_1), P_2
  (X_1), P_3 (X_2)$ can be read as a rule stating that, if $X_1$ has
  sort $P_1$ and also sort $P_2$, if $X_2$ has sort $P_3$, and even if
  $X_3$ has no sort, then $f (X_1, X_2, X_3)$ has sort $P$.  Given any
  clause $H \Leftarrow P_1 (t_1), \ldots, P_n (t_n)$, extract a {\em sort
    environment\/} $\rho$: for each $i$ such that $t_i$ is a variable
  $X$, $\rho$ states that $X$ has sort $P_i$.  Then, for any $j$ such
  that $t_j$ is not a variable, if we can deduce that $t_j$ has sort
  $P_j$ using the sort environment $\rho$ and the current sort
  declarations, then remove $P_j (t_j)$ from the clause.  In
  principle, this is just a form of resolution, coupled with backward
  subsumption of the parent clause.  However, this variant takes
  polynomial time, while simulating this by ordinary resolution can
  take exponential time in the worst case.

\item\aname{it_h1_monadic-proxy}{{\tt -monadic-proxy}, {\tt -standard-approx}}%
  \index{indexN}{monadic-proxy@{\tt -monadic-proxy}|bold}%
  \index{indexN}{standard-approx@{\tt -standard-approx}|bold}%
  .  By default ({\tt -standard-approx}), the approximation {\tt h1}
  uses (see Section~\ref{sec:h1:exns}) is a slight refinement of that
  of \citet{JGL:H1}.  This keeps more information, i.e., it is more
  precise in general, than the probably more intuitive approximation
  of \citet{FSVY:Prolog:types=programs}, which tries to capture the
  so-called types of variables in each input clause.  The {\tt
    -monadic-proxy} option forces {\tt h1} to use the latter, less
  precise approximation.  The idea is that, by using a less precise
  approximation, {\tt h1} could run faster.  Experience until now has
  shown, on the contrary, that the less precise approximation is also
  slower: {\tt h1} generates many spurious clauses that just could not
  be generated with the more precise approximation.
  
  In other words, {\tt -monadic-proxy} is a false good idea.  This
  option is therefore obsolescent.
  
\item\aname{it_h1_body-chop}{{\tt -body-chop} $\langle n\rangle$}%
  \index{indexN}{body-chop@{\tt -body-chop}|bold}%
  .  Yet another false good idea.  Forces {\tt h1} to keep only at
  most $n$ atoms of depth at least $1$ in bodies of clauses generated
  by resolution.  In other words, if {\tt h1} ever tries to generate a
  clause with $m > n$ atoms of depth at least $1$, i.e., of the form
  $P (f (t_1, \ldots, t_k))$, it will savagely remove $m-n$ of them.
  Resolution then becomes unsound, but will remain complete.  That is,
  if {\tt h1} concludes that the input clause set is satisfiable, it
  will still be right in saying so.  It seems that this in fact does
  not speed things up at all.  This option is therefore obsolescent.
\end{itemize}


\subsection{\label{sec:h1:theory}Theoretical Background}


The essentials of the algorithmic underpinnings of {\tt h1} are
described, rather tersely, in \citet{JGL:H1}: {\tt h1} implements a
form of ordered resolution with selection

% ordered resolution with selection, splittingless splitting.
% subsumption, and the restricted forms used in h1.
% useful predicates (SCCs), and why this is disabled with the -no-trim option.
% path sets, or approximating the least Herbrand model.
% fully defined predicate symbols, and the removal of parent clauses defining
% them.
% introduction of #q predicates and functions, deep splits.

% say that model, as alternating automaton, is subset of alternating automaton clauses.

\subsection{\label{sec:h1:op}Principle of Operation}


% state main loop, in the style of SPASS doc (see clause.ml)
% also list all rules.

% as a prover
% as a model generator
% as a converter from H1 clauses to tree automata
% as an abstraction engine
% technical details:
% P(x,y) means P(f(x,y))

% describe h1mon, and explain the meaning of all fields.  This requires explaining the algorithm.

\section{\label{sec:h1trace}Explaining and Checking Proofs: {\tt h1trace}, {\tt h1logstrip}}


% In case the proof is wrong (abstraction is inexact), h1 trace will do its
% best to explain it to humans (in -tree format); in -coq format, proof
% checking may fail in Coq.

% explain Emacs' outline-mode.

% explain how this works?


\section{\label{sec:h1mc}Model-Checking Clause Sets and Explaining the Absence of Proofs with
  {\tt h1mc}}


%\subsection{The Purpose of {\tt h1mc}}

% provide a proof certificate that is independently checkable by Coq
% verify that h1 did not have a bug in failing to find a proof.

% why does it take a trace log and not a tptp file as second argument?
% how do you use it on a tptp file?  (there is a format problem, since
% h1getlog source will give you something in pseudo-XML/Prolog format, arg)

% what happens if h1mc is run on a non-model?  as happens with models generated by h1 on unsatisfiable clause sets.  It will just satisfy most clauses, but not all, and say which are not satisfied.

\subsection{\label{sec:h1mc:theory}Theoretical Background}


% explain algorithm
% together with equivalent Coq principles.

\section{\label{sec:pldet}Determinizing Tree Automata with {\tt pldet}}


%!!! Explain XML format.

%!!! Note: pldet ignores states of the form #q..., which are reserved for
%speeding computation in h1;

%!!! Note: pldet also does not generate transition for function symbols
%starting with '#'.  This occurs with n-ary predicates such as __aux_23
%(X,Y,Z), which is actually understood as __aux_23 (#__aux_23 (X,Y,Z)).  As
%for #q predicates, these are just auxiliaries that speed up h1.  They tended
%to make pldet horribly slow, too.

\section{\label{sec:auto2pl}Converting XML Deterministic Tree Automata to Prolog Notation with
  {\tt auto2pl}}


%!!! can also be used to compute complements of languages.

\section{\label{sec:plpurge}Cleaning and Extracting Automata with {\tt plpurge}}

\section{\label{sec:pl2tptp}Converting Tree Automata and Prolog Programs to TPTP
  Files}



\section{\label{sec:tptpmorph}Applying Morphisms to $\mathcal H_1$ Clause Sets with {\tt tptpmorph}}



\section{\label{sec:linauto}Solving Presburger Arithmetic Formulas with {\tt linauto}}




\section{\label{sec:autodot}Displaying Automata with {\tt pl2gastex}}


%!!!

Sometimes, {\tt pl2gastex} gives pretty good results.

\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.5pt}
  \small
  \input{listeven_model}
%END IMAGE
%HEVEA\imageflush
\end{center}

On some more complex examples, {\tt pl2gastex} gives pretty awful
results.

\begin{center}
%BEGIN IMAGE
  \setlength\unitlength{0.3pt}
  \small
  \input{nspriv_model}
%END IMAGE
%HEVEA\imageflush
\end{center}

%\begin{center}
%%BEGIN IMAGE
%  \setlength\unitlength{0.3pt}
%  \small
%  \input{nspriv_twopi}
%%END IMAGE
%%HEVEA\imageflush
%\end{center}

%!!! Explain how {fig:tree3plus2_model} was obtained.


\section{\label{sec:h1getlog}Log Files and {\tt h1getlog}}



\section{\label{sec:bugs}Bugs}


\subsection*{There is no DTD for deterministic tree automata in XML format.}

Yes, I know.  Sorry.  I don't know how to write DTDs.  If anybody
wants to volunteer, the format should be clear from examples produced
by {\tt h1}.  Anyone?



\subsection*{{\tt h1} works for a long time, then gets ``Killed''}

A typical case is that you have exceeded some system quotas.
One case I had was that {\tt h1} was producing a log file
which turned out to exceed 2 Gb, and Linux could not handle
this.  (Or, it does, but using non-portable system calls,
from what I understood.)

If you don't need the log file, use the {\tt -no-log} option to {\tt
  h1}.  Otherwise, use the {\tt -log-out} option to {\tt h1}, and
redirected the standard output.  E.g., instead of \verb/h1 blah.p/,
use \verb/h1 -log-out blah.p > blah.log/.

% \subsection*{Doing {\tt h1 -no-resolve nspriv.p; zcat nspriv.log.gz} fails.}

% Typically, {\tt zcat} complains of {\tt nspriv.log.gz: unexpected end
%   of file}.  This is because {\tt h1} spawns a {\tt gzip -c
%   >nspriv.log.gz} subprocess to compress the log file as it builds it.
% The {\tt gzip} process can only terminate once {\tt h1} has finished
% working, but then needs some more time to complete compression.
% Meanwhile, {\tt zcat} starts decompresssing the file, and fails.  I
% currently know of no way to make {\tt h1} close the stream to its
% subprocess then wait until its subprocess has completed.

% If you want to use the log file produced by {\tt h1} in a script file,
% better use the {\tt -log-out} %
% \index{indexN}{log@{\tt -log-out}}%
% option, and read it from {\tt stdout}.  That is, use {\tt h1
%   -no-resolve -log-out nspriv.p} instead of {\tt h1 -no-resolve
%   nspriv.p; zcat nspriv.log.gz}.

\subsection*{Clause names are lost in converting clauses to Prolog format.}

Yes, this is unfortunate.  A few cases have been corrected, by using
special comments.  But more has to be done.

%\subsection*{How can I visualize alternating or non-deterministic tree automata?}

%For now, you have to determinize them with {\tt pldet}, then build a
%dot file with {\tt autodot}, which you run through {\tt dot} or {\tt
%  dotty}.  This is unfortunately impractical for most automata, and
%not at all pretty.  This definitely needs some improvement.
%Unfortunately, I must admit I am no expert at drawing automata.


%!!! pl2gastex: you may need to stop neato after a while (kill -2 <pid>).

\bibliographystyle{abbrvnat}
\bibliography{h1}

\printindex{indexC}{Concept Index}
\printindex{indexN}{Command Index}

\end{document}
