Browsing Interface : Welcome guest : log in
Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 



KB Term:  Term intersection
English Word: 

  ListLengthFn

Sigma KEE - ListLengthFn
ListLengthFn

appearance as argument number 1
-------------------------


(instance ListLengthFn UnaryFunction) Merge.kif 3123-3123 List length is an instance of unary function
(instance ListLengthFn TotalValuedRelation) Merge.kif 3124-3124 List length is an instance of total valued relation
(domain ListLengthFn 1 List) Merge.kif 3125-3125 The number 1 argument of list length is an instance of list
(range ListLengthFn NonnegativeInteger) Merge.kif 3126-3126 The range of list length is an instance of nonnegative integer
(documentation ListLengthFn EnglishLanguage "A Function that takes a List as its sole argument and returns the number of items in the List. For example, (ListLengthFn (ListFn Monday Tuesday Wednesday)) would return the value 3.") Merge.kif 3128-3131 The range of list length is an instance of nonnegative integer

appearance as argument number 2
-------------------------


(termFormat EnglishLanguage ListLengthFn "list length") domainEnglishFormat.kif 34693-34693
(termFormat ChineseTraditionalLanguage ListLengthFn "列表長度") domainEnglishFormat.kif 34694-34694
(termFormat ChineseLanguage ListLengthFn "列表长度") domainEnglishFormat.kif 34695-34695
(format EnglishLanguage ListLengthFn "length of %1") english_format.kif 270-270

antecedent
-------------------------


(=>
    (and
        (equal ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
        (not
            (equal ?LIST1 NullList))
        (not
            (equal ?LIST2 NullList))
        (lessThanOrEqualTo ?NUMBER1
            (ListLengthFn ?LIST1))
        (lessThanOrEqualTo ?NUMBER2
            (ListLengthFn ?LIST2))
        (instance ?NUMBER1 PositiveInteger)
        (instance ?NUMBER2 PositiveInteger))
    (and
        (equal
            (ListOrderFn ?LIST3 ?NUMBER1)
            (ListOrderFn ?LIST1 ?NUMBER1))
        (equal
            (ListOrderFn ?LIST3
                (AdditionFn
                    (ListLengthFn ?LIST1) ?NUMBER2))
            (ListOrderFn ?LIST2 ?NUMBER2))))
Merge.kif 3194-3213 If All of the following hold: (1) equal X, the list composed of Y, and Z (2) equal Y and null list (3) equal Z and null list (4) W is less than or equal to length of Y (5) V is less than or equal to length of Z (6) W is an instance of positive integer (7) V is an instance of positive integer, then equal U element of X and U element of Y and equal (length of Y and V)th element of X and T element of Z
(=>
    (and
        (equal
            (ListLengthFn ?LIST) ?NUMBER)
        (equal
            (ListOrderFn ?LIST ?NUMBER) ?ITEM))
    (equal
        (LastFn ?LIST) ?ITEM))
Merge.kif 3330-3334 If equal length of X and Y and equal Z element of X and W, then equal the last of X and W
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (equal 1
            (ListLengthFn ?L)))
    (equal ?A
        (ListOrderFn ?L 1)))
Merge.kif 3363-3367 If equal X and the sum of Y and equal 1 and length of Y, then equal X and 1th element of Y
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Merge.kif 3369-3379 If equal X and the sum of Y and length of Y is greater than 1, then equal X and (the first of Y and the sum of the sub-list from 2 to length of Y of Y)
(=>
    (and
        (equal ?A
            (AverageFn ?L))
        (greaterThan
            (ListLengthFn ?L) 0))
    (equal ?A
        (DivisionFn
            (ListSumFn ?L)
            (ListLengthFn ?L))))
Merge.kif 3388-3395 If equal X and the average of the numbers in Y and length of Y is greater than 0, then equal X, the sum of Y, and length of Y
(=>
    (and
        (equal ?VA
            (VarianceAverageFn ?M ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?VA
        (AdditionFn
            (VarianceAverageFn ?M
                (ListOrderFn ?L 1))
            (VarianceAverageFn ?M
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Weather.kif 2763-2775 If equal X and VarianceAverageFn of Y with the mean of Z and length of Y is greater than 1, then equal X and (VarianceAverageFn of 1th element of Y with the mean of Z and VarianceAverageFn of the sub-list from 2 to length of Y of Y with the mean of Z)
(=>
    (and
        (equal ?VA
            (VarianceAverageFn ?M ?L))
        (equal 1
            (ListLengthFn ?L)))
    (equal ?VA
        (MultiplicationFn
            (SubtractionFn ?M
                (ListOrderFn ?L 1))
            (SubtractionFn ?M
                (ListOrderFn ?L 1)))))
Weather.kif 2796-2807 If equal X and VarianceAverageFn of Y with the mean of Z and equal 1 and length of Y, then equal X and (Z and 1th element of Y) and (Z and 1th element of Y)

consequent
-------------------------


(=>
    (and
        (valence ?REL ?NUMBER)
        (instance ?REL Predicate))
    (forall (@ROW)
        (=>
            (?REL @ROW)
            (equal
                (ListLengthFn
                    (ListFn @ROW)) ?NUMBER))))
Merge.kif 3159-3166 If X has Y argument(s) and X is an instance of predicate, then for all : if X @ROW, then equal length of (@ROW) and Y
(=>
    (and
        (equal ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
        (not
            (equal ?LIST1 NullList))
        (not
            (equal ?LIST2 NullList))
        (lessThanOrEqualTo ?NUMBER1
            (ListLengthFn ?LIST1))
        (lessThanOrEqualTo ?NUMBER2
            (ListLengthFn ?LIST2))
        (instance ?NUMBER1 PositiveInteger)
        (instance ?NUMBER2 PositiveInteger))
    (and
        (equal
            (ListOrderFn ?LIST3 ?NUMBER1)
            (ListOrderFn ?LIST1 ?NUMBER1))
        (equal
            (ListOrderFn ?LIST3
                (AdditionFn
                    (ListLengthFn ?LIST1) ?NUMBER2))
            (ListOrderFn ?LIST2 ?NUMBER2))))
Merge.kif 3194-3213 If All of the following hold: (1) equal X, the list composed of Y, and Z (2) equal Y and null list (3) equal Z and null list (4) W is less than or equal to length of Y (5) V is less than or equal to length of Z (6) W is an instance of positive integer (7) V is an instance of positive integer, then equal U element of X and U element of Y and equal (length of Y and V)th element of X and T element of Z
(=>
    (equal
        (LastFn ?LIST) ?ITEM)
    (exists (?NUMBER)
        (and
            (equal
                (ListLengthFn ?LIST) ?NUMBER)
            (equal
                (ListOrderFn ?LIST ?NUMBER) ?ITEM))))
Merge.kif 3323-3328 If equal the last of X and Y, then there exists Z such that equal length of X, Z, equal W element of X, and Y
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Merge.kif 3369-3379 If equal X and the sum of Y and length of Y is greater than 1, then equal X and (the first of Y and the sum of the sub-list from 2 to length of Y of Y)
(=>
    (and
        (equal ?A
            (AverageFn ?L))
        (greaterThan
            (ListLengthFn ?L) 0))
    (equal ?A
        (DivisionFn
            (ListSumFn ?L)
            (ListLengthFn ?L))))
Merge.kif 3388-3395 If equal X and the average of the numbers in Y and length of Y is greater than 0, then equal X, the sum of Y, and length of Y
(=>
    (equal
        (MeasureFn ?H HourDuration)
        (MTBFInstanceFn ?D))
    (equal ?H
        (DivisionFn
            (AdditionFn
                (ListSumFn
                    (PhysicalQuantityToNumberFn
                        (DeviceUpTimeDurationListFn ?D)))
                (ListSumFn
                    (PhysicalQuantityToNumberFn
                        (DevicePlannedDownTimeDurationListFn ?D))))
            (ListLengthFn
                (DeviceFailTimeDurationListFn ?D)))))
Mid-level-ontology.kif 34359-34373 If equal X hour duration(s) and The MTBF of Y is HourDuration, then equal X and (the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The List of deviceUpTime duration for Y is and the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The List of deviceUpTime duration for Y is) and length of The List of deviceFailTime duration for Y is
(=>
    (equal
        (MeasureFn ?X HourDuration)
        (MTTRepairInstanceFn ?D))
    (equal ?X
        (DivisionFn
            (ListSumFn
                (PhysicalQuantityToNumberFn
                    (DeviceFailTimeDurationListFn ?D)))
            (ListLengthFn
                (DeviceFailTimeDurationListFn ?D)))))
Mid-level-ontology.kif 34644-34654 If equal X hour duration(s) and The time to repair of Y is HourDuration, then equal X, the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The List of deviceFailTime duration for Y is, and length of The List of deviceFailTime duration for Y is
(=>
    (equal
        (MeasureFn ?X HourDuration)
        (MTTRecoveryInstanceFn ?D))
    (equal ?X
        (DivisionFn
            (ListSumFn
                (PhysicalQuantityToNumberFn
                    (TimeToRecoveryDurationListFn ?D)))
            (ListLengthFn
                (TimeToRecoveryDurationListFn ?D)))))
Mid-level-ontology.kif 34737-34747 If equal X hour duration(s) and The time to repair of Y is HourDuration, then equal X, the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The list of time to recovery duration for Y is, and length of The list of time to recovery duration for Y is
(=>
    (average ?LIST1 ?AVERAGE)
    (exists (?LIST2 ?LASTPLACE)
        (and
            (equal
                (ListLengthFn ?LIST2)
                (ListLengthFn ?LIST1))
            (equal
                (ListOrderFn ?LIST2 1)
                (ListOrderFn ?LIST1 1))
            (forall (?ITEMFROM2)
                (=>
                    (inList ?ITEMFROM2 ?LIST2)
                    (exists (?POSITION ?POSITIONMINUSONE ?ITEMFROM1 ?PRIORFROM2)
                        (and
                            (greaterThan ?POSITION 1)
                            (lessThanOrEqualTo ?POSITION
                                (ListLengthFn ?LIST2))
                            (equal
                                (ListOrderFn ?LIST2 ?ITEMFROM2) ?POSITION)
                            (inList ?ITEMFROM1 ?LIST1)
                            (equal ?POSITION
                                (ListOrderFn ?LIST1 ?ITEMFROM1))
                            (inList ?PRIORFROM2 ?LIST2)
                            (equal ?POSITIONMINUSONE
                                (SubtractionFn ?POSITION 1))
                            (equal ?POSITIONMINUSONE
                                (ListOrderFn ?LIST2 ?PRIORFROM2))
                            (equal ?ITEMFROM2
                                (AdditionFn ?ITEMFROM1 ?PRIORFROM2))))))
            (equal ?LASTPLACE
                (ListLengthFn ?LIST2))
            (equal ?AVERAGE
                (DivisionFn
                    (ListOrderFn ?LIST2 ?LASTPLACE) ?LASTPLACE)))))
People.kif 306-327 If X is an average of Y, then there exist Z and W such that equal length of Z and length of Y and equal 1th element of Z and 1th element of Y and V V is a member of Zthere exist U, T,, , S and R such that U is greater than 1 and U is less than or equal to length of Z and equal Q element of Z and U and S is a member of Y and equal U and P element of Y and R is a member of Z and equal T and (U and 1) and equal T and O element of Z and equal V and (S and R) and equal W and length of Z and equal X and N element of Z and W
(=>
    (and
        (instance ?YEAR
            (YearFn ?Y))
        (equal
            (LifeExpectancyAtBirthFn ?AREA ?YEAR) ?REALNUMBER))
    (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH)
        (and
            (instance ?LIST List)
            (instance
                (ListLengthFn ?LIST) ?COUNT)
            (forall (?LISTITEM)
                (=>
                    (inList ?LISTITEM ?LIST)
                    (and
                        (instance ?LISTITEM ?LIFEEXPECTANCYAGE)
                        (not
                            (exists (?NUMBER)
                                (and
                                    (instance ?NUMBER ?LIFEEXPECTANCYAGE)
                                    (not
                                        (inList ?NUMBER ?LIST)))))
                        (equal ?COUNT
                            (CardinalityFn
                                (KappaFn ?LIFEEXPECTANCYAGE
                                    (and
                                        (instance ?BIRTH Birth)
                                        (experiencer ?BIRTH ?INDIVIDUAL)
                                        (instance ?INDIVIDUAL Human)
                                        (during
                                            (WhenFn ?BIRTH) ?YEAR)
                                        (equal
                                            (WhereFn ?BIRTH
                                                (WhenFn ?BIRTH)) ?AREA)
                                        (instance ?DEATH Death)
                                        (experiencer ?DEATH ?INDIVIDUAL)
                                        (holdsDuring
                                            (WhenFn ?DEATH)
                                            (age ?INDIVIDUAL
                                                (MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
            (average ?LIST ?REALNUMBER))))
People.kif 344-376 If X is an instance of the year Y and equal the life expectancy at birth of Z, X, and W, then All of the following hold: (1) there exist V, U,, , T,, , S,, , R (2) Q such that V is an instance of list (3) length of V is an instance of U (4) P P is a member of VP is an instance of T (5) there doesn't exist O such that O is an instance of T (6) O is not a member of V (7) equal U (8) the number of instances in the class described by T (9) W is an average of V
(=>
    (and
        (instance ?Y
            (YearFn ?YEAR))
        (equal
            (MaleLifeExpectancyAtBirthFn ?AREA ?Y) ?REALNUMBER))
    (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH)
        (and
            (instance ?LIST List)
            (instance
                (ListLengthFn ?LIST) ?COUNT)
            (forall (?LISTITEM)
                (=>
                    (inList ?LISTITEM ?LIST)
                    (and
                        (instance ?LISTITEM ?LIFEEXPECTANCYAGE)
                        (not
                            (exists (?NUMBER)
                                (and
                                    (instance ?NUMBER ?LIFEEXPECTANCYAGE)
                                    (not
                                        (inList ?NUMBER ?LIST)))))
                        (equal ?COUNT
                            (CardinalityFn
                                (KappaFn ?LIFEEXPECTANCYAGE
                                    (and
                                        (instance ?BIRTH Birth)
                                        (experiencer ?BIRTH ?INDIVIDUAL)
                                        (instance ?INDIVIDUAL Human)
                                        (attribute ?INDIVIDUAL Male)
                                        (during
                                            (WhenFn ?BIRTH) ?Y)
                                        (equal
                                            (WhereFn ?BIRTH
                                                (WhenFn ?BIRTH)) ?AREA)
                                        (instance ?DEATH Death)
                                        (experiencer ?DEATH ?INDIVIDUAL)
                                        (holdsDuring
                                            (WhenFn ?DEATH)
                                            (age ?INDIVIDUAL
                                                (MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
            (average ?LIST ?REALNUMBER))))
People.kif 391-424 If X is an instance of the year Y and equal the male life expectancy at birth of Z, X, and W, then All of the following hold: (1) there exist V, U,, , T,, , S,, , R (2) Q such that V is an instance of list (3) length of V is an instance of U (4) P P is a member of VP is an instance of T (5) there doesn't exist O such that O is an instance of T (6) O is not a member of V (7) equal U (8) the number of instances in the class described by T (9) W is an average of V
(=>
    (and
        (instance ?YEAR
            (YearFn ?Y))
        (equal
            (FemaleLifeExpectancyAtBirthFn ?AREA ?YEAR) ?REALNUMBER))
    (exists (?LIST ?COUNT ?LIFEEXPECTANCYAGE ?BIRTH ?INDIVIDUAL ?DEATH)
        (and
            (instance ?LIST List)
            (instance
                (ListLengthFn ?LIST) ?COUNT)
            (forall (?LISTITEM)
                (=>
                    (inList ?LISTITEM ?LIST)
                    (and
                        (instance ?LISTITEM ?LIFEEXPECTANCYAGE)
                        (not
                            (exists (?NUMBER)
                                (and
                                    (instance ?NUMBER ?LIFEEXPECTANCYAGE)
                                    (not
                                        (inList ?NUMBER ?LIST)))))
                        (equal ?COUNT
                            (CardinalityFn
                                (KappaFn ?LIFEEXPECTANCYAGE
                                    (and
                                        (instance ?BIRTH Birth)
                                        (experiencer ?BIRTH ?INDIVIDUAL)
                                        (instance ?INDIVIDUAL Human)
                                        (attribute ?INDIVIDUAL Female)
                                        (during
                                            (WhenFn ?BIRTH) ?YEAR)
                                        (equal
                                            (WhereFn ?BIRTH
                                                (WhenFn ?BIRTH)) ?AREA)
                                        (instance ?DEATH Death)
                                        (experiencer ?DEATH ?INDIVIDUAL)
                                        (holdsDuring
                                            (WhenFn ?DEATH)
                                            (age ?INDIVIDUAL
                                                (MeasureFn ?LIFEEXPECTANCYAGE YearDuration))))))))))
            (average ?LIST ?REALNUMBER))))
People.kif 437-470 If X is an instance of the year Y and equal the female life expectancy at birth of Z, X, and W, then All of the following hold: (1) there exist V, U,, , T,, , S,, , R (2) Q such that V is an instance of list (3) length of V is an instance of U (4) P P is a member of VP is an instance of T (5) there doesn't exist O such that O is an instance of T (6) O is not a member of V (7) equal U (8) the number of instances in the class described by T (9) W is an average of V
(=>
    (and
        (instance ?PAGE SearchResultsPage)
        (instance ?RESULTS SRPResults)
        (component ?RESULTS ?PAGE))
    (equal
        (DivisionFn
            (CardinalityFn
                (KappaFn ?CLICK
                    (and
                        (instance ?CLICK RequestingHyperlink)
                        (patient ?CLICK ?ELEMENT)
                        (destination ?CLICK ?LINKEDPAGE)
                        (instance ?ELEMENT HypertextLink)
                        (component ?ELEMENT ?PAGE)
                        (or
                            (instance ?LINKEDPAGE ProductDescriptionPage)
                            (instance ?LINKEDPAGE ViewItemPage)))))
            (ListLengthFn ?RESULTS))
        (SRPEngagementFn ?PAGE)))
UXExperimentalTerms.kif 3718-3736 If X is an instance of search results page, Y is an instance of search results, and Y is a component of X, then equal the number of instances in the class described by Z, length of Y, and qualifying clicks on X
(=>
    (and
        (equal ?VA
            (VarianceAverageFn ?M ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?VA
        (AdditionFn
            (VarianceAverageFn ?M
                (ListOrderFn ?L 1))
            (VarianceAverageFn ?M
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Weather.kif 2763-2775 If equal X and VarianceAverageFn of Y with the mean of Z and length of Y is greater than 1, then equal X and (VarianceAverageFn of 1th element of Y with the mean of Z and VarianceAverageFn of the sub-list from 2 to length of Y of Y with the mean of Z)
(=>
    (and
        (equal ?V
            (VarianceFn ?L))
        (equal ?M
            (AverageFn ?L)))
    (equal ?V
        (DivisionFn
            (VarianceAverageFn ?M ?L)
            (ListLengthFn ?L))))
Weather.kif 2785-2794 If equal X and The VarianceFn Y and equal Z and the average of the numbers in Y, then equal X, VarianceAverageFn of Y with the mean of Z, and length of Y
(=>
    (equal ?SPEED
        (Mean3SecondWindSpeedFn ?PLACE ?TIME))
    (holdsDuring ?TIME
        (exists (?MLIST ?RLIST ?NLIST ?UNIT)
            (and
                (instance ?MLIST MeasuringSurfaceWindSpeedList)
                (locationMeasuringList ?MLIST ?PLACE)
                (measuringListInterval ?MLIST
                    (MeasureFn 0.25 SecondDuration))
                (measuringListDuration ?MLIST
                    (MeasureFn 3 SecondDuration))
                (equal 12
                    (ListLengthFn ?MLIST))
                (measuringResult ?MLIST ?RLIST)
                (equal ?NLIST
                    (PhysicalQuantityToNumberFn ?RLIST))
                (equal ?SPEED
                    (MeasureFn
                        (AverageFn ?NLIST) ?UNIT))))))
Weather.kif 3171-3188 If equal X and Mean3SecondWindSpeedFn for Y in region Z, then there exist W, V,, , U and T such that W is an instance of measuring surface wind speed list and The eventLocated for W is Z and measuring list interval W and 0.25 second duration(s) and The Measuring for list W takes 3 second duration(s). and equal 12 and length of W and V is the result of W and equal U and PhysicalQuantityToNumberFn returns the numberic values of a list of V and equal X and the average of the numbers in U T(s) holds during Y
(=>
    (equal ?SPEED
        (Mean10MinutesWindSpeedFn ?PLACE ?TIME))
    (holdsDuring ?TIME
        (exists (?MLIST ?RLIST ?NLIST ?UNIT)
            (and
                (instance ?MLIST MeasuringSurfaceWindSpeedList)
                (locationMeasuringList ?MLIST ?PLACE)
                (measuringListInterval ?MLIST
                    (MeasureFn 5 SecondDuration))
                (measuringListDuration ?MLIST
                    (MeasureFn 10 MinuteDuration))
                (equal 120
                    (ListLengthFn ?MLIST))
                (measuringResult ?MLIST ?RLIST)
                (equal ?NLIST
                    (PhysicalQuantityToNumberFn ?RLIST))
                (equal ?SPEED
                    (MeasureFn
                        (AverageFn ?NLIST) ?UNIT))))))
Weather.kif 3490-3507 If equal X and Mean10MinutesWindSpeedFn for Y in region Z, then there exist W, V,, , U and T such that W is an instance of measuring surface wind speed list and The eventLocated for W is Z and measuring list interval W and 5 second duration(s) and The Measuring for list W takes 10 minute duration(s). and equal 120 and length of W and V is the result of W and equal U and PhysicalQuantityToNumberFn returns the numberic values of a list of V and equal X and the average of the numbers in U T(s) holds during Y
(=>
    (equal ?SPEED
        (Mean3MinutesWindSpeedFn ?PLACE ?TIME))
    (holdsDuring ?TIME
        (exists (?MLIST ?RLIST ?NLIST ?UNIT)
            (and
                (instance ?MLIST MeasuringSurfaceWindSpeedList)
                (locationMeasuringList ?MLIST ?PLACE)
                (measuringListInterval ?MLIST
                    (MeasureFn 5 SecondDuration))
                (measuringListDuration ?MLIST
                    (MeasureFn 2 MinuteDuration))
                (equal 36
                    (ListLengthFn ?MLIST))
                (measuringResult ?MLIST ?RLIST)
                (equal ?NLIST
                    (PhysicalQuantityToNumberFn ?RLIST))
                (equal ?SPEED
                    (MeasureFn
                        (AverageFn ?NLIST) ?UNIT))))))
Weather.kif 3525-3542 If equal X and Mean3MinutesWindSpeedFn for Y in region Z, then there exist W, V,, , U and T such that W is an instance of measuring surface wind speed list and The eventLocated for W is Z and measuring list interval W and 5 second duration(s) and The Measuring for list W takes 2 minute duration(s). and equal 36 and length of W and V is the result of W and equal U and PhysicalQuantityToNumberFn returns the numberic values of a list of V and equal X and the average of the numbers in U T(s) holds during Y
(=>
    (equal ?SPEED
        (Mean2MinutesWindSpeedFn ?PLACE ?TIME))
    (holdsDuring ?TIME
        (exists (?MLIST ?RLIST ?NLIST ?UNIT)
            (and
                (instance ?MLIST MeasuringSurfaceWindSpeedList)
                (locationMeasuringList ?MLIST ?PLACE)
                (measuringListInterval ?MLIST
                    (MeasureFn 5 SecondDuration))
                (measuringListDuration ?MLIST
                    (MeasureFn 2 MinuteDuration))
                (equal 24
                    (ListLengthFn ?MLIST))
                (measuringResult ?MLIST ?RLIST)
                (equal ?NLIST
                    (PhysicalQuantityToNumberFn ?RLIST))
                (equal ?SPEED
                    (MeasureFn
                        (AverageFn ?NLIST) ?UNIT))))))
Weather.kif 3560-3577 If equal X and Mean2MinutesWindSpeedFn for Y in region Z, then there exist W, V,, , U and T such that W is an instance of measuring surface wind speed list and The eventLocated for W is Z and measuring list interval W and 5 second duration(s) and The Measuring for list W takes 2 minute duration(s). and equal 24 and length of W and V is the result of W and equal U and PhysicalQuantityToNumberFn returns the numberic values of a list of V and equal X and the average of the numbers in U T(s) holds during Y
(=>
    (equal ?SPEED
        (Mean1MinuteWindSpeedFn ?PLACE ?TIME))
    (holdsDuring ?TIME
        (exists (?MLIST ?RLIST ?NLIST ?UNIT)
            (and
                (instance ?MLIST MeasuringSurfaceWindSpeedList)
                (locationMeasuringList ?MLIST ?PLACE)
                (measuringListInterval ?MLIST
                    (MeasureFn 5 SecondDuration))
                (measuringListDuration ?MLIST
                    (MeasureFn 1 MinuteDuration))
                (equal 12
                    (ListLengthFn ?MLIST))
                (measuringResult ?MLIST ?RLIST)
                (equal ?NLIST
                    (PhysicalQuantityToNumberFn ?RLIST))
                (equal ?SPEED
                    (MeasureFn
                        (AverageFn ?NLIST) ?UNIT))))))
Weather.kif 3595-3612 If equal X and Mean1MinuteWindSpeedFn for Y in region Z, then there exist W, V,, , U and T such that W is an instance of measuring surface wind speed list and The eventLocated for W is Z and measuring list interval W and 5 second duration(s) and The Measuring for list W takes 1 minute duration(s). and equal 12 and length of W and V is the result of W and equal U and PhysicalQuantityToNumberFn returns the numberic values of a list of V and equal X and the average of the numbers in U T(s) holds during Y

statement
-------------------------


(forall (@ROW ?ITEM)
    (equal
        (ListLengthFn
            (ListFn @ROW ?ITEM))
        (SuccessorFn
            (ListLengthFn
                (ListFn @ROW)))))
Merge.kif 3148-3151 For all Entity Y: equal length of (@ROW and Y) and (length of (@ROW)+1)
(forall (@ROW ?ITEM)
    (equal
        (ListOrderFn
            (ListFn @ROW ?ITEM)
            (ListLengthFn
                (ListFn @ROW ?ITEM))) ?ITEM))
Merge.kif 3153-3157 For all Entity Y: equal length of (@ROW and Y)th element of (@ROW and Y) and Y


Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners