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

Formal Language: 



KB Term:  Term intersection
English Word: 

  ListLengthFn

Sigma KEE - ListLengthFn
ListLengthFn

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


(documentation ListLengthFn ChineseLanguage "这个 Function 接受一个 List 作为它唯一的参数, 然后交出这个 List 中项目的数量。例如: (ListLengthFn (ListFn Monday Tuesday Wednesday))交出的值会是3。") chinese_format.kif 1967-1969
(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 2946-2949
(domain ListLengthFn 1 List) Merge.kif 2943-2943 The number 1 argument of list length is an instance of list
(instance ListLengthFn TotalValuedRelation) Merge.kif 2942-2942 List length is an instance of total valued relation
(instance ListLengthFn UnaryFunction) Merge.kif 2941-2941 List length is an instance of unary function
(range ListLengthFn NonnegativeInteger) Merge.kif 2944-2944 The range of list length is an instance of nonnegative integer

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


(format ChineseLanguage ListLengthFn "%1 的长度") chinese_format.kif 265-265
(format EnglishLanguage ListLengthFn "length of %1") english_format.kif 270-270
(termFormat ChineseLanguage ListLengthFn "列表长度") domainEnglishFormat.kif 34674-34674
(termFormat ChineseLanguage ListLengthFn "找出表列长度的函数") chinese_format.kif 266-266
(termFormat ChineseTraditionalLanguage ListLengthFn "列表長度") domainEnglishFormat.kif 34673-34673
(termFormat EnglishLanguage ListLengthFn "list length") domainEnglishFormat.kif 34672-34672

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


(=>
    (and
        (equal ?A
            (AverageFn ?L))
        (greaterThan
            (ListLengthFn ?L) 0))
    (equal ?A
        (DivisionFn
            (ListSumFn ?L)
            (ListLengthFn ?L))))
Merge.kif 3201-3208
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (equal 1
            (ListLengthFn ?L)))
    (equal ?A
        (ListOrderFn ?L 1)))
Merge.kif 3176-3180
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Merge.kif 3182-3192
(=>
    (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 1485-1496
(=>
    (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 1452-1464

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


(<=>
    (and
        (equal ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
        (not
            (equal ?LIST1 NullList))
        (not
            (equal ?LIST2 NullList)))
    (forall (?NUMBER1 ?NUMBER2)
        (=>
            (and
                (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 3012-3028 A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer
(<=>
    (average ?LIST1 ?AVERAGE)
    (exists (?LIST2)
        (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 289-310 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
(<=>
    (equal
        (FemaleLifeExpectancyAtBirthFn ?AREA
            (YearFn ?YEAR)) ?REALNUMBER)
    (exists (?LIST)
        (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)
                                            (YearFn ?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 415-446 The female life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
(<=>
    (equal
        (LastFn ?LIST) ?ITEM)
    (exists (?NUMBER)
        (and
            (equal
                (ListLengthFn ?LIST) ?NUMBER)
            (equal
                (ListOrderFn ?LIST ?NUMBER) ?ITEM))))
Merge.kif 3140-3145 The last of a list is equal to an entity if and only if there exists a positive integer such that length of the list is equal to the positive integer and the positive integerth element of the list is equal to the entity
(<=>
    (equal
        (LifeExpectancyAtBirthFn ?AREA
            (YearFn ?YEAR)) ?REALNUMBER)
    (exists (?LIST)
        (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)
                                            (YearFn ?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 327-357 The life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
(<=>
    (equal
        (MaleLifeExpectancyAtBirthFn ?AREA
            (YearFn ?YEAR)) ?REALNUMBER)
    (exists (?LIST)
        (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)
                                            (YearFn ?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 371-402 The male life expectancy at birth of a geopolitical area and the year an integer is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list
(=>
    (and
        (equal ?A
            (AverageFn ?L))
        (greaterThan
            (ListLengthFn ?L) 0))
    (equal ?A
        (DivisionFn
            (ListSumFn ?L)
            (ListLengthFn ?L))))
Merge.kif 3201-3208
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Merge.kif 3182-3192
(=>
    (and
        (equal ?V
            (VarianceFn ?L))
        (equal ?M
            (AverageFn ?L)))
    (equal ?V
        (DivisionFn
            (VarianceAverageFn ?M ?L)
            (ListLengthFn ?L))))
Weather.kif 1474-1483
(=>
    (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 1452-1464
(=>
    (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 3928-3946
(=>
    (and
        (valence ?REL ?NUMBER)
        (instance ?REL Predicate))
    (forall (@ROW)
        (=>
            (?REL @ROW)
            (equal
                (ListLengthFn
                    (ListFn @ROW)) ?NUMBER))))
Merge.kif 2977-2984
(=>
    (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 2216-2233
(=>
    (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 2321-2338
(=>
    (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 2286-2303
(=>
    (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 2251-2268
(=>
    (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 1903-1920

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


(forall (@ROW ?ITEM)
    (equal
        (ListLengthFn
            (ListFn @ROW ?ITEM))
        (SuccessorFn
            (ListLengthFn
                (ListFn @ROW)))))
Merge.kif 2966-2969 For all @ROW and another entity length of (@ROW and the other entity) is equal to (length of (@ROW)+1)
(forall (@ROW ?ITEM)
    (equal
        (ListOrderFn
            (ListFn @ROW ?ITEM)
            (ListLengthFn
                (ListFn @ROW ?ITEM))) ?ITEM))
Merge.kif 2971-2975 For all @ROW and another entity length of (@ROW and the other entity)th element of (@ROW and the other entity) is equal to the other entity


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 is open source software produced by Articulate Software and its partners