The Inference Loop

The main loop for inferring and processing clauses and searching for a proof is sometimes called the given clause algorithm. It operates mainly on the sos and usable lists.

While the sos list is not empty:
    1. Select a given clause from sos and move it to the usable list;
    2. Infer new clauses using the inference rules in effect;
       each new clause must have the given clause as one of its
       parents and members of the usable list as its other parents;
    3. process each new clause;
    4. append new clauses that pass the retention tests to the sos list.
end of while loop.

Two Frequently Asked Questions

At some point in the search, Prover9 has all of the clauses needed to make an important inference, and one of the potential parents is selected as the given clause. But Prover9 fails to make the inference. Why is that?

Why do all parents have to be in the usable list?

The answer to both questions is the same, and it has to do with redundancy. Assume

clause C can be inferred from clauses A and B;
both A and B are in the sos list; and
A is selected first.

According to the algorithm, C is not derived until B has also been selected. Otherwise, C would be derived twice from A and B.

Variations of the Loop

There are two common versions of the given clause algorithm that differ in how and when simplification (i.e., rewriting) occurs.

In the Otter loop, which Prover9 uses, clauses in the sos list can simplify new clauses, and new simplifiers are applied immediately to all clauses, including sos clauses.

In the Discount loop, clauses in the sos list (also called the passive list) cannot simplify or be simplified until they are selected as given clauses.

The tradeoff between the two versions is straightforward --- the Otter loop spends much more time simplifying with the possible benefit of making an important simplification sooner.

Next Section: Select Given