Most inference rules distinguish the parents by the roles they play in the inference, e.g., positive and nonpositive for binary resolution, nucleus and 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. For general information on ordered inference, see the section Ordered Inference below.
set(binary_resolution). clear(binary_resolution). % default clear
If this flag is set, binary resolution will be applied to the given clause; literal_selection is used to determine eligible literals.If the flag ordered_res is also set, ordered resolution.
If the flags check_res_instances and ordered_res are both set, then the ordering tests are applied after the substitution for the inference has been applied to the parent clauses.
set(neg_binary_resolution). clear(neg_binary_resolution). % default clear
If this flag is set, negative binary resolution will be applied to the given clause. That is, the negative resolved literal must be in a clause in which all literals are negative.If the flag ordered_res is also set, the negative resolved literal must be maximal in its clause, and the positive resolved literal must be maximal among the positive literals of its clause.
If the flags check_res_instances and ordered_res are both set, then the ordering tests described in the preceding paragraphs are applied after the substitution for the inference has been applied to the parent clauses.
Note that neg_binary_resolution is not the dual of positive binary resolution (implemented with binary_resolution and positive_inference), 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=maximal_negative, range [maximal_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.Literal selection is ordinarily used with ordered inference (flags ordered_res and ordered_para), but it can be used without ordered inference.
- maximal_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;
set(positive_inference). % default set clear(positive_inference).
The only direct effect of this flag is that setting it causes the literal_selection parameter to be changed as follows.set(positive_inference) -> assign(literal_selection, maximal_negative).This setting causes binary_resolution and paramodulation to be restricted so that one of the two parents is a positive clause.
set(pos_hyper_resolution). clear(pos_hyper_resolution). % default clear
If this flag is set, positive hyperresolution (usually called simply hyperresolution) will be 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 will be 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) will be 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
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 are 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 are 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).
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.
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.
Setting the flag paramodulation causes the flag back_demod to be automatically set. Back demodulation can be disabled by placing clear(back_demod) after set(paramodulation) in the input file.
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.
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.
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.
set(basic_paramodulation). clear(basic_paramodulation). % default clear
This option hasn't been implemented yet.
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.