| appearance as argument number 1 |
|
| (documentation average ChineseLanguage "这是一个部分函数，只要一个 List 的元素都是 RealNumber，它会把这个List 和一个 RealNumber 联系起来。和这个 List 联系的 RealNumber 等于这个 List 内的 RealNumber 的数学平均 除以列表元素的总数。") | chinese_format.kif 2284-2286 | |
| (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 5263-5267 | |
| (domain average 1 List) | Merge.kif 5260-5260 | |
| (domain average 2 RealNumber) | Merge.kif 5261-5261 | |
| (instance average BinaryPredicate) | Merge.kif 5258-5258 | |
| (instance average PartialValuedRelation) | Merge.kif 5257-5257 | |
| (instance average SingleValuedRelation) | Merge.kif 5259-5259 |
| appearance as argument number 2 |
|
|
| (format ChineseLanguage average "%2 %n 是 %1 的 average") | domainEnglishFormat.kif 228-228 | |
| (format ChineseTraditionalLanguage average "%2 %n 是 %1 的 average") | domainEnglishFormat.kif 227-227 | |
| (format EnglishLanguage average "%2 is %n an average of %1") | domainEnglishFormat.kif 226-226 | |
| (termFormat ChineseLanguage average "平均") | domainEnglishFormat.kif 9351-9351 | |
| (termFormat ChineseTraditionalLanguage average "平均") | domainEnglishFormat.kif 9350-9350 | |
| (termFormat EnglishLanguage average "average") | english_format.kif 1847-1847 |
| antecedent |
|
|
| (<=> (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 | |
| (=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber)))) |
Merge.kif 5269-5274 |
| consequent |
|
|
| (<=> (and (instance ?Y (YearFn ?YEAR)) (equal (MaleLifeExpectancyAtBirthFn ?AREA ?Y) ?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) ?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 372-405 | |
| (<=> (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 418-449 | |
| (<=> (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 |
|
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 is open source software produced by Articulate Software and its partners