Class Class-Partition

• Defined in ontology: Frame-ontology
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/ontolingua/../../all-ontologies/ontolingua/frame-ontology.lisp

Arity: 1

Documentation:

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

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.

Instance-Of: Class, Relation, Set

Range-Of: Subclass-Partition

Subclass-Of: Set

---

Slots:

Implication Axioms for Class-Partition:

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

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

Equivalence Axioms for Class-Partition:

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

Equivalence Axioms mentioning Class-Partition:

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