| 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 5363-5367 | |
| (documentation average JapaneseLanguage "List を RealNumber に関連付ける部分関数で、 Listに RealNumber であるリスト要素のみが含まれる。List に関連付けられた RealNumber は、 List の RealNumber の数学的平均をリスト要素の総数で割った値に等しい。") | japanese_format.kif 952-954 | |
| (domain average 1 List) | Merge.kif 5360-5360 | 域 平均, 1 and List |
| (domain average 2 RealNumber) | Merge.kif 5361-5361 | 域 平均, 2 and RealNumber |
| (instance average BinaryPredicate) | Merge.kif 5358-5358 | 例 平均 and BinaryPredicate |
| (instance average PartialValuedRelation) | Merge.kif 5357-5357 | 例 平均 and PartialValuedRelation |
| (instance average SingleValuedRelation) | Merge.kif 5359-5359 | 例 平均 and SingleValuedRelation |
| 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 9342-9342 | |
| (termFormat ChineseTraditionalLanguage average "平均") | domainEnglishFormat.kif 9341-9341 | |
| (termFormat EnglishLanguage average "average") | english_format.kif 1847-1847 |
| antecedent |
|
|
| (<=> (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 272-293 | RealNumber 是 List 的 average List PositiveInteger 等於 列表長度 List and 列表長度 List 等於 清單順序 List and 1 and 清單順序 List and 1 PositiveInteger
|
| (=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber)))) |
Merge.kif 5369-5374 |
|
| consequent |
|
|
| (<=> (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 357-390 | 例 年 and 年 年EAR 等於 GeopoliticalArea 和 年 的 male 出生估計壽命 and RealNumber List Integer, SymbolicString, entity, entity and entity 例 List and List 例 列表長度 List and Integer ListITEM
|
| (<=> (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 403-436 | 例 年 and 年 Integer 等於 GeopoliticalArea 和 年 的 female 出生預期壽命 and RealNumber List Integer, SymbolicString, entity, entity and entity 例 List and List 例 列表長度 List and Integer ListITEM
|
| (<=> (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 310-342 | 例 年 and 年 Integer 等於 GeopoliticalArea 和 年 的出生預期 life and RealNumber List Integer, SymbolicString, entity, entity and entity 例 List and List 例 列表長度 List and Integer ListITEM
|
|
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