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 organizes 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 ambiguous and 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.

Forward or Direct Proofs

The following flag restricts the use of negative clauses in Horn sets, 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.

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

This flag applies only to Horn sets. If it is set, negative clauses (clauses in which all literals are negative) are given special treatment.
Paramodulation will not be applied to negative clauses. (However, negative clauses will be simplified by back demodulation and back unit deletion.) In addition, negative clauses will always receive the weight 0, so that they will (usually) not be deleted by the weight limit. A side effect of the weight of 0 is that negative clauses will usually be selected right away as given clauses.
The effect of setting restrict_denials is that proofs involving equality will usually be more forward or direct. This option can speed up proofs, it can delay proofs, and it can block all proofs.

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 search for short proofs.)
If this flag is clear, denials and all of their 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.

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