Relation MUST-BE-ONE-OF

• Defined in theory: Slot-constraint-sugar
• Source code: slot-constraint-sugar.lisp

Slots on this relation:

Documentation:

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

Arity: 2

Subrelation-Of: Can-be-one-of

Axioms:

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