Geolog Experiments

4. About limiting splitting rules per branch ∨

This example is borrowed from Marc Bezem. Newman's Lemma in rewriting theory states that a rewrite relation is confluent if it is terminating and locally confluent. Huet's proof is by well-founded induction. We prove the induction step in this experiment.

Load the following geolog theory into GeologUI.

% nlA.gl INDUCTION STEP IN NEWMAN's LEMMA true => exists(a), exists(b), exists(c). s(b,X),s(c,X) => goal. true => s(a,b),s(a,c). exists(X) => e(X,X). e(X,Y) => e(Y,X). e(X,Y) => s(X,Y). r(X,Y) => s(X,Y). s(X,Y),s(Y,Z) => s(X,Z). r(X,Y),r(X,Z) => exists(U),s(Y,U),s(Z,U). r(a,X),s(X,Y),s(X,Z) => exists(U),s(Y,U),s(Z,U). s(X,Y) => e(X,Y) | exists(Z),r(X,Z),s(Z,Y).

The theory as given yields a nice proof. The ordering of the last two rules is a sensitive issue.

Let us investigate what happens when the last two rules are switched.

% nlB.gl INDUCTION STEP IN NEWMAN's LEMMA true => exists(a), exists(b), exists(c). s(b,X),s(c,X) => goal. true => s(a,b),s(a,c). exists(X) => e(X,X). e(X,Y) => e(Y,X). e(X,Y) => s(X,Y). r(X,Y) => s(X,Y). s(X,Y),s(Y,Z) => s(X,Z). r(X,Y),r(X,Z) => exists(U),s(Y,U),s(Z,U). s(X,Y) => e(X,Y) | exists(Z),r(X,Z),s(Z,Y). r(a,X),s(X,Y),s(X,Z) => exists(U),s(Y,U),s(Z,U).

Save a clip of nlB.gl to file and load it into GeologUI. With all heuristic controls off, attempt to achieve a proof. Stepping through inferences should convince the experimenter that switching the last two rules allows repeated opportunities for the splitting rule, which was move up in preference, to fire using new Skolem constants which are introduced in the second choice of the consequent of the splitting rule. This is a very subtle inference effect. The reader can verify that yielding

does NOT mitigate the effect.

A reasonable hypothesis to counter this subtle effect would be to limit the number of applications of splitting for each branch. The original proof was achieved with only 2 splits per branch. Let us try that restriction, ∨(2) on the toolbar.

This ploy produces essentially the same proof as we achieved for nlA.gl!