Function VALUE-CARDINALITY

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

Slots on this function:

Documentation:

The VALUE-CARDINALITY of a binary-relation with respect to a given domain instance is the number of range-elements to which the relation maps the domain-element. For a function (single-valued relation), the VALUE-CARDINALITY is 1 on all domain instances for which the function is defined. It is 0 for those instances outside the exact domain of the function.

VALUE-CARDINALITY may be used within the definition of a class to specify a slot cardinality if its first argument is the class's instance variable.

Instance-Of: Function

Arity: 3

Axioms:

(Nth-Domain Value-Cardinality 3 Nonnegative-Integer)

(Nth-Domain Value-Cardinality 2 Binary-Relation)

Other Related Axioms:

(<- (Value-Cardinality ?Instance ?Binary-Relation)
    (Cardinality (Setofall ?Y (Holds ?Binary-Relation ?Instance ?Y))))

(<=> (Minimum-Value-Cardinality ?Instance ?Binary-Relation ?N)
     (And (Binary-Relation ?Binary-Relation)
          (Nonnegative-Integer ?N)
          (>= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(<=> (Maximum-Value-Cardinality ?Instance ?Binary-Relation ?N)
     (And (Binary-Relation ?Binary-Relation)
          (Nonnegative-Integer ?N)
          (=< (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(=> (= (Slot-Cardinality ?Domain-Class ?Binary-Relation) ?N)
    (=> (Instance-Of ?Instance ?Domain-Class)
        (= (Value-Cardinality ?Instance ?Binary-Relation) ?N)))

(<=> (Minimum-Slot-Cardinality ?Domain-Class ?Relation ?N)
     (=> (Instance-Of ?Instance ?Domain-Class)
         (>= (Value-Cardinality ?Instance ?Relation) ?N)))

(<=> (Maximum-Slot-Cardinality ?Domain-Class ?Relation ?N)
     (=> (Instance-Of ?Instance ?Domain-Class)
         (=< (Value-Cardinality ?Instance ?Relation) ?N)))

(<=> (One-To-One-Relation ?R)
     (And (Unary-Function ?R)
          (Value-Type ?R Inverse Function)
          (Value-Cardinality ?R Inverse 1)))

(<=> (One-To-Many-Relation ?R)
     (And (Binary-Relation ?R)
          (Value-Type ?R Inverse Function)
          (Value-Cardinality ?R Inverse 1)))

Notes:

• See-Also: slot-cardinality