Class CLASS-PARTITION

A set of mutually disjoint classes. Disjointness of classes is a special case of disjointness of sets.

Subclass-Of: Set

Axioms:

(<=> (Class-Partition ?Set-Of-Classes)
     (And (Set ?Set-Of-Classes)
          (Forall (?C) (=> (Member ?C ?Set-Of-Classes) (Class ?C)))
          (Forall (?C1 ?C2)
                  (=> (And (Member ?C1 ?Set-Of-Classes)
                           (Member ?C2 ?Set-Of-Classes)
                           (Not (= ?C1 ?C2)))
                      (Forall (?I)
                              (=> (Instance-Of ?I ?C1)
                                  (Not (Instance-Of ?I ?C2))))))))

• Defined in theory: Frame-ontology
• Source code: frame-ontology.lisp

Notes:

• Why not just use the set machinery?

  We want to localize the relationship between sets and classes to just a few axioms, so we use the instance-of machinery here.