## 4 The `h1` Prover

- 4.1 How to Use `h1`
- 4.2 Theoretical Background
- 4.3 Principle of Operation

Most of the features of `h1` are explained in Section 3. We explain the structure of the `h1` command line in Section 4.1, then turn to the theoretical basis of `h1` in Section 4.2. We refine this description in Section 4.3, by stating the precise rules used by `h1`.

### 4.1 How to Use `h1`

The `h1` tool recognizes the following options. As in all Unix tools, options start with a minus sign `-`. Some options are flags, which can be toggled between an active state and a deactivated state. In this case, the convention used in `h1` and other tools of the `h1` suite is to have `-`<option> activate the option, while `-no-`<option> deactivates it.
The options recognized by the `h1` prover are:

- `-h` prints help. This is basically a terse summary of the current explanation.
- `-v`< n> (with no space between `-v` and < n>) sets the verbosity level to the integer n. Also, `-v` sets the verbosity level to 1. The default is 0 (run silently).
  While other tools of the `h1` suite understand verbosity as a way of printing more or less comments on `stderr`, the `h1` prover itself prints these comments into the log file. That is, into <filename>`.log.gz` if run as `<filename>`, into `h1out.log.gz` if run without a file, i.e., as `h1 -`, and on `stdout` if the `-log-out` option is activated.
  This can be useful to examine how `h1` proceeds to derive new clauses and to remove redundant clauses while it is reasoning.
  At verbosity level 1, i.e., with `-v1` or `-v`, `h1` adds comments of the form `% |-` <clause> to say which clauses are being derived, and added to the queue of clauses waiting to be processed. Normally, `h1` only lists clauses it is currently processing. At verbosity level 1, `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 `-v2`, `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 `h1 -v1 nspriv.p` or `h1 -v2 nspriv.p`, followed by the command `less nspriv.log` to see concrete examples of such comments.
  The `-v` options are only active if some log file is output at all, that is, if `-log` or `-log-out` is in effect. (By default, `-log` is active.)
- `-check-h1` < n> enables or disables H1 format checking. If n=0, no check is done at all (default). Clauses outside H1 are approximated as in Section 3.4, using a slightly more clever variant of the approximation algorithm of [2005 (Goubault-Larrecq)]. If n=1, warnings are printed as to which clauses are not in H1, and what the problem is, then `h1` proceeds approximating all clauses. If n=2, the same warnings are printed; however, if any warning has been emitted, then `h1` will stop and refuse to solve the given clause set.
- `-first`, `-all`: by default, `h1` works as any prover, and stops on finding the first contradiction (`-first`). With the `-all` option, `h1` will report all goal clauses through which a contradiction can be found. See Section 3.4 for an example.
  The way `h1` does it is by replacing every goal clause `false` :- P1 (t1), …, Pn (tn), of name <name>, by a definite clause q<name> :- P1 (t1), …, Pn (tn) for a special nullary predicate symbol q<name>, called a signalling symbol. With the `-first` option, as soon as `h1` derives a signalling symbol, it prints its name inside `*** Derived:` and `***` and stops. With the `-all` option, `h1` prints the names of all signalling symbols that can be derived.
- `-log`, `-log-out`, `-no-log`: by defaut, `h1` outputs a trace of what it is doing into a log file (`-log`). If `h1` was called on file <filename>`.p`, then the trace will be in <filename>`.log`. If `h1` was given `-` as input file (i.e., if `h1` reads from standard input), then this file will be `h1out.log`. If `-log-out` is given instead of `-log`, this trace is output on `stdout`. If `-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. To see a rather extreme example, run

      memtime h1 -progress Fabrice/alice_full1.p

  This is a 459 clause example, generated automatically from the static analysis by an early and faulty version of the Csur static analyzer [2005 (Goubault-Larrecq and Parrennes)] of a small C implementation of the Needham-Schroeder public-key protocol (not the same as the symmetric-key protocol of Section 3.4). 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.
  However, you risk having the following output instead:

      Killed [25]
      1372.43 user, 12.62 system, 1414.11 elapsed -- Max VSize = 240624KB, Max RSS = 239348KB

  This is what happens when the log file exceeds its maximum allowed size. To avert this, run:

      memtime h1 -progress -log-out Fabrice/alice_full1.p >alice_full1.log

  This outputs the log file to `stdout`; then the Unix shell knows how to record this in a file almost as large as you wish.
  `Fabrice/alice\_full1.p` is the largest example we can deal with. Note however that the time and space used by `h1` are more related to the structure than to the size of the input problem; e.g., `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 `h1`.
  You may want to run

      watch h1mon h1.pgr

  in parallel, to see how `h1` progresses on `Fabrice/alice\_full1.p`. (See Section 4.3.) To cut it short, `Fabrice/alice\_full1.p` will be detected as (possibly) unsatisfiable by `h1`, and will generate the log file `Fabrice/alice\_full1.log`. This is 2.73 Gb large. Early versions of `h1` instead compressed the log file on the file using `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 `h1` tool suite.
- `-model`, `-no-model`: by default, `h1` outputs a candidate model of the input clause set, as a set of Horn clauses, into file <filename>`.model.pl`, if `h1` was called on file <filename>.p, or into `h1out.model.pl` if `h1` expects its input from standard input.
  The `h1` prover is 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: `h1mc` will then complain, and state which clauses are not satisfied in the candidate model. See Section 6.
  To understand what this candidate model may be, especially in the case where there is no model, see Section 4.2: the candidate model is just the subset of all alternating automaton clauses, and universal clauses of the final, saturated clause set that `h1` eventually computes.
- `-progress`, `-no-progress`: by default, this is deactivated (`-no-progress`). If activated with `-progress`, a kludge is enabled that allows one to monitor `h1`'s progress: a special file `h1.pgr` is created and written into as `h1` goes forward. Each time `h1` adds a clause, subsumes a clause, or does anything of the kind, it adds a conventional character to `h1.pgr`. Using `h1mon h1.pgr` at any time while `h1` is running will give you instantaneous statistics about how many operations `h1` has performed until now. See Section 4.3 for more explanations. Using `watch` in combination with `h1mon`, as in `watch h1mon h1.pgr`, is particularly useful here.
- `-resolve`, `-no-resolve`. By default (`-resolve`), `h1` computes an H1 approximation of the given clause set, then saturates the latter by a form of resolution. The `-no-resolve` disables the resolution engine, so that `h1 -no-resolve` merely produces the H1 approximation into the log file (see `-log` option). This is useful to just see what the approximated clauses actually are. To actually see these clauses, run `h1getlog processed` on the log file. See 3.4 for an example.
- `-trim`, `-no-trim`. By default (`-trim`), `h1` does a quick preprocessing phase (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) :- P1 (t1), …, Pn (tn) is an input clause, we say that P depends on P1, ..., Pn. A predicate symbol P is needed if and only if there is a goal clause of the form `false` :- …, P (t), …, or if some needed predicate symbol depends on P, inductively. By default, `h1` removes all clauses headed by unneeded predicate symbols.
  This is useful to avoid `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, `h1` may lose quite some time saturating it by resolution. Trimming will just eliminate all clauses, and `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 `h1` as a tree automaton tool, as in Section 3.3, you will probably want precisely to feed `h1` with just definite clauses, no goal clause, and expect `h1` to output some compiled alternating tree automaton computing the same languages. To obtain this result, use `-no-trim`.
- `-path-refine` < n>. Another trick that `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 4.2. This consists essentially in computing the sets of paths through atoms in the least Herbrand model, truncated to some fixed length. The `-path-refine` option allows one to specify what the cutoff length should be. By default, it is 3.
- `-alternation`, `-no-alternation`. By default (`-alternation`), `h1` produces an alternating tree automaton as model in the model file (see `-model` option). With the `-no-alternation` option, `h1` produces a non-deterministic tree automaton. This is in general bigger than the corresponding alternating tree automaton, so that `h1` may take more time saturating clauses with the `-alternation` option. See Section 3.3.4.
- `-deep-abbrv`, `-no-deep-abbrv`. By default (`-deep-abbrv`), `h1` uses a rule called abbreviation of deep terms, which accelerates resolution, sometimes spectacularly. This rule has the following effect. Given some clause H ⇐ P1 (t1), …, Pn (tn) such that, say, ti is deep, i.e., ti is neither a variable nor a function applied to variables. Then list the free variables of ti, say X1, ..., Xk, create a fresh predicate symbol Q, and replace the above clause by

  H | ⇐ | P1 (t1), …, Pi−1 (ti−1), Q (X1, …, Xk), Pi+1 (ti+1), …, Pn (tn)
  Q (X1, …, Xk) | ⇐ | Pi (ti)

  In fact, Q needs not be fresh: if we apply the same rule on the same Pi and the same ti, we generate the same Q. Using `-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.
- `-sort-simplify`, `-no-sort-simplify`. By default (`-sort-simplify`), `h1` uses a rule called 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 Sa be the set of alternating automata clauses. These can be seen as sort declarations. E.g., the alternating automaton clause P (f (X1, X2, X3)) ⇐ P1 (X1), P2 (X1), P3 (X2) can be read as a rule stating that, if X1 has sort P1 and also sort P2, if X2 has sort P3, and even if X3 has no sort, then f (X1, X2, X3) has sort P. Given any clause H ⇐ P1 (t1), …, Pn (tn), extract a sort environment ρ: for each i such that ti is a variable X, ρ states that X has sort Pi. Then, for any j such that tj is not a variable, if we can deduce that tj has sort Pj using the sort environment ρ and the current sort declarations, then remove Pj (tj) 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.
- `-monadic-proxy`, `-standard-approx`. By default (`-standard-approx`), the approximation `h1` uses (see Section 3.4) is a slight refinement of that of [2005 (Goubault-Larrecq)]. This keeps more information, i.e., it is more precise in general, than the probably more intuitive approximation of [1991 (Frühwirth et al.)], which tries to capture the so-called types of variables in each input clause. The `-monadic-proxy` option forces `h1` to use the latter, less precise approximation. The idea is that, by using a less precise approximation, `h1` could run faster. Experience until now has shown, on the contrary, that the less precise approximation is also slower: `h1` generates many spurious clauses that just could not be generated with the more precise approximation.
  In other words, `-monadic-proxy` is a false good idea. This option is therefore obsolescent.
- `-body-chop` < n>. Yet another false good idea. Forces `h1` to keep only at most n atoms of depth at least 1 in bodies of clauses generated by resolution. In other words, if `h1` ever tries to generate a clause with m > n atoms of depth at least 1, i.e., of the form P (f (t1, …, tk)), it will savagely remove m−n of them. Resolution then becomes unsound, but will remain complete. That is, if `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.

### 4.2 Theoretical Background

The essentials of the algorithmic underpinnings of `h1` are described, rather tersely, in [2005 (Goubault-Larrecq)]: `h1` implements a form of ordered resolution with selection

### 4.3 Principle of Operation