axioms domain/range

[arademaker]

We do not generate fof axioms for the domain/range declarations, but we do generate axioms that mention domain and range predicates:

Original axiom:

(domain maxValue 1 Relation)
(domain maxValue 2 Integer)
(domain maxValue 3 Quantity)

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

our transformation:

/*
(FORALL (?VAL ?N ?ARG ?ARGS0 ?ARGS1 ?ARGS2)
 (=>
  (AND (INSTANCE ?ARGS1 POSITIVEINTEGER) (INSTANCE ?ARG POSITIVEINTEGER)
       (INSTANCE ?VAL QUANTITY) (INSTANCE ?N QUANTITY)
       (INSTANCE ?ARGS0 RELATION) (INSTANCE ?ARGS2 SETORCLASS))
  (=>
   (AND (MAXVALUE DOMAIN ?ARG ?N)
        (AND (DOMAIN ?ARGS0 ?ARGS1 ?ARGS2)
             (EQUAL ?VAL (LISTORDERFN (LISTFN3 ?ARGS0 ?ARGS1 ?ARGS2) ?ARG))))
   (GREATERTHAN ?N ?VAL))))
*/
fof(a72251,axiom,! [VAL,N,ARG,ARGS0,ARGS1,ARGS2] : (((s_INSTANCE(ARGS1, s_POSITIVEINTEGER) & s_INSTANCE(ARG, s_POSITIVEINTEGER) & s_INSTANCE(VAL, s_QUANTITY) & s_INSTANCE(N, s_QUANTITY) & s_INSTANCE(ARGS0, s_RELATION) & s_INSTANCE(ARGS2, s_SETORCLASS)) => ((s_MAXVALUE(s_DOMAIN_m, ARG, N) & (s_DOMAIN(ARGS0, ARGS1, ARGS2) & (VAL = s_LISTORDERFN(s_LISTFN3(ARGS0, ARGS1, ARGS2), ARG)))) => greater(N, VAL))))).

it doesn't make sense. Some relations are not candidates to substitute variable in a predicate position.

[arademaker]

Moreover, some substitutions (in particular cases) doesn't trivialize the theory but doesn't make sense either , for example, the subclass for this same axiom never will have a numeric argument

(FORALL (?VAL ?N ?ARG ?ARGS1 ?ARGS0)
 (=>
  (AND (INSTANCE ?ARGS1 SETORCLASS) (INSTANCE ?N QUANTITY)
       (INSTANCE ?VAL QUANTITY) (INSTANCE ?ARG POSITIVEINTEGER)
       (INSTANCE ?ARGS0 SETORCLASS))
  (=>
   (AND (MAXVALUE SUBCLASS ?ARG ?N)
        (AND (SUBCLASS ?ARGS0 ?ARGS1)
             (EQUAL ?VAL (LISTORDERFN (LISTFN2 ?ARGS0 ?ARGS1) ?ARG))))
   (GREATERTHAN ?N ?VAL))))

[arademaker]

@apease doesn't transform these axioms in his fof translation. See https://github.com/ontologyportal/sigmakee/issues/38

[fcbr]

Sorry I think I missing something... can you mention explicitly which:

axioms for the domain/range declarations

we are not generating?

As for your second comment, yes I see that right now all we do is check for the arity to expand the variable. We should probably check the types of the arguments and thus avoid generating those spurious axioms that would never hold due to type differences.

[arademaker]

Hi @fcbr , our transformation does not transform the top level declarations (domain ...). The @apease code also omit these declarations:

% f: (domain wears 1 Animal)
% 3954 of 13092 from file /Users/ar/.sigmakee/KBs/Merge.kif at line 16027
% not higher order
% filtered predicate

[apease]

in Sigma's TPTP and TFF0 translations we don't need to translate the domain statements explicitly because their semantics is captured as type guards on implications. So

(domain baz 1 Foo)

(=>
  (baz ?X ?Y)
  (bar ?Y ?X))

becomes

(=>
  (instance ?X Foo)
  (=>
      (baz ?X ?Y)
      (bar ?Y ?X)))

[arademaker]

Yes, it is the right thing to do. But my problem is how we are transforming the axiom about the maxValue, we are producing a (domain ...) atomic formula in the middle of the implication and the tptp will know nothing about the (domain ...) predicates.

[apease]

why are you producing a domain statement?

[fcbr]

It's because we are expanding the variable in the predicate position combined with row expansion.

Using @arademaker's example above:

(?R @ARGS)

will be used as a template to generate all possible values for ?R, including domain, eg.:

(DOMAIN ?ARGS0 ?ARGS1 ?ARGS2)

[apease]

yes, but that's not needed since any relation substituted in for the row variable will already have a domain declaration

[arademaker]

@apease, my question is, in your code, do you have a fixed list of filtered predicates? It looks like the list is this one:

https://github.com/ontologyportal/sigmakee/blob/master/src/java/com/articulate/sigma/trans/SUMOKBtoTPTPKB.java#L35-L45

right? why range is not on your list above? Output of @apease code

% f: (range AdditionFn Quantity)
% 8473 of 13092 from file /Users/ar/.sigmakee/KBs/Merge.kif at line 4849
% not higher order
fof(kb_SUMO_3221,axiom,(( s__range(s__AdditionFn__m,s__Quantity) ))).

[apease]

yes that looks the right list and I agree that although it's harmless to generate an fof() for range that could be excluded too

[fcbr]

For cl-krr, the list is https://github.com/own-pt/cl-krr/blob/master/suo-kif.lisp#L19-L23

So I think the bug fix would be to use this list (by way of the EXCLUDED-PREDICATE-P function) when expanding variables in the predicate position here: https://github.com/own-pt/cl-krr/blob/master/suo-kif.lisp#L313-L358

[arademaker]

We need also to add range in our list.

[hmuniz]

The problem is not only with the axioms generated by expanding predicate variables. For example, the following axiom: https://github.com/ontologyportal/sumo/blob/b3c95dbb1f8ab932d836154a536228f22e8ad257/Merge.kif#L207-L211

Our code generates the following:

/*
(FORALL (?PRED1 ?NUMBER ?CLASS1 ?PRED2)
 (=>
  (AND (INSTANCE ?CLASS1 SETORCLASS) (INSTANCE ?PRED1 RELATION)
       (INSTANCE ?NUMBER POSITIVEINTEGER) (INSTANCE ?PRED2 RELATION))
  (=> (AND (SUBRELATION ?PRED1 ?PRED2) (DOMAIN ?PRED2 ?NUMBER ?CLASS1))
   (DOMAIN ?PRED1 ?NUMBER ?CLASS1))))
*/
fof(a22,axiom,! [PRED1,NUMBER,CLASS1,PRED2] : (((s_INSTANCE(CLASS1, s_SETORCLASS) & s_INSTANCE(PRED1, s_RELATION) & s_INSTANCE(NUMBER, s_POSITIVEINTEGER) & s_INSTANCE(PRED2, s_RELATION)) => ((s_SUBRELATION(PRED1, PRED2) & s_DOMAIN(PRED2, NUMBER, CLASS1)) => s_DOMAIN(PRED1, NUMBER, CLASS1)))))

[arademaker]

Good @hmuniz! The @apease code also produces a fof axiom for this SUMO axiom:

% f: (=> (and (subrelation ?PRED1 ?PRED2) (domain ?PRED2 ?NUMBER ?CLASS1)) (domain ?PRED1 ?NUMBER ?CLASS1))
% 417 of 13092 from file /Users/ar/.sigmakee/KBs/Merge.kif at line 209
% not higher order
fof(kb_SUMO_306,axiom,(( ( ! [V__CLASS1,V__PRED2,V__NUMBER,V__PRED1] : ((s__instance(V__CLASS1,s__SetOrClass) & s__instance(V__PRED2,s__Relation) & s__instance(V__NUMBER,s__PositiveInteger) & s__instance(V__PRED1,s__Relation)) => ((s__subrelation(V__PRED1,V__PRED2) & s__domain(V__PRED2,V__NUMBER,V__CLASS1)) => s__domain(V__PRED1,V__NUMBER,V__CLASS1))) ) ))).

Having an axiom mentioning the domain predicate doesn't seem consistent with the decision of filtering the domain axioms from the TPTP output. does it make sense @apease ?