Description of the Settings

set(hyper_res).

This option activates the inference rule hyperresolution.

set(back_demod).

When new equalities are deduced, use them as rewrite rules.

set(dynamic_demod_all).

Use all new orientable equalities as rewrite rules.

set(index_for_back_demod).

This options causes indexing to be used when searching for terms to which a new rewrite rule can be applied. ROO requires this ``option'' whenever back demodulation is enabled. Otter frequently benefits from this option.

assign(pick_given_ratio,5).

By default Otter chooses each new given clause based on its symbol count. This means that a heavy clause that is needed for the proof cannot be used until all lighter clauses have been used. Recently we have found it useful to mix this strategy with a breadth-first strategy by choosing some percentage of the given clauses according to the order in which they are generated rather than by weight. This setting chooses every sixth given clause in order of generation, and the rest by (minimal) symbol count.

clear(print_kept). clear(print_new_demod).clear(print_back_demod).

These options suppress output, saving file space and a little time.

assign(max_mem,20000).

This setting restricts memory usage to 20 Megabytes. Its real use is in conjunction with the next parameter.

set(control_memory).

This setting has a relatively complex effect. Every ten given clauses, memory usage is analyzed. If more than a third of max_mem has been used, then the max_weight parameter is automatically set to a value calculated such that only the lightest 5% of the clauses in the current set of support have lower weight. No clauses are deleted, but from this point on, new clauses heavier than this weight are discarded. Using this parameter has the effect of allowing the system to choose a value for max_weight and adjust it during the run.

set(knuth_bendix).

This option causes Otter and ROO to automatically set a collection of options that approximate a Knuth-Bendix completion procedure. Under this option, the theorem prover orders equalities, paramodulates from left sides into left sides, and back demodulates.

set(process_input).

This option causes all input clauses to be processed (subsumption, demodulation, equality ordering, back demodulation) as if they were generated clauses.

lex(list of symbols).

This command specifies an ordering on constant, function, and predicate symbols, with smallest first. For the experiments described in this paper, the ordering is used to attempt to orient equalities.

set(lex_rpo).

This options specifies the lexicographic recursive path ordering for comparing terms when attempting to orient equalities.

lrpo_lr_status(list of symbols).

This command specifies that function symbols are to be compared left-to-right when applying the lexicographic recursive path ordering.