Function Length

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

Instance-Of@Frame-Ontology:

Binary-Relation@Ol-User%Kif-Relations, Function@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets

Domain@Frame-Ontology: List

Range@Frame-Ontology: Nonnegative-Integer

Arity@Frame-Ontology: 2

Documentation@Ol%Frame-Ontology: The function constant {tt length} gives the number of items in a list.

Implication Axioms mentioning Length:

(=> (= (Cardinality@Ol-User%Kif-Extensions ?Set) ?Integer)
    (Exists (@Elements)
            (And (= ?Set (Setof @Elements))
                 (= ?Integer (Length (Listof @Elements))))))

(=> (= (Arity@Frame-Ontology ?Relation) ?N)
    (Forall (?Tuple)
            (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
                (= (Length ?Tuple) ?N))))

(=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type)
    (Forall (?Tuple)
            (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
                (And (>= (Length ?Tuple) ?N)
                     (Instance-Of@Frame-Ontology (Nth ?Tuple ?N)
                                  ?Type)))))

Equivalence Axioms mentioning Length:

(<=> (Null ?List) (And (List ?List) (= (Length ?List) 0)))

(<=> (Single ?List) (And (List ?List) (= (Length ?List) 1)))

(<=> (Double ?List) (And (List ?List) (= (Length ?List) 2)))

(<=> (Triple ?List) (And (List ?List) (= (Length ?List) 3)))

(<=> (Cardinality@Ol-User%Kif-Extensions ?Set)
     (And (Set@Ol-User%Kif-Sets ?Set)
          (Exists (@Elements)
                  (And (= ?Set (Setof @Elements))
                       (= ?Integer (Length (Listof @Elements)))))))

Axioms mentioning Length:

(= (Length ?List) 0)

(= (Length ?List) 1)

(= (Length ?List) 2)

(= (Length ?List) 3)