Hints

Hint clauses can be used to help guide Prover9's search. Prover9's input can contain any number of hint lists (which are simply concatenated by Prover9).

Each list of hint clauses must start with formulas(hints). and end with end_of_list. Any clause is acceptable as a hint. For example (the label attributes are optional),

formulas(hints).
    x ' * (x * y) = y       # label(6).
    x * (x * y) = y         # label(7).
    x * (y * (x * y)) = e   # label(8).
    x ' ' * e = x           # label(9).
    x ' * e = x             # label(10).
    x ' = x                 # label(11).
    x * e = x               # label(12).
    x * (y * x) = y         # label(13).
    x * y = y * x           # label(14).
end_of_list.

A derived clause matches a hint if it subsumes the hint. If a clause matches more than one hint, the first matching hint is used.

In Otter, "matching a hint" can mean (depending on the parameter settings) subsumes, subsumed by, or equivalent to. These other types of matching may be added to Prover9 if there is any demand for them.

Hints are used primarily when selecting given clauses. The mechanism for doing this is the given-clause selection procedure. In short, the default value of the hints_part parameter says to select clauses that match hints (lightest first) whenever any are available.

Hints are also used when deciding to keep a new clause. Clauses that match hints are not deleted by any of the parameters max_weight, max_vars, max_literals, or max_depth.

Where do Hints Come From?

Hints frequently consist of proofs, perhaps many, of related theorems.

Bob Veroff developed the concept, installing code for hints in an early version of Otter, to experiment with his method of proof sketches [Veroff-hints, Veroff-sketches]. In the proof sketches method, a difficult conjecture is attacked by first proving several (or many) weakened variants of the conjecture, and using those proofs as hints to guide searches for a proof of the original conjecture.

The program Prooftrans, which is distributed along with Prover9, can be used to extract proofs from a Prover9 output file and transform the proofs to lists of hints suitable for input to subsequent Prover9 jobs.

An Example

This example consists of four jobs. The first is a proof of a nontrivial theorem called "hard". The other three jobs prove the hard theorem indirectly by first proving an easier theorem (in this case, the easier theorem simply the harder theorem with an extra assumption); then using the proof of the easier theorem as hints to help prove the hard theorem.

A Prover9 job that proves the hard theorem.
```
prover9 -f hard.in > hard.out
```
A proof of the easier thorem.
```
prover9 -f easy.in > easy.out
```
A Prooftrans job converts the proof of the easier theorem into a list of hints.
```
prooftrans hints -f easy.out > easy.hints
```
A Prover9 job that uses the hints to prove the harder theorem.
```
prover9 -f hard.in easy.hints  > hard-hints.out
```

Proving the hard theorem indirectly (jobs 2,3,4) takes about 1/4 the time as proving it directly (job 1). Of course the difficult and interesting part of working this way is finding good "easy" theorems.

Special Weight Assignments

When the given clause selection procedure calls for a clause that matches a hint, the lightest such clause is chosen. Ordinarily, clauses that match hints are weighed just as any other clause is weighed. However, if one believes some hints are more important that others, one can, in effect, say "any clause that matches this hint gets a specific weight". This is accomplished by attaching a bsub_hint_wt attribute to the hint, as in the following example.

formulas(hints).
  x ' * (x * y) = y     # label("very important hint") # bsub_hint_wt(-100).
end_of_list.

Another way to assign a special weight is with the following flag.

set(breadth_first_hints).
clear(breadth_first_hints).    % default clear

Setting this flag causes all clauses that match hints to receive weight 0. The effect is as if each hint had the attribute bsub_hint_wt(0). This causes clauses that match hints to be selected in the order they are generated.

The weight assigned by any of the preceding methods may be modified if the flag degrade_hints is set.

Hint Degradation

In many searches that use hints, a given hint can match many different derived clauses. As a hint matches more and more clauses, we wish its influence to diminish. This is the idea behind Veroff's hint degradation method.

set(degrade_hints).    % default set
clear(degrade_hints).

If this flag is set, a weight penalty is added to clauses that match hints that have been previously matched. The following procedure is used. Given a newly derived clause, say C, assume we find a hint that matches the clause; let n be the number of times the hint has already been matched; then the weight of C is increased by (n * 1000). In other words, 1000 is added for each previous match of the hint.
The effect of this procedure is (usually) that clauses matching hints are selected in the following order: clauses matching hints that have not been matched before, clauses matching hints that have been matched once before, and so on.

Keeping/Limiting Clauses the Match Hints

Ordinarily, when a clause matching a hint is derived, the clause will be retained even if it violates limits such as max_weight. Setting the following flag will cause those limits to be applied to such clauses, and it may be useful with trying to simplify known proofs.

set(limit_hint_matchers).
clear(limit_hint_matchers).    % default clear

If this flag is set, the parameters max_weight, max_literals, max_depth, and max_vars will be applied to clauses that match hints (as well as to clauses that don't match hints).
Otherwise (the default), those limits will not be applied to clauses that match hints.

Back Demodulation of Hints

When hints come from proofs in which equality and rewriting play a major role, they may have trouble guiding a search, because the rewriting may occur in different ways in the new search. In particular, a hint may fail to match a clause, because the clause has been rewritten and the hint has not. This is the motivation for the following feature.

set(back_demod_hints).    % default set
clear(back_demod_hints).

If this flag is set, hints are back demodulated. That is, they are kept simplified with respect to the current set of demodulators.

Labels on Hints

Label attributes on hint clauses get special treatment. When a hint containing a label matches a clause, the label attribute is copied to the clause.

The following flag addresses the situation in which the input contains sets of equivalent hints. (This situation frequently occurs when the hints contain many proofs of similar theorems.)

set(collect_hint_labels).
clear(collect_hint_labels).    % default clear

If this flag is set, and the hints list contains a set of equivalent hints, only the first copy of the hint is retained. However, the labels from all of the other equivalent hints are collected and put on the retained copy. When a clause matches the retained hint, it gets copies of all of the labels from the equivalent hints.
If this flag is clear, when a clause matches a set of equivalent hints, it receives the label (if any) from the first copy only.

Next Section: Semantics