Function CARDINALITY

• Defined in theory: Kif-extensions
• Source code: kif-extensions.lisp

Slots on this function:

Documentation:

Returns the number of elements in a set.

Instance-Of: Function

Arity: 2

Domain: Set

Range: Integer

Equivalence Axioms:

(<=> (Cardinality ?Set)
     (And (Set ?Set)
          (Exists (@Elements)
                  (And (= ?Set (Setof @Elements))
                       (= ?Integer (Length (Listof @Elements)))))))

Other Related Axioms:

(=> (Cardinality $X $Y) (Set $X))

(=> (= (Cardinality ?Set) ?Integer)
    (Exists (@Elements)
            (And (= ?Set (Setof @Elements))
                 (= ?Integer (Length (Listof @Elements))))))

(=> (= (Cardinality ?Set) ?Integer) (Set ?Set))

Notes:

• not explicitly defined in the KIF 3.0 spec