search

own-pt / cl-krr

Environment for knowledge representation, reasoning, and engineering.
Apache License 2.0
4 stars 3 forks source link

bug transformation subclass #24

Open arademaker opened 5 years ago

arademaker commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

This is actually already identified in #1 by @fcbr

arademaker commented 5 years ago

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 https://github.com/ontologyportal/sumo/issues/181