Function Cardinality

• Defined in ontology: Kif-extensions
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/kif/../../all-ontologies/kif/kif-extensions.lisp

Instance-Of@Frame-Ontology:

Binary-Relation, Function, Relation, Set

Domain@Frame-Ontology: Set

Range@Frame-Ontology: Integer

Arity@Frame-Ontology: 2

Documentation@Ol%Frame-Ontology:

Returns the number of elements in a set.

Notes:

• not explicitly defined in the KIF 3.0 spec

Equivalence Axioms for Cardinality:

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

Implication Axioms mentioning Cardinality:

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

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