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