Prover9 Manual Version 2009-11A

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 complete (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. 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 satellites), 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 maximal. 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 maximal. 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 incomplete 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 incompleteness 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 incompleteness 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 incompleteness 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 incompleteness 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 incompleteness 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 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