Relation Can-Be-One-Of

• Defined in ontology: Slot-constraint-sugar
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/ontolingua/../../all-ontologies/ontolingua/slot-constraint-sugar.lisp

Instance-Of: Binary-Relation, Relation, Set

Has-Subrelation: Must-Be-One-Of

Arity: 2

Documentation:

An instance i CAN-BE-ONE-OF a set of classes S iff i is an instance of at most one of the classes. Inside the definition of a class, the form (CAN-BE-ONE-OF ?i (setof C1 C2 ...)) is a convention for stating (subclass-partition class (setof C1 C2 ...)). The two forms are equivalent if each class C1, C2, ... is also defined to be a subclass of C.

Implication Axioms for Can-Be-One-Of:

(=> (Can-Be-One-Of ?Instance ?Set-Of-Classes)
    (Forall (?Class)
            (=> (Member ?Class ?Set-Of-Classes)
                (Instance-Of ?Instance ?Class)
                (Forall (?Other-Class)
                        (=> (Member ?Other-Class ?Set-Of-Classes)
                            (Not (= ?Other-Class ?Class))
                            (Not (Instance-Of ?Instance ?Other-Class)))))))

Equivalence Axioms for Can-Be-One-Of:

(<=> (Can-Be-One-Of ?Instance ?Set-Of-Classes)
     (And (Forall (?Class)
                  (=> (Member ?Class ?Set-Of-Classes) (Class ?Class)))
          (Forall (?Class)
                  (=> (Member ?Class ?Set-Of-Classes)
                      (Instance-Of ?Instance ?Class)
                      (Forall (?Other-Class)
                              (=> (Member ?Other-Class
                                          ?Set-Of-Classes)
                                  (Not (= ?Other-Class ?Class))
                                  (Not (Instance-Of ?Instance
                                                    ?Other-Class))))))))

Axioms for Can-Be-One-Of:

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

Implication Axioms mentioning Can-Be-One-Of:

(=> (Must-Be-One-Of ?Instance ?Set-Of-Classes)
    (Can-Be-One-Of ?Instance ?Set-Of-Classes))

Equivalence Axioms mentioning Can-Be-One-Of:

(<=> (Must-Be-One-Of ?Instance ?Set-Of-Classes)
     (And (Can-Be-One-Of ?Instance ?Set-Of-Classes)
          (Exists (?Class)
                  (And (Member ?Class ?Set-Of-Classes)
                       (Instance-Of ?Instance ?Class)))))

Axioms mentioning Can-Be-One-Of:

(<= (Can-Be-One-Of Ontolingua-Internal::@Arg-List)
    (Must-Be-One-Of Ontolingua-Internal::@Arg-List))