Relation Subclass-Of

Arity: 2
Definition-Sort-Index@Interface-Ontology: 1000
Documentation:
Class C is a subclass of parent class P if and only if every instance of C is also an instance of P. A class may have multiple superclasses and subclasses. Subclass-of is transitive: if (subclass-of C1 C2) and (subclass-of C2 C3) then (subclass-of C1 C3).

Object-centered systems sometimes distinguish between a subclass-of relationship that is asserted and one that is inferred. For example, (subclass-of C1 C3) might be inferred from asserting (subclass-of C1 C2) and (subclass-of C2 C3). The functional interfaces to such systems might call the asserted form something like `parents' and the inferred form `ancestors'. However, both are logically identical to subclass-of; distinctions based on inference procedures and the current state of the knowledge base are not captured in this ontology.

Notes:

  • See-Also: direct-subclass-of
  • See-Also: In CycL, subclass-of is called #%allGenls because it is a slot from a collection to all of its generalizations (superclasses).

    In the KL-ONE literature, subclass relationships are also called subsumption relationships and ISA is sometimes used for subclass-of.

  • Why is it called Subclass-of instead of subclass or superclass?

    Because the latter are ambiguous about the order of their arguments. We are following the naming convention that a binary relationship is read as an english sentence `Domain-element Relation-name Range-value'. Thus, `person subclass-of animal' rather than `person superclass animal'.

Domain: Class
Has-Subrelation: Direct-Subclass-Of
Instance-Of:
Binary-Relation, Binary-Relation, Relation, Relation, Transitive-Relation ...
Inverse: Superclass-Of
Range: Class

Implication Axioms for Subclass-Of:

(=> (Subclass-Of ?Child-Class ?Parent-Class)
    (Forall (?Instance)
            (=> (Instance-Of ?Instance ?Child-Class)
                (Instance-Of ?Instance ?Parent-Class))))


Equivalence Axioms for Subclass-Of:

(<=> (Subclass-Of ?Child-Class ?Parent-Class)
     (And (Class ?Parent-Class)
          (Class ?Child-Class)
          (Forall (?Instance)
                  (=> (Instance-Of ?Instance ?Child-Class)
                      (Instance-Of ?Instance ?Parent-Class)))))


Frame References to Subclass-Of:

In class Universal-Time-Spec@Simple-Time:

Subclass-Of: Time-Point@Simple-Time

In class Complex-Number:

Subclass-Of: Number

In class Negation:

Subclass-Of: Logsent

In class Unary-Relation:

Subclass-Of: Relation

In class Reflexive-Relation:

Subclass-Of: Binary-Relation

In class Many-To-One-Relation:

Subclass-Of: Binary-Relation
...

Implication Axioms mentioning Subclass-Of:

(=> (Inherited-Through-Class-Of-Relation ?R)
    (=> (And (Holds ?R ?X ?C1)
             (Class ?C1)
             (Class ?C2)
             (Subclass-Of ?C2 ?C1))
        (Holds ?R ?X ?C2)))

(=> (Domain ?Relation ?Restriction)
    (Subclass-Of (Exact-Domain ?Relation) ?Restriction))

(=> (Range ?Relation ?Type)
    (Subclass-Of (Exact-Range ?Relation) ?Type))

(=> (Subclass-Partition ?C ?Class-Partition)
    (Forall (?Subclass)
            (=> (Member ?Subclass ?Class-Partition)
                (Subclass-Of ?Subclass ?C))))


Equivalence Axioms mentioning Subclass-Of:

(<=> (Inherited-Through-Class-Of-Relation ?R)
     (And (Binary-Relation ?R)
          (=> (And (Holds ?R ?X ?C1)
                   (Class ?C1)
                   (Class ?C2)
                   (Subclass-Of ?C2 ?C1))
              (Holds ?R ?X ?C2))))

(<=> (Onto ?Relation ?Range-Class)
     (Subclass-Of (Exact-Range ?Relation) ?Range-Class))

(<=> (Domain ?Relation ?Restriction)
     (And (Binary-Relation ?Relation)
          (Class ?Restriction)
          (Subclass-Of (Exact-Domain ?Relation) ?Restriction)))

(<=> (Range ?Relation ?Type)
     (And (Relation ?Relation)
          (Class ?Type)
          (Subclass-Of (Exact-Range ?Relation) ?Type)))

(<=> (Subclass-Partition ?C ?Class-Partition)
     (And (Class ?C)
          (Class-Partition ?Class-Partition)
          (Forall (?Subclass)
                  (=> (Member ?Subclass ?Class-Partition)
                      (Subclass-Of ?Subclass ?C)))))


Axioms mentioning Subclass-Of:

(<= (Instance-Of ?Arg1 ?Class2)
    (And (Instance-Of ?Arg1 ?Class1) (Subclass-Of ?Class1 ?Class2)))

(<= (Subclass-Of Ontolingua-Internal::@Arg-List)
    (Direct-Subclass-Of Ontolingua-Internal::@Arg-List))

(<= (Subclass-Of ?X Integer) (Integer-Range@Ranges ?X))

(<= (Subclass-Of ?X Real-Number) (Real-Range@Ranges ?X))