1. About yieldingproof with yielding and limiting eigenvariables ∃

To illustrate these heuristic search strategies, consider the following simple geolog theory forever1. (Save a clip of the following code to file forever1.gl.)
%forever1.gl

true => a < b.

X < Y => Y < Z.

A < B, B < C, C < D, D < E => goal.
This theory is not optimally ordered (see below), but it will serve as a simple example where yielding can be effective. Start GeologUI, and load forever1 . Hit the run button ..

infinite descent
Figure 1. Yielding OFF

One can inspect the inference tree on the left and realize that the second rule in forever1 repeatedly fires to produce an endless sequence of new geolog eigenvariables (a.k.a. Skolem constants sk_i).

Turn on yielding proof with yielding and one gets a proof:

infinite descent
Figure 2. Yielding ON

Yielding/1 means that each rule can fire exactly once before yielding to subsequent rules, in the order that the rules appear in the theory panel. In effect this limits the second rule to be fired once before yielding to the third rule. Once a rule has yielded, and there has been a resulting inference from some subsequent rule, the yielding restriction is rescinded and the rule is allowed to fire again, and the yielding continues again. Thus the second rule was allowed to fire three times, yielding between, until goal was achieved.

For another experiment, turn off yielding control and set the limit button on generating new eigenvariables (∃ on toolbar) using a limit of 3. This also easily produces a proof when run. Why?

Consider another version of the theory, forever2

% forever2.gl
true => a < b.
A < B, B < C, C < D, D < E => goal.
X < Y => Y < Z.

The reader can easily check that this version, with the original second and third rules exchanged, easily leads to a proof, since the goal rule checks before any new individuals are generated.

In general, for improved results, geolog rules should be ordered so that goal rules come before existential rules and existential rules come before splitting rules. This is, however, not a guarantee for termination when there is a proof.

Exercise. Show that yielding can introduce incompleteness. That is, a geolog theory may have a proof with yielding off, but fail to prove with yielding turned on. Find such a geolog theory.