1 Installing h1

1 Installing `h1`

To install, the preferred way is as follows. First, install GimML, a variant of the Standard ML language of my own.

If you install from sources, do not forget to install the lexer generator glex and the parser generator gyacc.

Second, fetch the h1 tool suite compressed tar ball. Decompress anywhere you want. Then type

tar -xvjf h1.1.tbz
cd H1.1/
./configure
make
make install exec_prefix=/usr/local

The latter assumes you want to install the h1 tool suite binaries in /usr/local/bin, etc.

The files in the h1 tool suite include:

h1: the h1 prover;
pl2tptp: convert alternating tree automata in Prolog notation to TPTP input_clause syntax;
tptp2dfg: quick hack to convert TPTP input_clause syntax to SPASS dfg syntax (corrects trail overflow bug in tptp2X);
tptpmorph: apply language morphisms to tree automata, and more generally first-order clause sets in TPTP input_clause syntax;
pldet: determinize alternating tree automata;
plpurge: purge alternating tree automaton from unreachable states;
h1trace: extract proof from trace file generated by h1;
h1logstrip: purge trace file from clauses that do not lead to a refutation;
h1mc: model-check first-order logic clause sets against models described as alternating tree automata, in Prolog syntax;
h1mon: monitor progress of h1 in real-time, by scanning h1.pgr file;
linauto: convert quantifier-free Presburger formulae to equivalent deterministic automata;
autodot (obsolete): draw deterministic tree automata through dot.
pl2gastex: draw alternating tree automata, using dot, neato or twopi as layout engines, and rendering through the gasT_EX library for LaT_EX.