Prover9 Manual |  | Version 2009-02A

# More Search Prep

    set(expand_relational_defs).
    clear(expand_relational_defs).    % default clear

> If this flag is set, Prover9 looks for relational definitions in the assumptions and uses them to rewrite all occurrences of the defined relations elsewhere in the input, before the start of the search. The expansion steps are detailed in the output file and appear in proofs with the justification `expand_def`.

> Relational definitions must be closed formulas for example,

>     formulas(assumptions).
>       all x all y all z (A(x,y,z) <-> ((x <= y & y <= z) | (z <= y & y <= x))).
>     end_of_list.

> If there are circular definitions, Prover9 will immediately exit with a fatal error.

> This flag eliminates predicate symbols, and its effects overlap somewhat with the flag `predicate_elim`.

> Here is a trivial example, using the transitivity-of-subset problem.

>     prover9 -f subset_trans_expand.in > subset_trans_expand.out

> For more examples using this flag, see the problem set "Ternary Relations in Lattices", which is available from the Prover9 Web page.

    set(predicate_elim).    % default set
    clear(predicate_elim).

> If this flag is set, Prover9 applies a procedure that attempts to eliminate predicate symbols from the problem before the start of the search. The eliminations occur by resolution, and those steps show up as ordinary resolution inferences in any proofs that are found. The procedure works by selecting an eliminable predicate symbol, say `P`, then doing some set of resolution inferences on `P`, then removing all clauses that contain `P`. The procedure is intended to preserve the existence of proofs; however, if there are multiple goals, predicate elimination may prevent multiple proofs.

> The effects of this flag overlap somewhat with `expand_relational_defs`, which also eliminates predicate symbols.

    assign(fold_denial_max, n).  % default n=0, range [-1 .. INT_MAX]

> This parameter applies to negated ground input equalities in which neither side is a constant, say `f(a,b) != f(b,a)`. If the left-hand side has fewer than n symbols, a new constant is introduced and set equal to the left-hand side. This operation is applied to at most one clause in the input `sos` list.

    set(sort_initial_sos).
    clear(sort_initial_sos).    % default clear

> If this flag is set, the `sos` list is sorted just before the start of the search. The order (somewhat arbitrary) is
> - positive clauses < negative clauses < mixed clauses;
> - fewer symbols < more symbols;
> - fewer literals < more literals;
> - shallower < deeper.

    set(process_initial_sos).    % default set
    clear(process_initial_sos).

> If this flag is set, clauses in the initial `sos` list will be handled (with a few exceptions) as if they were inferred. For example, demodulation, subsumption, and the check for unit conflict will be applied. The exceptions are that none of `max_weight`, `max_vars`, `max_depth`, or `max_literals` will be applied. (These four parameters are never applied before the first given clause is selected.)

> This flag should be cleared only in very rare circumstances.

Next Section: Search Limits