bug in the transformation of row variables

[arademaker]

We have a serious bug in the transformation of the axiom:

(=>
   (exhaustiveDecomposition @ROW)
   (=>
      (inList ?ELEMENT (ListFn @ROW))
      (instance ?ELEMENT Class)))

This axiom is transformed into the following FOL code where ?ROW1 should be the ?CLASS:

/*
(forall (?CLASS ?ROW0 ?ROW1)
 (forall (?OBJ)
  (exists (?ITEM)
   (and (instance ?ITEM SetOrClass)
    (=> (instance ?OBJ Entity)
     (=>
      (and (instance ?ROW0 Entity) (instance ?CLASS SetOrClass)
       (instance ?ROW1 Entity))
      (=> (exhaustiveDecomposition2 ?CLASS ?ROW0)
       (=> (instance ?OBJ ?CLASS)
        (and (inList ?ITEM (ListFn2 ?ROW0 ?ROW1)) (instance ?OBJ ?ITEM))))))))))
*/
fof(a67962,axiom,! [CLASS,ROW0,ROW1] : (! [OBJ] : (? [ITEM] : ((s_instance(ITEM, s_SetOrClass) & (s_instance(OBJ, s_Entity) => ((s_instance(ROW0, s_Entity) & s_instance(CLASS, s_SetOrClass) & s_instance(ROW1, s_Entity)) => (s_exhaustiveDecomposition2(CLASS, ROW0) => (s_instance(OBJ, CLASS) => (s_inList(ITEM, s_ListFn2(ROW0, ROW1)) & s_instance(OBJ, ITEM)))))))))))

[fcbr]

I recommend using save-passes to save each pass of the transformation to help narrow down the bug: https://github.com/own-pt/cl-krr/blob/master/suo-kif.lisp#L641

[arademaker]

The bug in the transformation is a fact. But the axiom above is wrong in SUMO so I have changed it to:

(=>
   (exhaustiveDecomposition ?CLASS @ROW)
   (forall (?OBJ)
      (=>
         (instance ?OBJ ?CLASS)
         (exists (?ITEM)
            (and
               (inList ?ITEM (ListFn @ROW))
               (instance ?OBJ ?ITEM))))))

But we still have clearly a bug, see the extra row2 variable below:

/*
(forall (?ROW1 ?ROW0 ?CLASS ?ROW2)
 (forall (?OBJ)
  (exists (?ITEM)
   (and (instance ?ITEM SetOrClass)
    (=> (instance ?OBJ Entity)
     (=>
      (and (instance ?CLASS SetOrClass) (instance ?CLASS Class)
       (instance ?ROW1 Class) (instance ?ROW1 Entity) (instance ?ROW0 Class)
       (instance ?ROW0 Entity) (instance ?ROW2 Entity))
      (=> (exhaustiveDecomposition3 ?CLASS ?ROW0 ?ROW1)
       (=> (instance ?OBJ ?CLASS)
        (and (inList ?ITEM (ListFn3 ?ROW0 ?ROW1 ?ROW2))
         (instance ?OBJ ?ITEM))))))))))
*/
fof(a67115,axiom,! [ROW1,ROW0,CLASS,ROW2] : (! [OBJ] : (? [ITEM] : ((s_instance(ITEM, s_SetOrClass) & (s_instance(OBJ, s_Entity) => ((s_instance(CLASS, s_SetOrClass) & s_instance(CLASS, s_Class) & s_instance(ROW1, s_Class) & s_instance(ROW1, s_Entity) & s_instance(ROW0, s_Class) & s_instance(ROW0, s_Entity) & s_instance(ROW2, s_Entity)) => (s_exhaustiveDecomposition3(CLASS, ROW0, ROW1) => (s_instance(OBJ, CLASS) => (s_inList(ITEM, s_ListFn3(ROW0, ROW1, ROW2)) & s_instance(OBJ, ITEM))))))))))).

[arademaker]

moreover, universal and existential row variables should have different transformations. Consider

(instance foo VariableArityRelation)
(forall (@row) (foo @row))
(exists (@row) (foo @row))

The intuition is that universal means:

(AND (foo0)
    (forall (?x1)(foo1 ?x1))
    (forall (?x1 ?x2)(foo2 ?x1 ?x2))
    (forall (?x1 ?x2 ?x3) (foo3 ?x1 ?x2 ?x3))
    ...)

But existential should be

(OR (foo0)
    (exists (?x1)(foo1 ?x1))
    (exists (?x1 ?x2)(foo2 ?x1 ?x2))
    (exists (?x1 ?x2 ?x3) (foo3 ?x1 ?x2 ?x3))
   ...)

Of course, the AND resulting axiom can be split into top-level axioms of the theory, but not the OR. These intuitions are actually made formal by http://www.w3c.hu/forditasok/RDF/cached/HayesMenzel-SKIF-IJCAI2001.pdf.