h1 is distributed under the GNU General Public License (see
file COPYING).
In particular, h1 comes with ABSOLUTELY NO WARRANTY.
This is free software, and you are welcome to redistribute it
under certain conditions; see file COPYING.

h1 is a resolution-based solver of Horn clauses in the decidable
class H1; see the paper
  Normalizable Horn Clauses, Strongly Recognizable Relations and Spi
  by Flemming Nielson, Hanne Ries Nielson, and Helmut Seidl,
  Proceedings of the 9th Static Analysis Symposium (SAS'2002),
  Springer-Verlag LNCS 2477, 2003.
However the techniques used in h1 are wildly different from
those of the paper above: h1 is based on ordered resolution
with selection and splittingless splitting (see Jean Goubault-
Larrecq's lecture notes at
	http://www.lsv.ens-cachan.fr/~goubault/cours.html#SOresol
and the 2003 exam:
	http://www.lsv.ens-cachan.fr/~goubault/seidl_ans.ps
Checking satisfiability of sets of H1 clauses is
DEXPTIME-complete.  h1 also has support for interfacing with
Coq, dot, and other tools.  Type 'h1 -h' for help.

h1 was written by Jean Goubault-Larrecq, at the Laboratoire
Spécification et Vérification (LSV), INRIA Futurs projet SECSI &
CNRS UMR 8643 & ENS Cachan.
The example file 'NeedhamSchroeder.clauses.p' was written
by Fabrice Parrennes at LSV.

The h1 package consists of:
- the h1 prover itself;
- the pl2tptp utility, which converts clause sets in Prolog format
  to TPTP format;
- the xmlauto utility, which converts complete deterministic
  automata in XML form to Prolog format;
- the tptpmorph utility, which computes the image of a set of
  clauses in TPTP format by a term algebra morphism (in particular,
  if the input clauses are Horn clauses, this defines the image
  of the languages defined by the input clauses by the morphism).

Jean Goubault-Larrecq acknowledges the support of:
- the RNTL project EVA (Explication et Vérification Automatique
  de protocoles cryptographiques), 2000--2003;
- the ACI Jeunes Chercheurs "S\'ecurit\'e informatique, protocoles
  cryptographiques et d\'etection d'intrusions", 2001--2004;
- the ACI cryptologie VERNAM, 2000--2003;
- the ACI cryptologie Psi-Robuste, 2002--2005.

Fabrice Parrennes acknowledges the support of the above
cited ACI Jeunes Chercheurs "S\'ecurit\'e informatique, protocoles
cryptographiques et d\'etection d'intrusions".