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


KB Term:  Term intersection
English Word: 

Sigma KEE - average
average

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


(instance average PartialValuedRelation) Merge.kif 5480-5480 average is an instance of partial valued relation
(instance average BinaryPredicate) Merge.kif 5481-5481 average is an instance of binary predicate
(instance average SingleValuedRelation) Merge.kif 5482-5482 average is an instance of single valued relation
(domain average 1 List) Merge.kif 5483-5483 The number 1 argument of average is an instance of list
(domain average 2 RealNumber) Merge.kif 5484-5484 The number 2 argument of average is an instance of real number
(documentation average EnglishLanguage "A partial function that relates a List to a RealNumber, provided that the List only has list elements that are RealNumbers. The RealNumber associated with the List is equal to the mathematical average of the RealNumbers in the List divided by the total number of list elements.") Merge.kif 5486-5490 The number 2 argument of average is an instance of real number

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


(format EnglishLanguage average "%2 is %n an average of %1") domainEnglishFormat.kif 226-226
(format ChineseTraditionalLanguage average "%2 %n 是 %1 的 average") domainEnglishFormat.kif 227-227
(format ChineseLanguage average "%2 %n 是 %1 的 average") domainEnglishFormat.kif 228-228
(termFormat ChineseTraditionalLanguage average "平均") domainEnglishFormat.kif 9341-9341
(termFormat ChineseLanguage average "平均") domainEnglishFormat.kif 9342-9342
(termFormat EnglishLanguage average "average") english_format.kif 1851-1851

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


(=>
    (average ?LIST ?AVERAGE)
    (forall (?LISTITEM)
        (=>
            (inList ?LISTITEM ?LIST)
            (instance ?LISTITEM RealNumber))))		 Merge.kif 5492-5497 If X is an average of Y, then For all Entity Z: if Z is a member of Y, then Z is an instance of real number
(=>
    (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

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


(=>
    (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


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


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