Prover9 Manual |  | Version 2009-02A

# Inference Rules

When a given clause is selected, all of the enabled inference rules are applied to it. For each inference, one of the parents is the given clause, and all other parents must be in the `usable` list.

Most inference rules distinguish the parents by the roles they play in the inference, e.g., positive or negative literal for binary resolution, nucleus or satellite for hyper rules, and from and into for paramodulation. The given clause can play any role in the inference.

After an inference rule generates a new clause, the clause is processed, which includes simplification operations such as demodulation and `unit_deletion`, and retention tests, such as `max_weight`. Processing also includes several operations that might be considered inference rules, such as `factor` and `new_constants`.

Prover9 uses ordered resolution and paramodulation with literal selection. These methods restrict the literals that are eligible for inference. The resolution and paramodulation inference rules are intended to be <g>complete<g> (exceptions are given in the descriptions of the options below), but we have not done a rigorous analysis of the algorithms, so users should not make any assumptions about completeness. For an overview of ordered inference with literal selection, see the section Ordered Inference below.

## Binary Resolution Rules and Options

    set(binary_resolution).
    clear(binary_resolution).    % default clear

> If this flag is set, binary resolution will be applied to the given clause. The options `literal_selection`, `ordered_res`, and `check_res_instances` determine eligible literals.

    set(neg_binary_resolution).
    clear(neg_binary_resolution).    % default clear

> If this flag is set, negative binary resolution is applied to the given clause. That is, the negative resolved literal must be in a clause in which all literals are negative. The options `ordered_res`, and `check_res_instances` are also used to determine eligible literals.

> Note that there is no inference rule "pos_binary_resolution". Positive binary resolution can be achieved by using the parameter `literal_selection` so that at least one negative literal is always selected. Positive binary resolution is not the dual of `neg_binary_resolution`, because the `literal_selection` technique is not symmetric between positive and negative literals; in particular, selected literals are always negative. The `literal_selection` parameter is always ignored for negative binary resolution.

    set(ordered_res).    % default set
    clear(ordered_res).

> This option puts restrictions on the binary and hyperresolution inference rules (but not on UR-resolution). It says that resolved literals in one or more of the parents must be maximal in the clause.

> See the section Ordered Inference below.

    set(check_res_instances).
    clear(check_res_instances).    % default clear

> This flag applies to the binary and hyperresolution inference rules if the flag `ordered_res` is also set. If `check_res_instances` is set, the `ordered_res` test is is applied after the substitution for the inference has been applied to the parents.

    assign(literal_selection, string).  % default string=max_negative, range [max_negative, all_negative, none]

> This parameter affects to the inference rules `binary_res` and `paramodulation`. It determines which literals are eligible for inference. Here are the accepted values.
> - `max_negative`: negative literals that are maximal w.r.t. the negative literals of the clause are marked;
> - `all_negative`: all negative literals are marked;
> - `none`: no literals are marked;
> If at least one negative literal is always selected (e.g., `max_negative` or `all_negative`), binary resolution will be positive binary resolution, and paramodulation will be positive paramodulation.

> Literal selection is ordinarily used with ordered inference (flags `ordered_res` and `ordered_para`), but it can be used without ordered inference.

## Hyper and UR Resolution Rules and Options

The Hyper and UR resultion rules can resolve more than one literal of one of the parent clauses (the nucleus) with other parent clauses (the <g>satellites</g>), all in one step. An application of one of these inference rules can be viewed as a sequence of binary resolution steps.

    set(pos_hyper_resolution).
    clear(pos_hyper_resolution).    % default clear

> If this flag is set, positive hyperresolution (usually called simply hyperresolution) is applied to the given clause. If the flag `ordered_res` is set, the resolved literals in the satellites (positive parents) must be </g>maximal</g>. If the flags `ordered_res` and `check_res_instances` are both set, the maximality check is done after the substitution for the inference has been applied to the parents. Literal selection is not applied to hyperresolution.

    set(hyper_resolution).
    clear(hyper_resolution).    % default clear

> This flag is a synonym for `pos_hyper_resolution`. The only effect of changing this flag is to make the corresponding change to the flag `pos_hyper_resolution`.

    set(neg_hyper_resolution).
    clear(neg_hyper_resolution).    % default clear

> If this flag is set, negative hyperresolution is applied to the given clause. If the flag `ordered_res` is set, the resolved literals in the satellites (negative parents) must be </g>maximal</g>. If the flags `ordered_res` and `check_res_instances` are both set, the maximality check is done after the substitution for the inference has been applied to the parents. Literal selection is not applied to hyperresolution.

    set(ur_resolution).
    clear(ur_resolution).    % default clear

> If this flag is set, UR resolution (unit-resulting resolution) is applied to the given clause. In fact, the only effect of this flag is that it automatically sets the flags `pos_ur_resolution` and `neg_ur_resolution`

> UR resolution may be <g>incomplete</g> when there are non-Horn clauses.

    set(pos_ur_resolution).
    clear(pos_ur_resolution).    % default clear

> If this flag is set, positive UR resolution is applied to the given clause. That is, the resulting unit clause is a positive clause. Neither ordering constraints nor literal selection is applied to UR resolution.

    set(neg_ur_resolution).
    clear(neg_ur_resolution).    % default clear

> If this flag is set, negative UR resolution is applied to the given clause. That is, the resulting unit clause is a negative clause. Neither ordering constraints nor literal selection is applied to UR resolution.

    set(initial_nuclei).
    clear(initial_nuclei).    % default clear

> This flag puts a restriction on the nucleus for the hyperresolution and UR-resolution inference rules. It says that each nucleus must be an input clause (more precisely, an initial clause).

> Setting this flag may cause <g>incompleteness</g> of the inference system.

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

> If n != -1, then the nucleus for each UR-resolution inference can have at most n literals.

> This option may cause <g>incompleteness</g> of the inference system.

## Paramodulation Rules and Options

    set(paramodulation).
    clear(paramodulation).    % default clear

> If this flag is set, paramodulation is applied to the given clause. If the from literal is oriented (oriented equalities are always heavy=light), the paramodulation is applied left-to-right. If the from literal cannot be oriented Prover9 attempts to paramodulate from both sides of it. Unlike the inference rule superposition, this inference rule goes into "light" sides of equations.

> If the flag `ordered_para` is also set, ordered paramodulation is used.

> If paramodulation involves non-unit clauses, `literal_selection` is used to determine eligible literals.

> Note that the flag `back_demod` set set by default, so that derived equations can be used to rewrite older clauses.

    set(ordered_para).    % default set
    clear(ordered_para).

> This flag places a restrictions on the `paramodulation` inference rule, based on maximal literals. See the section Ordered Inference.

    set(check_para_instances).
    clear(check_para_instances).    % default clear

> This flag applies to the `paramodulation` inference rule and is analogous to the flag `check_res_instances` for `binary_resolution`. It says to apply the ordering tests after the substitution for the inference has been applied to the parent claues.

    set(para_from_vars).    % default set
    clear(para_from_vars).

> This flag says that paramodulation may occur from variables. That is, a literal x=t, in which x does not ocur in t, may be used as the from literal, unifying arbitrary terms with x, and replacing them with t.

> For (unit) equational problems, this flag is nearly always irrelevant.

> Clearing this flag may cause <g>incompleteness</g> of the inference system.

    set(para_from_small).
    clear(para_from_small).    % default clear

> This flag says that paramodulation may occur from smaller sides of equality literals. That is, paramodulation may interoduce larger terms. Roughly speaking, given a literal s=t, in which s > t in the term ordering, the term t may be unified with some other term, which is then replaced with the corresponding instance of s.

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

> If n ≠ -1, each parent in paramodulation can have at most n literals. This option may cause <g>incompleteness</g> of the inference system.

    set(para_units_only).
    clear(para_units_only).    % default clear

> This flag says that both parents for paramodulation must be unit clauses. The only effect of this flag is to assign 1 to the parameter `para_lit_limit`.

> Setting this flag may cause <g>incompleteness</g> of the inference system.

    set(basic_paramodulation).
    clear(basic_paramodulation).    % default clear

> This option hasn't been implemented yet.

## Ordered Inference

This section contains a practical overview of ordered inference as implemented in Prover9. For theoretical presentations, see [Bachmair-Ganzinger-res] and [Nieuwenhuis-Rubio-para].

Prover9 uses ordered inference with literal selection.

- Ordered inference.Within a clause, there is a partial order on literals, determined by the term ordering. A subset of the literals is marked as maximal. (If the clause is ground, the order is total, and the greatest literal is marked as maximal.) The inference rules may be restricted in some cases so that they apply only to maximal literals.
- Literal selection. In each clause, a subset of the negative literals of a clause is marked as selected. (Different clauses may have the subset chosen by different methods.) The inference rules may be restricted in some cases so that they apply only to selected literals.

Ordered inference and literal selection are typically used together, but each can be used without the other, by changing the options `ordered_res` and `literal_selection`. In the following, if `ordered_res` is disabled, simply assume all literals are maximal. The setting `assign(literal_selection, none)` has the effect of disabling literal selection.

### Ordered Binary Resolution with Literal Selection

    A positive literal PL in a clause C is eligible for resolution if
      no literal is selected in C, and PL is maximal in C.

    A negative literal NL in a clause C is eligible for resolution if
      (1) NL is selected in C, or
      (2) no literal is selected in C, and NL is maximal in C.

Note that if at least one negative literals is selected in every clause, we have a version of positive binary resolution, because no literal may be selected in the clause containing the positive resolved literal.

### Ordered Factoring

Prover9 does not do ordered factoring. Instead, if factoring is enabled (see flag `factor`), factoring is applied as much as possible to all newly kept clauses. In theory, factoring can be restricted to maximal literals without losing completeness, but we believe applying it eagerly is more practical.

### Ordered Paramodulation with Selection

For ordered paramodulation with selection, literal eligibility for the "from" literal is that same as eligibilty of the positive literal for ordered resolution with selection.

Literal eligibility for positive "into" literals is that same as eligibilty of the positive literal for ordered resolution with selection.

Literal eligibility for negative "into" literals is the same as eligibilty of the negative literal for ordered resolution with selection.

In other words,

    A positive literal PL in a clause C is eligible for paramodularion
      (as the "from" or the "into" parent) if no literal is selected in C,
      and PL is maximal in C.

    A negative literal NL in a clause C is eligible for paramodulation if
      (1) NL is selected in C, or
      (2) no literal is selected in C, and NL is maximal in C.

### Negative Ordered Binary Resolution

    A positive literal NL in a clause C is eligible for resolution if
      NL is maximal among the positive literals of C.

    A negative literal NL in a clause C is eligible for resolution if
      C has no positive literals, and NL is maximal in C.

Note that negative ordered binary resolution is not the dual of positive ordered binary resolution, because the negative version ignores literal selection.

Next Section: Process Inferred