Better support for detecting arity of a relation

[fcbr]

Right now we detect the arity of fixed arity relations by infering it from the domain declarations. For example:

(domain instance 1 Entity)
(domain instance 2 SetOrClass)

From these declarations we can safely infer that instance is a binary operation.

The code that does this is here: https://github.com/own-pt/cl-krr/blob/master/suo-kif.lisp#L248-L254

Unfortunately some relations do not have domain declarations, like superficialPart.

(instance superficialPart TransitiveRelation)
(subclass TransitiveRelation BinaryRelation)

The side effect from this is best explained through an example:

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

When we don't know the arity of a relation, we simply generate all possible arities (up to a certain maximum), see: https://github.com/own-pt/cl-krr/blob/master/suo-kif.lisp#L440-L453

This means that we end up generating something like this:

/*
(FORALL (?VAL ?N ?ARG ?ARGS0)
 (=>
  (AND (INSTANCE ?ARG POSITIVEINTEGER) (INSTANCE ?VAL QUANTITY)
       (INSTANCE ?N QUANTITY))
  (=>
   (AND (MAXVALUE SUPERFICIALPART ?ARG ?N)
        (AND (SUPERFICIALPART ?ARGS0)
             (EQUAL ?VAL (LISTORDERFN (LISTFN1 ?ARGS0) ?ARG))))
   (GREATERTHAN ?N ?VAL))))
*/

Notice the incorrect arity (SUPERFICIALPART ?ARGS0).

While Vampire handles this by assuming that SUPERFICIALPART is overloaded (I guess!), the latest E complains:

s_SUPERFICIALPART used with arity 1, but registered with arity 2

We need to:

1. Either improve our arity inference code;
2. Improve our argument expansion code;
3. Figure out how to convince E to accept this invalid code.

[arademaker]

Line 3570 Merge.kif

(=>
 (instance ?REL BinaryPredicate)
 (valence ?REL 2))

and Line 3237:

(=>
  (and
    (valence ?REL ?NUMBER)
    (instance ?REL Predicate))
  (forall (@ROW)
     (=>
        (?REL @ROW)
        (equal (ListLengthFn (ListFn @ROW)) ?NUMBER))))

these make superficialPart arity 2.

[arademaker]

I am not sure if we can infer from the domain declarations the arity of a predicate. Do we have any check of completeness of domain declarations?

[fcbr]

Do we have any check of completeness of domain declarations?

We don't, and indeed for the domain heuristic to work we have the additional prerequisite that the entire ontology is loaded before emitting TPTP. If we were doing some sort of streaming processing, this wouldn't work.

As for BinaryPredicate and valence, it's not clear how to connect this to the transformation phase yet, but I see that it would help (somehow). There are a few problems that I can see:

1. we are making our transformation more dependent to SUMO that it already is -- ideally we should only know about SUO-KIF, but I guess this is a bigger discussion;
2. SUMO only defines a limited number of *ary relations, where, of course, there could be an arbitrary number of those;
3. It would also need the same prerequisite that the entire ontology is loaded before starting to emit TPTP (which is already the case, so technically not a new problem);

By the way, I'm not sure how to use the ListLengthFn axiom in connection to this.

Boilerplate code

On a more philosophical note: I would say both approaches have one major drawback: they are forcing writers of SUO-KIF ontologies to remember to declare that their predicates are BinaryPredicate, TernaryPredicate, etc., which may be the right thing to do but it starts to smell like "boilerplate" code.

The same argument is valid for having to declare the domain of their arguments as well, of course. Indeed the root cause of this issue is the fact that superficialPart does not have the domain declaration.

[arademaker]

I am not sure about the good practices that @apease adopt. Maybe all relations should have domain declarations.

Regarding (1), suo-kif is minimal , it doesn’t say nothing about the type system nor the upper level hierarchy. The transformation really needs to deal with the sumo axioms.

Item 2 is not a problem, the declarations are for convenience.

[fcbr]

Item 2 is not a problem, the declarations are for convenience.

If they are for convenience, then it looks to me that they are optional, and if they are optional then we can't use them safely to figure out the arity of a predicate, which is the subject of this issue. Is that correct, or did I miss something?

[apease]

all relations do have domain restrictions. The domain statements are either made directly for each relation or inherited from its parent relations

[arademaker]

Hi @apease, so superficialPart is an exception? It can't inherit any domain definition from IrreflexiveRelation, TransitiveRelation, and PartialValuedRelation. Am I right?

TransitiveRelation can't inherit domain definition from Relation and Relation doesn't have domain declaration either.

[apease]

aha we removed the subrelation on superficial part to solve issue ontologyportal/sumo#16 so I need to add domain statements for it, as well as the other relations for which I made this fix. good catch!

[fcbr]

so I guess one improvement that we can make to cl-krr is to list relations for which domain was not set.

[apease]

or run the Sigma Diagnostics function, which already has this