Prover9 Manual Version June-2006

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 any of the interpretations, it is marked as "false" and given the attribute label(false); if it is true in all 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 always uses the parameters age_part, 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 terms(interpretations). and ends with and_of_list. The following example is a lattice in terms of the meet and join operations.

terms(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.

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 hypothesis and conclusion are both 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 age_part, true_part,and false_part, which used regardless of whether semantic guidance is in effect, there is just one option, eval_limit, to control semantic guidance.

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 dv instances of the clause to determine that it is true. The following parameter causes large evaluations to be skipped.

assign(eval_limit, n).  % default n=1024, range [-1 .. INT_MAX]
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 the 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