Prover9 Manual Version June-2006

Goals

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.

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 lists clauses(goals) and 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.

If there is just one clause in clauses(goals), the meaning is clear, and the clause is processed by taking first taking 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.

If there is just one formula in formulas(goals), the meaning is clear, and it is simply negated and then Skolemized as usual.

If there is more than one clause in clauses(goals) or more than one formula in formulas(goals), the meaning is not clear. For example, if there are two clauses in clauses(goals), is the conclusion the disjunction or the conjunction of those clauses? What does a list of goal clauses mean if some of them are non-units or non-positive?

To simplify the meanings of multiple goals, the following restrictions are in place.

To avoid any of these restrictions, one can always write the conclusions clearly as a single formula for formulas(goals).

When there are multiple goals in clauses(goals), should the proofs of the goals be presented together as one proof or as separate proofs? We have chosen the latter for the simple reason that if any goal is proved, we wish to have a proof.

Forward or Direct Proofs

This subsection refers to the negative clauses that exist at the start of the search. These include ones that are input, ones that are derived from ordinary Skolemization, and those that are derived from clauses(goals) and formulas(goals).

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. The secondary effect of this flag is that when there are multiple conclusions, Prover9 will not give more than one proof of the same conclusion.

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

If this flag is set, negative clauses (clauses in which all literals are negative) are given special treatment. At the start of the search, they are moved to a list denials, and during the search, only a subset of the ordinary operations are applied to them.

The clauses will not be selected as given clauses, so the ordinary inference rules of the search will not be applied to them. The following operations will be applied to the clauses: back demodulation, back unit deletion, unit conflict.

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.

In addition, when a clause in list denials is used in a proof, it is disabled (unless the flag reuse_denials is set). When multiple proofs are sought (see max_proofs), this prevents more than one proof of the same theorem.

Handling Multiple Conclusions

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. If the user asks for more than one proof by changing this parameter, the flag restrict_denials will be automatically set. This option dependency prevents multiple proofs of the same theorem.

Note that the flag restrict_denials can substantially alter the search, so one must be aware of situations like the following. One runs a job that finds a quick proof of a single goal; then a second job is run, containing a second goal and also assign(max_proofs,2); the first goal may no longer be proved, because the first proof has bidirectional reasoning which is not allowed by restrict_denials.

Of course, the option dependency can be undone with clear(restrict_denials).

Multiple Proofs of the Same Conclusion

If the flag restrict_denials is set, and if there are multiple denials, then by default, when a denial is refuted, it is disabled so that it is not refuted again later in the search. The following flag allows for multiple refutations using the same denial.
set(reuse_denials).
clear(reuse_denials).    % default clear
If this flag is set, when a clause in list denials (which gets there by flag restrict_denials), occurs in a proof, it is not disabled, allowing it to occur in subsequent proofs.