TFO transformation of minValue

[arademaker]

This axiom is ignored in the tf0 and fof transformations:

(=>
  (and
    (minValue ?R ?ARG ?N)
    (?R @ARGS)
    (equal ?VAL (ListOrderFn (ListFn @ARGS) ?ARG)))
  (greaterThan ?VAL ?N))

why?

Related to ontologyportal/sumo#160

[apease]

I'm not sure. It should get expanded with row variable substitution and predicate instantiation, at which point it will be strictly first order and should get translated to TFF0 and TPTP. We'd have to run some tests to find out what's wrong. Thanks for spotting this

[arademaker]

Actually, we found that the axiom is not ignored but only 1 substitution was done for the predicate variable:

% f: (=> (and (minValue ?R ?ARG ?N) (instance ?R Predicate) (?R @ARGS) (equal ?VAL (ListOrderFn (ListFn @ARGS) ?ARG))) (greaterThan ?VAL ?N))
% 937 of 34586 from file /Users/ar/workspace/sumo/Merge.kif at line 18756
% not higher order
tff(kb_SUMO_647,axiom,(! [V__ARG : $int,V__ARGS1 : $i,V__N : $i,V__VAL : $i] : (s__instance(V__ARGS1, s__Attribute) => (s__minValue__2In(s__contraryAttribute__m, V__ARG, V__N) & s__instance(s__contraryAttribute__m, s__Predicate) & s__contraryAttribute_1(V__ARGS1) & equal(V__VAL ,s__ListOrderFn__2InFn(s__ListFn_1(V__ARGS1), V__ARG))) => greaterThan(V__VAL ,V__N)))).

So the transformation is clearly incomplete.

[apease]

hmm, PredVarInst is creating the hundreds of right substitutions (see below) but somehow they're not making it to the TFF0 conversion step, investigating further...

(and
(minValue KiloFn ?ARG ?N)
(KiloFn @Args)
(equal ?VAL
(ListOrderFn
(ListFn @Args) ?ARG)))
(greaterThan ?VAL ?N)),

(=>
(and
(minValue ImmediatePastFn ?ARG ?N)
(ImmediatePastFn @Args)
(equal ?VAL
(ListOrderFn
(ListFn @Args) ?ARG)))
...

[apease]

resolved the issue of expansion and implemented some speedups since the row variable expansion was too slow, but now verifying whether it works as intended