Relation Subclass-Partition

Arity: 2
Definition-Sort-Index@Interface-Ontology: 800
Documentation:
A subclass-partition of a class C is a set of subclasses of C that are mutually disjoint.

Notes:

  • Why is the second argument a set, rather than a sequence variable?

    Interesting design choice. The ``notation'' question here is not new syntax for a language, it's just the definition of a particular relation called subclass-partition. In KIF you can define relations that take an arbitrary number of arguments, using a a "sequence variable" that acts like &rest in Lisp. So I could have made the subclass-partition relation take a variable number of arguments. I decided not to use a sequence variable because that is not a minimal ontological commitment; it imposes an extra logical constraint for the sake of syntactic convenience. A sequence (list) imposes an order. But a class-partition requires no order among the classes. And I wanted the second argument to subclass-partition to be a class-partition -- a thing that is defined independently as a set of classes.

Domain: Class
Has-Subrelation: Exhaustive-Subclass-Partition
Instance-Of:
Binary-Relation, Binary-Relation, Relation, Relation, Relation ...
Range: Class-Partition

Implication Axioms for Subclass-Partition:

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

Equivalence Axioms for Subclass-Partition:

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

Axioms for Subclass-Partition:

(Class-Partition ?Class-Partition)

Frame References to Subclass-Partition:

In class Agent@Agents:

Subclass-Partition: {Organization@Agents, Person@Agents}

Implication Axioms mentioning Subclass-Partition:

(=> (Exhaustive-Subclass-Partition ?C ?Class-Partition)
    (Subclass-Partition ?C ?Class-Partition))

Equivalence Axioms mentioning Subclass-Partition:

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

Axioms mentioning Subclass-Partition:

(<= (Subclass-Partition Ontolingua-Internal::@Arg-List)
    (Exhaustive-Subclass-Partition Ontolingua-Internal::@Arg-List))