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


This page last updated July 9, 2021.
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 as a zipped archive; this uncompresses as a directory H1.1 containing the source (and several useless files).

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

This document was translated from LATEX by HEVEA.