Goals and Denials

This section shows how the conclusion(s) of a conjecture can be stated in positive form, how one can search for direct proofs as opposed to bidirectional proofs, and how multiple conclusions are stated and handled.

Terminology

Conclusion: this term is used informally.
Goal: this term refers to a conclusion stated in positive form.
Denial clause: this term refers to a negative clause in a Horn set, because such clauses usually correspond to the negation of a conclusion.

Goals: Stating Conclusions in Positive Form

In Otter, the conclusions are always stated in negated form.

Prover9 allows the user to state conclusions in positive form by using the list formulas(goals). However, Prover9 always works by refutation, so the clauses or formulas in the goals lists are negated as described below, and the results are appended to the sos clause list before the search starts. In other words, goals are "syntactic sugar" for input, and have nothing to do with the way Prover9 conducts its search for refutations.

When the conclusion is given in positive form, the user has no control over the Skolem symbols (if any) that Prover9 introduces. If the user needs some control of the Skolem symbols, for example, to insert them into the symbol precedence at a particular spot, or to include them in the weighting function, the user should do the Skolemizing and give the conclusion in negated form.

If there is just one formula in formulas(goals), the meaning is clear: the formula is processed by first taking its universal closure, then negating. The formula is then handled exactly as if it had been input in formulas(sos), that is, by Skolemizing and transforming to clauses.

Multiple Goals

If there is more than one formula in formulas(goals), the meaning is not clear. Is the conclusion the disjunction of those formulas? Or the conjunction? The answer: disjunction: if any goal is proved, the proof is reported, printed, and counted.

Multiple complex goals are not allowed, because the quantification of free variables can be very confusing. Therefore Prover9 enforces the following rule.

If there is more than one formula in the goals list, each must be a positive universal conjunctive formula, that is a formula constructed from atomic formulas, universal quantification, and conjunction only.

To avoid this restriction, one can always write the conclusion clearly as a single goal formula containing any of the logic connectives and quantification. However, if the conjecture involves multiple complex conclusions, we recommend, for search efficiency, separate Prover9 searches.

If there are multiple goals, each is processed separately by applying universal closure, negation, and transformation to clauses. After this processing, Prover9 forgets that there were multiple goals and simply searches for refutations.

When there are multiple goals, and when the user wishes to prove more than one goal, the parameter max_proofs should be set to an appropriate value. (The flag auto_denials (default set) can do so automatically.)

Multiple Proofs

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

This parameter tells Prover9 to stop searching when the n-th proof has been found.

Denials: Negative Clauses in Horn Sets

Denial clauses (negative clauses in Horn sets) can be derived from goals, or they can be input directly as negative clauses.

Multiple Proofs of the Same Conclusion

set(reuse_denials).
clear(reuse_denials).    % default clear

If this flag is set, when a denial clause (a negative clause in a Horn set) is used in a proof, and when max_proofs says to search for more proofs, subsequent proofs may be of the same conclusion. (Multiple proofs of the same conclusion may be useful when one is searching for short proofs.)
If this flag is clear, then when a proof is found, the denial and all of its descendants are disabled so that they will not appear in subsequent proofs.
This flag is independent of the flag restrict_denials.

Auto_denials

set(auto_denials).    % default set
clear(auto_denials).

If this flag is set (the default), negative clauses in Horn sets receive some special initial processing.
If a Horn set has more than one denial (negative) clause, we assume they correspond to separate conclusions, and the user wishes to have a separate proof of each conclusion. Therefore, if max_proofs has not been changed from its default value of 1, we assign to max_proofs the number of negative clauses. (Note that when reuse_denials is clear (the default), Prover9 prevents multiple proofs of the same conclusion.)
Also, if a negative clause in a Horn set has label attribute but no answer attribute, the clause is given an answer attribute corresponding to the first label attribute. This saves the user from changing "label" to "answer" when moving formulas from the sos list to the goals list.

Forward or Direct Proofs

The following flag restricts the use of negative clauses, with the aim of finding proofs that are more direct; that is, proofs that go forward from the hypotheses to the conclusion rather than proofs that reason backward from the conclusion.

Ordinarily, the term denial refers to a negative clause in a Horn set. Here, we use it for any negative clause. Originally, the flag restrict_denials applied only to Horn sets, but we eliminated that restriction when we realized that it can be useful for non-Horn sets. However, its use has been well analyzed for non-Horn sets.

set(restrict_denials).
clear(restrict_denials).    % default clear

If the flag is set, negative clauses (clauses in which all literals are negative) are referred to as restricted denials and are given special treatment.
The inference rules (i.e., paramodulation and the resolution rules) will not be applied to restricted denials. However, restricted denials will be simplified by back demodulation and back unit deletion.
In addition, restricted denials will not be deleted if they are over the weight limit (max_weight).
The effect of setting restrict_denials is that proofs will usually be more forward or direct. This option can speed up proofs, it can delay proofs, and it can block all proofs.

An Example

The following example illustrates multiple goals (including a goal that is a combination of other goals), auto_denials, and restrict_denials.

prover9 -f olsax.in > olsax.out

Next Section: Production Mode