Class CLASS-PARTITION

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

Slots on this class:

Documentation:

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

Instance-Of: Class

Subclass-Of: Set

Range-Of: Subclass-partition

Equivalence 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))))))))

Axioms:

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

(Forall (?C) (=> (Member ?C ?Set-Of-Classes) (Class ?C)))

(Set ?Set-Of-Classes)

Other Related 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))))))))

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

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

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.