Semantic Guidance

Prover9 has a method of using finite interpretations to guide the search for a proof; in particular, to help select the given clause.

To use semantic guidance the user gives one or more interpretations along with the ordinary Prover9 input. All clauses (input and derived) that are eligible to be selected as given clauses are evaluated in the interpretations. If a clause is false in all of the interpretations, it is marked as "false" and given the attribute label(false); if it is true in any of the interpretations, it is marked as "true". (There is an exception: see the parameter eval_limit below.)

If a clause being evaluated contains a symbol that is not in an interpretation, a warning message is given, and the clause receives the value "true".

When selecting the given clause, Prover9 may use the parameters true_part,and false_part, as described on the page Selecting the Given Clause. With semantic guidance (explicit interpretations), the "true_part" and "false_part" refer simply to clauses marked as "true" and "false" with respect to the interpretations.

Format of Interpretations for Semantic Guidance

The interpretations are finite and must be in the format produced by Mace4. They must appear in a list that starts with list(interpretations). and ends with and_of_list. The following example is a lattice in terms of the meet and join operations.

list(interpretations).
interpretation(6, [], [
    function(^(_,_), [
        0,0,0,0,0,0,
        0,1,2,3,4,5,
        0,2,2,0,0,0,
        0,3,0,3,5,5,
        0,4,0,5,4,5,
        0,5,0,5,5,5]),
    function(v(_,_), [
        0,1,2,3,4,5,
        1,1,1,1,1,1,
        2,1,2,1,1,1,
        3,1,1,3,1,3,
        4,1,1,1,4,4,
        5,1,1,3,4,5])]).
end_of_list.

An Example of Semantic Guidance

Here a job that uses the preceding interpretation for semantic guidance.

prover9 -f LT-82-2.in > LT-82-2.out

Notes about the preceding job.

The interpretation is the only additional input needed to give semantic guidance. The default values of the parameters age_part, true_part, false_part, and eval_limit, work well for this job (and many others).
The interpretation does not contain Skolem constants that appear in the denial, and warning messages are given when Prover9 attempts to evaluate clauses containing those Skolem constants. (They receive the value "true".)
One of the input clauses is assigned the attribute label(false), because it is false in the interpretation.
The "false" given clauses (#12, #13, #17, #18, #22, #23, ...) are mostly heavier than the "true" given clauses, showing that they would likely not enter the search at such an early stage without semantic guidance.
At given clause #138, there are no more false clauses to select; and then several more are inferred and given near the end of the search, leading to a proof.
This job takes about 11 seconds. A similar job without semantic guidance takes about 25 minutes to find a proof.

Advice on Selecting Interpretations

If the conjecture formulates naturally as

theory, hypotheses -> conclusion,

a good first step is to try the smallest model of the theory in which the conclusion is false. The preceding example has that form, and the interpretation used in the that example can be easily found with the following Mace4 job.

mace4 -N10 -f LT-82-2-interp.in > LT-82-2-interp.out

If the conjecture formulates naturally as

theory -> conclusion,

with no obvious hypothesis, one can try to slightly weaken the theory in some way that relates to the conclusion, and use a model of the weakened theory in which the conclusion is false.

Options for Semantic Guidance

Aside from the parameters true_part,and false_part, which may be used regardless of whether semantic guidance is in effect, there are just two options to control semantic guidance.

assign(multiple_interps, string).  % default string=false_in_all, range [false_in_all, false_in_some]

This parameter is used when there are multiple interpretations. It determines the method for marking clauses as "false": false in all interpretations, or false in some interpretations.

assign(eval_limit, n).  % default n=1024, range [-1 .. INT_MAX]

If an interpretation is large, or if a clause being evaluated has many variables, evaluation can take too long, because it must consider each instance of the clause over the domain of the interpretation. That is if an interpretation has size d, and a clause has v variables, evaluation has to consider d^v instances of the clause to determine that it is true. This parameter causes large evaluations to be skipped.
This parameter applies when explicit interpretations are being used to select the given clause. When a clause is being evaluated in an interpretation, if the number of ground instances that would be considered is greater than n, the evaluation is skipped and the clause is assigned the value true.
The default value of 1024 allows

clauses with up to 3 variables to be evaluated in interpretations up to size 10,
clauses with up to 4 variables to be evaluated in interpretations up to size 5,
clauses with up to 5 variables to be evaluated in interpretations up to size 4,
clauses with up to 6 variables to be evaluated in interpretations up to size 3, and
clauses with up to 10 variables to be evaluated in interpretations of size 2.

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

This parameter is another (more convenient) way to limit the evaluation of clauses. It overrides the parameter eval_limit. Clauses with more than n variables will not be evaluated in the largest interpretation(s).
In particular, if the value n is set to some value other than -1, the parameter eval_limit will be reset to dⁿ, where d is the size of the largest interpretation in the input.
Note that if there are multiple interpretations of different sizes, and if multiple_interps is set to "false_in_some", then clauses with more than n variables may be evaluated in the smaller interpretations.

Next Section: Mace4