| appearance as argument number 1 |
|
| (documentation average ChineseLanguage "这是一个部分函数，只要一个 List 的元素都是 RealNumber，它会把这个List 和一个 RealNumber 联系起来。和这个 List 联系的 RealNumber 等于这个 List 内的 RealNumber 的数学平均 除以列表元素的总数。") | Merge.kif 7749-7751 | |
| (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 7743-7747 | |
| (documentation average JapaneseLanguage "List を RealNumber に関連付ける部分関数で、 Listに RealNumber であるリスト要素のみが含まれる。List に関連付けられた RealNumber は、 List の RealNumber の数学的平均をリスト要素の総数で割った値に等しい。") | Merge.kif 7753-7755 | |
| (domain average 1 List) | Merge.kif 7739-7739 | average の数値 1 引数は リスト の instance では %n |
| (domain average 2 RealNumber) | Merge.kif 7740-7740 | average の数値 2 引数は 実数 の instance では %n |
| (instance average BinaryPredicate) | Merge.kif 7737-7737 | average は 2進述語 の instance では %n |
| (instance average PartialValuedRelation) | Merge.kif 7736-7736 | average は 部分的価値関係 の instance では %n |
| (instance average SingleValuedRelation) | Merge.kif 7738-7738 | average は 一価関係 の instance では %n |
| 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 9355-9355 | termFormat ChineseLanguage, average and "平均" |
| (termFormat ChineseTraditionalLanguage average "平均") | domainEnglishFormat.kif 9354-9354 | termFormat ChineseTraditionalLanguage, average and "平均" |
| (termFormat EnglishLanguage average "average") | domainEnglishFormat.kif 9353-9353 | termFormat EnglishLanguage, average and "average" |
| 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 285-306 | average リスト and 実数 リスト リスト の length は リスト の length と equal では %n リスト の 1th element は リスト の 1th element と equal では %n 正の整数
|
| (=> (average ?LIST ?AVERAGE) (forall (?LISTITEM) (=> (inList ?LISTITEM ?LIST) (instance ?LISTITEM RealNumber)))) |
Merge.kif 7757-7762 |
| consequent |
|
|
| (<=> (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 411-442 | FemaleLifeExpectancyAtBirthFn 地政学的地域 and 整数 year 目 は 実数 と equal では %n リスト リスト は リスト の instance では %n リスト の length は 整数 の instance では %n リストITEM
|
| (<=> (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 323-353 | LifeExpectancyAtBirthFn 地政学的地域 and 整数 year 目 は 実数 と equal では %n リスト リスト は リスト の instance では %n リスト の length は 整数 の instance では %n リストITEM
|
| (<=> (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 367-398 | MaleLifeExpectancyAtBirthFn 地政学的地域 and 整数 year 目 は 実数 と equal では %n リスト リスト は リスト の instance では %n リスト の length は 整数 の instance では %n リストITEM
|
|
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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners