Automatic Modes

Prover9's automatic mode is set by default. Otter's automatic mode must be explicitly set.

If you simply give Prover9 a set of clauses and/or formulas, Prover9 will look at the clauses and decide which inference rules to use. In addition, it will use two default limits (max_weight and sos_limit) that, although good in practice, can prevent proofs from being found.

If don't like the inference rules that Prover9 selects, you can clear the flag auto_inference and select your own rules. If you wish to remove the limits max_weight and sos_limit, you can clear the flag auto_limits. If you wish to do both, you can clear the flag auto. Prover9 output files show the effects of changing these flags.

set(auto).    % default set
clear(auto).

This is the basic automatic mode of Prover9. The only direct effect of this flag is that it changes several secondary auto flags as follows.

  set(auto) -> set(auto_inference).
  set(auto) -> set(auto_process).
  set(auto) -> set(auto_limits).
  set(auto) -> set(auto_denials).

  clear(auto) -> clear(auto_inference).
  clear(auto) -> clear(auto_process).
  clear(auto) -> clear(auto_limits).
  clear(auto) -> clear(auto_denials).

set(auto_inference).    % default set
clear(auto_inference).

If this flag is set, the input clauses are checked for several syntactic properties such as the presence of equality and non-Horn clauses. Based on the results of the checks, Prover9 decides which inference rules to use. In addition, changing this flag causes the following changes.

  set(auto_inference) -> set(predicate_elim).
  set(auto_inference) -> assign(eq_defs, unfold).

  clear(auto_inference) -> clear(predicate_elim).
  clear(auto_inference) -> assign(eq_defs, pass).

set(auto_process).    % default set
clear(auto_process).

This flag causes several other flags that affect clause processing to be altered based syntactic properties of the initial clauses.

If all clauses are Horn and there are negative nonunits, the flag back_unit_deletion is automatically set. If there are non-Horn clauses, the flags back_unit_deletion and factor are automatically set.

Unlike ordinary option dependencies, the options that are changed by auto_process cannot be undone by placing commands in the input file, because they depend on the structure of the clauses.

set(auto_limits).    % default set
clear(auto_limits).

The only effect of changing this flag is that two parameters are changed in the following ways.

  set(auto_limits) -> assign(max_weight, 100).
  set(auto_limits) -> assign(sos_limit, 10000).

  clear(auto_limits) -> assign(max_weight, INT_MAX).
  clear(auto_limits) -> assign(sos_limit, -1).

set(auto_denials).    % default set
clear(auto_denials).

If this flag is set (the default), Horn sets that have more than one negative clause receive some special initial processing.

We use the term denial to refer to a negative clause in a Horn set, because such clauses usually correspond to the negation of the conclusion. If a Horn set has more than one denial, we assume they correspond to separate conclusions, and the user wishes to have a separate proof of each of the conclusions. We therefore assign to max_proofs the number of negative clauses. Note that this also causes the flag restrict_denials to be set, which prevents multiple proofs of the same conclusion.

An Experimental Automatic Mode

set(auto2).
clear(auto2).    % default clear

assign(lrs_ticks, n).  % default n=-1, range [-1 .. INT_MAX]

assign(lrs_interval, n).  % default n=50, range [1 .. INT_MAX]

assign(min_sos_limit, n).  % default n=0, range [0 .. INT_MAX]

These three parameters work together and are used to automatically adjust the parameter sos_limit by means of a "limited resource strategy" [RV-lrs]. If lrs_ticks ≥ 0, the method is applied.

This is an experimental feature and is not recommended for general use.