bug transformation subclass

[arademaker]

The original axiom could be used to type the arguments, but the translation turns this axiom useless.

(=>
  (subclass ?X ?Y)
  (and
    (instance ?X SetOrClass)
    (instance ?Y SetOrClass)))

/*
(forall (?Y ?X)
 (=> (and (instance ?Y SetOrClass) (instance ?X SetOrClass))
  (=> (subclass ?X ?Y)
   (and (instance ?X SetOrClass) (instance ?Y SetOrClass)))))
*/
fof(a14,axiom,! [Y,X] : (((s_instance(Y, s_SetOrClass) & s_instance(X, s_SetOrClass)) 
 => (s_subclass(X, Y) => (s_instance(X, s_SetOrClass) & s_instance(Y, s_SetOrClass)))))).

[arademaker]

It looks like there is no easy way to prove that ins Vertebrate Class from ins Vertebrate SetOrClass. The axioms from subclass have the types as conditions.

We have (partition SetOrClass Set Class) but we don't have ways to say that something is not a Set.

It looks like the only way is to show that is using the axiom below and showing that it is a subclass of Entity:

(<=>
    (instance ?CLASS Class)
    (subclass ?CLASS Entity))

But for that, I will need to use the fact that subclass is a PartialOrderingRelation

[arademaker]

This is actually already identified in #1 by @fcbr

[arademaker]

The question is how we should interpret the axioms below:

(instance subclass BinaryPredicate)
(instance subclass PartialOrderingRelation)
(domain subclass 1 SetOrClass)
(domain subclass 2 SetOrClass)
...

(=>
  (subclass ?X ?Y)
  (and
    (instance ?X SetOrClass)
    (instance ?Y SetOrClass)))

See ontologyportal/sumo#181