4  The h1 Prover

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

4.1  How to Use h1

• -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 zcat nspriv.log.gz | less 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 H₁ format checking. If n=0, no check is done at all (default). Clauses outside H₁ 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 H₁, 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 :- P₁ (t₁), …, P_n (t_n), of name <name>, by a definite clause q_<name> :- P₁ (t₁), …, P_n (t_n) 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.gz. If h1 was given - as input file (i.e., if h1 reads from standard input), then this file will be h1out.log.gz. If -log-out is given instead of -log, this trace is output, uncompressed, on stdout. If -no-log is given, then no trace is produced at all.
  
  The reason why the trace is compressed by default is because it may be huge. So huge in fact that I've seen cases where it went above the 2 Gb file size limit on Unix files. 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 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.
  
  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 compressed log file Fabrice/alice\_full1.log.gz. The latter is 94.5 Mb. This is not much compared to the uncompressed file, which is a bit more than 40 million lines long, and 2.67 Gb long. These figures are obtained by running

  zcat Fabrice/alice_full1.log.gz | wc -c -l
  

  which itself runs in about 20 s.
  
  
• -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 H₁ 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 H₁ 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) :- P₁ (t₁), …, P_n (t_n) is an input clause, we say that P depends on P₁, ..., P_n. 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 ⇐ P₁ (t₁), …, P_n (t_n) such that, say, t_i is deep, i.e., t_i is neither a variable nor a function applied to variables. Then list the free variables of t_i, say X₁, ..., X_k, 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 P_i and the same t_i, 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 S_a be the set of alternating automata clauses. These can be seen as sort declarations. E.g., the alternating automaton clause P (f (X₁, X₂, X₃)) ⇐ P₁ (X₁), P₂ (X₁), P₃ (X₂) can be read as a rule stating that, if X₁ has sort P₁ and also sort P₂, if X₂ has sort P₃, and even if X₃ has no sort, then f (X₁, X₂, X₃) has sort P. Given any clause H ⇐ P₁ (t₁), …, P_n (t_n), extract a sort environment ρ: for each i such that t_i is a variable X, ρ states that X has sort P_i. Then, for any j such that t_j is not a variable, if we can deduce that t_j has sort P_j using the sort environment ρ and the current sort declarations, then remove P_j (t_j) 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 (t₁, …, t_k)), 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

4.3  Principle of Operation