Prover9 Manual		Version 2009-02A

Inference Rules

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.

• 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

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]

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

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 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.

Ordered Factoring

Ordered Paramodulation 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.