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.
set(binary_resolution). clear(binary_resolution). % default clear
If this flag is set,positive binary resolution will be applied to the given clause.If the flag ordered_res is set, there are additional restrictions on both parents: the literal resolved in the positive parent must be
maximal , and the literal in the nonpositive parent must satisfy the literal_selection parameter.If the flags check_res_instances and ordered_res aren 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.
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.If the flag ordered_res is set, there are additional restrictions on both parents: the literal resolved in the negative parent must be
maximal , and the literal in the nonnegative parent must satisfy the literal_selection parameter.If the flags check_res_instances and ordered_res aren both set, then the ordering tests described in the preceding paratgraphs are applied after the substitution for the inference has been applied to the parent clauses.
assign(literal_selection, string). % default string=maximal, range [maximal, first_maximal, all, first]
This parameters applies to the binary resolution inference rules, and it determines which literals of the "other" parent are eligible for resolution. That is, for binary_resolution, it applies to the nonpositive parent, and for neg_binary_resolution, it applies to the nonnegative parent. Here are the accepted values.
- maximal: maximal literals are eligible;
- first_maximal: the first maximal literal is eligible;
- all: all literals are eligible;
- first: the first literal is eligible.
set(hyper_resolution). clear(hyper_resolution). % default clear
If this flag is set,positive 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.
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.
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, positiveUR resolution is applied to the given clause. That is, the resulting unit clause is a positive clause. Ordering constraints are not applied to UR resolution.
set(neg_ur_resolution). clear(neg_ur_resolution). % default clear
If this flag is set, negativeUR resolution is applied to the given clause. That is, the resulting unit clause is a negative clause. Ordering constraints are not applied to UR resolution.
set(initial_nuclei). clear(initial_nuclei). % default clear
This flag puts a restriction on thenucleus for the hyperresolution and UR-resolution inference rules. It says that each nucleus must be an input clauses (more precisely, aninitial clause ).
assign(ur_nucleus_limit, n). % default n=-1, range [-1 .. INT_MAX]
If n != -1, then thenucleus for each UR-resolution inference can have at most n literals.
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 bemaximal in the clause. For binary_resolution and hyper_resolution, the resolved literals in the positive parents must be maximal, and for neg_binary_resolution and neg_hyper_resolution, the resolved literals in the negative parents must be maximal.
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.
set(paramodulation). clear(paramodulation). % default clear
If this flag is set, paramodulation is applied to the given clause. If thefrom literal is oriented (oriented equalities are always heavy=light), the paramodulation is applied left-to-right. If thefrom literal cannot be oriented Prover9 attempts to paramodulate from both sides of it according to the flag check_para_instances.If the flag ordered_para is also set, the
from clause must be positive, and equality literal that is used in thefrom clause must be maximal. If the flag check_para_instances is also set, the equalitySetting this flag 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_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 mostliterals.
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. It says that thefrom parent must be positive and thefrom literal must be maximal.
set(check_para_instances). clear(check_para_instances). % default clear
This flag applies to the paramodulation inference rule when thefrom literal cannot be oriented.If this flag is set and the
from literal cannot be oriented, Prover9 applies the substitution for the inference to thefrom literal to determine if the instance can be oriented. If so, it will not apply the paramodulation backward (light-to-heavy).If this flag is clear, paramodulation occurs from both sides of nonorientedable equality literals.