subclass axiom

[arademaker]

In Merge.kif:

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

...

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

During FOL transformation, the domain declarations are used to create the restriction to the axiom but the axiom itself is being defined to properly type the arguments. So the axiom can be irrelevant or there is more on the 'operational semantics' of the implicit type system of SUMO to consider.

[apease]

yes, this axiom is redundant (although harmless)

[arademaker]

and useless! It is reduced to the FOL tautology α → β → α

[nordlow]

Further, isn't also

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

redundant

with

(instance subclass PartialOrderingRelation)

?

But...I can't find any axioms that define the meaning of PartialOrderingRelation.

[arademaker]

@nordlow can you open a new issue about this question about PartialOrderingRelation and the redundancy you are questioning ...

[arademaker]

@nordlow here my opinion:

PartialOrderingRelation does have its semantics defined by the axioms about Reflexive, TotalValue and Transitive.

But this is different of defining what does it means subclass. Say that subclass is PartialOrderingRelation , only says how subclass propagate in the hierarchy of classes.

[arademaker]

Considering that I answered the question. We can close it, issue #190 further discuss the problem that opened this issue