A subclass-partition of a class C is a set of subclasses of C that are mutually disjoint.
(<=> (Subclass-Partition ?C ?Class-Partition)
(And (Class ?C)
(Class-Partition ?Class-Partition)
(Forall (?Subclass)
(=> (Member ?Subclass ?Class-Partition)
(Subclass-Of ?Subclass ?C)))))
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.