Relation SUBCLASS-OF

Slots on this relation:

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.

Instance-Of: Relation
Arity: 2
Domain: Class
Range: Class

Equivalence Axioms:

(<=> (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)))))

Other Related Axioms:

(Subclass-Of Class Relation)

(Subclass-Of Individual-Thing Individual)

(Subclass-Of Individual-Thing Thing)

(=> (And (Holds ?R ?X ?C1) (Subclass-Of ?C1 ?C2)) (Holds ?R ?X ?C2))

(Subclass-Of Inherited-Through-Class-Of-Relation Binary-Relation)

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

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

(<= (Subclass-Of $Arg1 $Arg3)
    (And (Subclass-Of $Arg1 $Arg2) (Subclass-Of $Arg2 $Arg3)))

(=> (Subclass-Of $X $Y) (Class $X))

(=> (Subclass-Of $X $Y) (Class $Y))

(<=> (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)))))

(<=> (Superclass-Of $Arg1 $Arg2) (Subclass-Of $Arg2 $Arg1))

(Inverse Superclass-Of Subclass-Of)

(=> (Direct-Instance-Of ?Individual ?Class)
    (<= (Not (Exists (?Other-Class)
                     (And (Not (= ?Other-Class ?Class))
                          (Instance-Of ?Individual ?Other-Class)
                          (Subclass-Of ?Other-Class ?Class))))
        (Not (Provable (Not (Not (Exists (?Other-Class)
                                         (And (Not (= ?Other-Class
                                                      ?Class))
                                              (Instance-Of 
                                                  ?Individual
                                                  ?Other-Class)
                                              (Subclass-Of 
                                                  ?Other-Class
                                                  ?Class)))))))))

(Subrelation-Of Direct-Subclass-Of Subclass-Of)

(=> (Direct-Subclass-Of ?Child-Class ?Parent-Class)
    (<= (Not (Exists (?Other-Class)
                     (And (Not (= ?Other-Class ?Child-Class))
                          (Not (= ?Other-Class ?Parent-Class))
                          (Subclass-Of ?Child-Class ?Other-Class)
                          (Subclass-Of ?Other-Class ?Parent-Class))))
        (Not (Provable (Not (Not (Exists (?Other-Class)
                                         (And (Not (= ?Other-Class
                                                      ?Child-Class))
                                              (Not (= ?Other-Class
                                                      ?Parent-Class))
                                              (Subclass-Of 
                                                  ?Child-Class
                                                  ?Other-Class)
                                              (Subclass-Of 
                                                  ?Other-Class
                                                  ?Parent-Class)))))))))

(<=> (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-Of Class-Partition Set)

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

(Subclass-Of Symmetric-Relation Binary-Relation)

(Subclass-Of Antisymmetric-Relation Binary-Relation)

(Subclass-Of Asymmetric-Relation Irreflexive-Relation)

(Subclass-Of Asymmetric-Relation Antisymmetric-Relation)

(Subclass-Of Reflexive-Relation Binary-Relation)

(Subclass-Of Irreflexive-Relation Binary-Relation)

(Subclass-Of Transitive-Relation Binary-Relation)

(Subclass-Of Weak-Transitive-Relation Binary-Relation)

(Subclass-Of One-To-One-Relation Unary-Function)

(Subclass-Of Many-To-One-Relation Function)

(Subclass-Of Many-To-One-Relation Binary-Relation)

(Subclass-Of One-To-Many-Relation Binary-Relation)

(Subclass-Of Many-To-Many-Relation Binary-Relation)

(Subclass-Of Equivalence-Relation Transitive-Relation)

(Subclass-Of Equivalence-Relation Symmetric-Relation)

(Subclass-Of Equivalence-Relation Reflexive-Relation)

(Subclass-Of Partial-Order-Relation Transitive-Relation)

(Subclass-Of Partial-Order-Relation Asymmetric-Relation)

(Subclass-Of Partial-Order-Relation Reflexive-Relation)

(Subclass-Of Total-Order-Relation Partial-Order-Relation)

Notes: