Examples regarding the interplay between disjuction and rule order for colog14I

8/1/2023

These notes involve some details regarding how colog14I deals with rule order in the presence of a disjunctive rule, using some very simple examples. The note arose to inform students on background information about how to make rule order more predictable and manageable for the AutoLog system, which is currently under development. There appears to be a quandry: Do the examples reveal a bug in colog14I source code or an issue to be resolved by more careful input theory editing? The examples ameliorate the problem using input theory editing, but a better solution amounts to a Java source code bug fix, and suggestions for that are given at the end of this note. The examples using source theory editing provide crucial clues regarding a code bug fix.

Example A 

    true => p | q.  % ruleA1
    true => p.      % ruleA2
    p => goal.      % ruleA3
Using the colog GUI, this theory generated the following inference tree
Note that ruleA2 is not actionable for the prover along the left branch of the inference tree since the consequent p already occurs at branch[1] for the left branch of the inference tree. If we turn on the inspect table switch under the options menu and enter branch 1 before running the prover, we get the following report written to the console tab pane: 
   AutoLog Analyzer index report
   Functors & predicates by index
   0 : true   keys=<[]>
   1 : goal   keys=<[]>
   2 : false    
   3 : p   keys=<[]>
   4 : q   keys=<[]>
   
   table @ leaf 1: 
   0: [0f]   true@branch[0]
   1: [2f]   goal@branch[2]
   2: []
   3: [1f]   p@branch[1]
   4: []
   5: []

   table @ leaf 2: 
   0: [0f]   true@branch[0]
   1: []
   2: []
   3: []
   4: [1f]   q@branch[1]
   5: []
Using the analysis data, why exactly is it that the inference engine cannot apply ruleA2 to the right branch? See below for a summary.
exercise
Example B. Modify ExampleA so that it looks like this: 
    true => p | q.  % ruleB1
    true => p.      % ruleB2
    p => goal.      % ruleB3
    true => p.      % ruleB4
Using the colog GUI, this theory generated the following inference tree
and then perform similar experiments to that illustrated above for Example A. Explain how the proof is achieved.
exercise
Example C. Modify ExampleA so that it looks like this: 
    true => p | q.  % ruleC1
    p => goal.      % ruleC2
    true => p.      % ruleC3
Using the colog GUI, this theory generated the following inference tree
and then perform similar experiments to that illustrated above. Explain how the proof is achieved.
The issue of the input rule/rewrite order for the logic source code is being rexamined for the pending implementation of AutoLog with a Skolem Machine. The input theories used above suggest the following source code mofification details for the colog14I application.

A. The hash table inspections for A imply that RuleA2 is blocked on the 2nd branch (p makes no appearance on that branch). The apply() method for ActiveDCRule.java uses a start instance variable to test whether it sould fire (first time or repeat). The first attempt to apply() RuleA2 fails (because of p at node 1) and that sets the start instance variable to false. When the prover switches to the right branch a rollBack method realigns antecedent rule choices if needed, but at present the start variable is NOT reset to true for the new branch and so ruleA2 acts as if it is turned off (cannot apply()). A detailed restricted code fix confirms this intuition, but needs to be more carefully coded and tested for unwanted bad side effects.

B. Considering the comments just given for A, RuleB2 fails and is blocked from apply() on the right branch. However, RuleB3 finished off the 1st branch and RuleB4 is NOT even attempted, so it is ready to apply() on the 2nd branch, etc.

C. The order position of RuleC3 in the input theory order leaves it avaiable to apply() on the second branch, thus giving the proof similarly to version B.

Resolution of the quandry (10/6/2023) only required small modification of the rollBack (Ver.3) method for sam/infer/ActiveDCRule.java. It appears to have been an oversight when the original code was writen, but was not noticed until recently.