Function ONE-OF

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

Slots on this function:

Documentation:

ONE-OF is a function for defining classes by enumerating their instances. It takes a variable number of terms as arguments, and denotes the class whose instances are exactly those terms.

For example, (one-of yes no) denotes the class containing the objects called yes or no. (instance-of yes (One-of yes no)) is true, and (instance-of maybe (one-of yes no) is false. A common use for one-of is in defining type restrictions. For example, the relation value-type takes a class as an argument. To specify a finite set of possible values for a slot, one can use (value-type ?instance ?slot (one-of a b c)).

Instance-Of: Function

Equivalence Axioms:

(<=> (One-Of @Members)
     (Forall (?Instance)
             (<=> (Instance-Of ?Instance ?Class)
                  (Member ?Instance (Setof @Members)))))

Axioms:

(Undefined (Arity One-Of))

Other Related Axioms:

(Instance-Of (Arity One-Of) Undefined)

(=> (= (One-Of @Members) ?Class)
    (Forall (?Instance)
            (<=> (Instance-Of ?Instance ?Class)
                 (Member ?Instance (Setof @Members)))))