The h1 Download Pages

Jean Goubault-Larrecq
LSV/UMR 8643, CNRS, ENS Cachan & INRIA Futurs projet SECSI
61 avenue du président-Wilson, F-94235 Cachan Cedex
goubault@lsv.ens-cachan.fr
Phone: +33-1 47 40 75 68   Fax: +33-1 47 40 75 21


New Jan. 2008 distribution! Essentially h1mc changed. Faster, better, and outputs Coq v8 proofs. Look below.

The h1 tool suite is a collection of utilities to handle H1 clause sets [NNS02]. This can also be seen as a tree automaton handling library. Various other tools allow you to extract proof traces, draw pictures of tree automata, generate counter-models and the proofs that they indeed are counter-models (all proofs can be generated for Coq v7), solve quantifier-free Presburger formulae, among other things.

The h1 tool suite is distributed under the GNU General Public License (GPL). The complete source distribution can be found either as a compressed tar ball (use tar -xvjf to decompress), or as a source tree. The latter is still a bit messy, and contains several useless files.

A draft tutorial is also available. Note that much is still missing.


This document was translated from LATEX by HEVEA.