AdditionFn |
appearance as argument number 1 |
![]() |
(documentation AdditionFn ChineseLanguage "如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (AdditionFn ?NUMBER1 ?NUMBER2)就是这些数字的算术和。") | chinese_format.kif 2214-2215 | |
(documentation AdditionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.") | Merge.kif 4714-4716 | |
(documentation AdditionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (AdditionFn ?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。") | japanese_format.kif 878-879 | |
(domain AdditionFn 1 RealNumber) | Merge.kif 4710-4710 | AdditionFn の数値 1 引数は 実数 の instance では %n |
(domain AdditionFn 2 RealNumber) | Merge.kif 4711-4711 | AdditionFn の数値 2 引数は 実数 の instance では %n |
(identityElement AdditionFn 0) | Merge.kif 5293-5293 | 0 は AdditionFn の identity 要素では %n |
(instance AdditionFn AssociativeFunction) | Merge.kif 4706-4706 | AdditionFn は 結合関数 の instance では %n |
(instance AdditionFn BinaryFunction) | Merge.kif 4705-4705 | AdditionFn は 2変数関数 の instance では %n |
(instance AdditionFn CommutativeFunction) | Merge.kif 4707-4707 | AdditionFn は 可換関数 の instance では %n |
(instance AdditionFn TotalValuedRelation) | Merge.kif 4709-4709 | AdditionFn は 合計値関係 の instance では %n |
(range AdditionFn RealNumber) | Merge.kif 4712-4712 | AdditionFn の range は 実数 のインスタンス では %n |
appearance as argument number 2 |
![]() |
(format ChineseLanguage AdditionFn "(%*[+])") | chinese_format.kif 682-682 | |
(format EnglishLanguage AdditionFn "(%*[+])") | english_format.kif 684-684 | |
(format FrenchLanguage AdditionFn "(%*[+])") | french_format.kif 414-414 | |
(format ItalianLanguage AdditionFn "(%*[+]") | relations-it.txt 20-20 | |
(format JapaneseLanguage AdditionFn "(%*[+])") | japanese_format.kif 2131-2131 | |
(format PortugueseLanguage AdditionFn "(%*[+])") | portuguese_format.kif 366-366 | |
(format cz AdditionFn "(%*[+])") | relations-cz.txt 423-423 | |
(format de AdditionFn "(%*[+])") | relations-de.txt 889-889 | |
(format hi AdditionFn "(%*[+]") | relations-hindi.txt 65-65 | |
(format ro AdditionFn "(%*[+])") | relations-ro.kif 436-436 | |
(format sv AdditionFn "(%*[+])") | relations-sv.txt 458-458 | |
(format tg AdditionFn "(%*[+]") | relations-cb.txt 54-54 | |
(termFormat ChineseLanguage AdditionFn "加成") | domainEnglishFormat.kif 5423-5423 | |
(termFormat ChineseLanguage AdditionFn "加法函数") | chinese_format.kif 683-683 | |
(termFormat ChineseTraditionalLanguage AdditionFn "加成") | domainEnglishFormat.kif 5422-5422 | |
(termFormat EnglishLanguage AdditionFn "addition") | domainEnglishFormat.kif 5421-5421 | |
(termFormat tg AdditionFn "tungkulin ng pagsasama") | relations-tg.txt 57-57 |
antecedent |
![]() |
consequent |
![]() |
(<=> (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 | average リスト and 実数 リスト 正の整数 リスト の length は リスト の length と equal では %n リスト の 1th element は リスト の 1th element と equal では %n 正の整数
|
(=> (and (equal (PathWeightFn ?PATH) ?SUM) (graphPart ?ARC1 ?PATH) (graphPart ?ARC2 ?PATH) (arcWeight ?ARC1 ?NUMBER1) (arcWeight ?ARC2 ?NUMBER2) (forall (?ARC3) (=> (graphPart ?ARC3 ?PATH) (or (equal ?ARC3 ?ARC1) (equal ?ARC3 ?ARC2))))) (equal (PathWeightFn ?PATH) (AdditionFn ?NUMBER1 ?NUMBER2))) |
Merge.kif 5988-6001 | |
(=> (and (equal (PathWeightFn ?PATH) ?SUM) (subGraph ?SUBPATH ?PATH) (graphPart ?ARC1 ?PATH) (arcWeight ?ARC1 ?NUMBER1) (forall (?ARC2) (=> (graphPart ?ARC2 ?PATH) (or (graphPart ?ARC2 ?SUBPATH) (equal ?ARC2 ?ARC1))))) (equal ?SUM (AdditionFn (PathWeightFn ?SUBPATH) ?NUMBER1))) |
Merge.kif 5974-5986 | |
(=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5102-5113 | |
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3259-3269 | |
(=> (and (equal ?LIST3 (ListConcatenateFn ?LIST1 ?LIST2)) (not (equal ?LIST1 NullList)) (not (equal ?LIST2 NullList)) (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 3084-3103 |
|
(=> (and (equal ?OUT (ReverseFn ?IN)) (equal ?LEN (StringLengthFn ?IN)) (greaterThan ?LEN 1) (greaterThan ?N 0) (lessThan ?N ?LEN) (equal ?PIVOT (CeilingFn (DivisionFn (SubtractionFn ?LEN 1) 2))) (equal ?NEW (AdditionFn (SubtractionFn ?PIVOT ?N) ?PIVOT)) (equal ?S (SubstringFn ?IN ?N (AdditionFn 1 ?N)))) (equal ?S (SubstringFn ?OUT ?NEW (AdditionFn 1 ?NEW)))) |
Media.kif 3050-3071 |
|
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (greaterThan (SubtractionFn ?E ?S) 1)) (equal ?R (ListConcatenateFn (ListFn (ListOrderFn ?L ?S)) (SubListFn (AdditionFn 1 ?S) ?E ?L)))) |
Merge.kif 3191-3203 | |
(=> (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 1437-1449 | |
(=> (and (instance ?M Mixture) (instance ?Z UnitOfMeasure) (mixtureRatio ?A ?B ?X ?Y ?Z) (measure ?M (MeasureFn ?T ?Z)) (part ?A ?M) (part ?B ?M) (measure ?A (MeasureFn ?X ?Z)) (measure ?B (MeasureFn ?Y ?Z))) (equal ?T (AdditionFn ?X ?Y))) |
Food.kif 1248-1262 | |
(=> (and (instance ?MIT BarMitzvah) (patient ?MIT ?X) (instance ?X Boy) (member ?X ?GROUP) (instance ?GROUP Judaism) (birthdate ?X ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?Y13 ?BD13) (and (instance ?Y13 Integer) (equal ?Y13 (AdditionFn ?Y 13)) (instance ?BD13 (DayFn ?D (MonthFn ?M (YearFn ?Y13)))) (equal (WhenFn ?MIT) (ImmediateFutureFn ?BD13))))) |
Biography.kif 69-85 |
|
(=> (and (instance ?MIT BatMitzvah) (patient ?MIT ?X) (instance ?X Girl) (member ?X ?GROUP) (instance ?GROUP Judaism) (birthdate ?X ?DAY) (instance ?DAY (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (exists (?Y13 ?BD13) (and (instance ?Y13 Integer) (equal ?Y13 (AdditionFn ?Y 13)) (instance ?BD13 (DayFn ?D (MonthFn ?M (YearFn ?Y13)))) (equal (WhenFn ?MIT) (ImmediateFutureFn ?BD13))))) |
Biography.kif 99-115 |
|
(=> (and (instance ?UNIT UnitOfArea) (landAreaOnly ?AREA (MeasureFn ?LAND ?UNIT)) (waterAreaOnly ?AREA (MeasureFn ?WATER ?UNIT))) (totalArea ?AREA (MeasureFn (AdditionFn ?LAND ?WATER) ?UNIT))) |
Geography.kif 555-560 | |
(=> (and (instance ?UTC (HourFn ?H1 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (instance ?CST (HourFn ?H2 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (equal (RelativeTimeFn ?UTC CentralTimeZone) ?CST)) (equal ?H2 (AdditionFn ?H1 6))) |
Merge.kif 17283-17289 | |
(=> (and (instance ?UTC (HourFn ?H1 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (instance ?EST (HourFn ?H2 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (equal (RelativeTimeFn ?UTC EasternTimeZone) ?EST)) (equal ?H2 (AdditionFn ?H1 5))) |
Merge.kif 17295-17301 | |
(=> (and (instance ?UTC (HourFn ?H1 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (instance ?MST (HourFn ?H2 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (equal (RelativeTimeFn ?UTC MountainTimeZone) ?MST)) (equal ?H2 (AdditionFn ?H1 7))) |
Merge.kif 17271-17277 | |
(=> (and (instance ?UTC (HourFn ?H1 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (instance ?PST (HourFn ?H2 (DayFn ?D (MonthFn ?M (YearFn ?Y))))) (equal (RelativeTimeFn ?UTC PacificTimeZone) ?PST)) (equal ?H2 (AdditionFn ?H1 8))) |
Merge.kif 17259-17265 | |
(=> (and (totalLengthOfHighwaySystem ?AREA (MeasureFn ?LENGTH ?UNIT)) (lengthOfPavedHighway ?AREA (MeasureFn ?LENGTH1 ?UNIT)) (lengthOfUnpavedHighway ?AREA (MeasureFn ?LENGTH2 ?UNIT)) (instance ?UNIT UnitOfLength)) (totalLengthOfHighwaySystem ?AREA (MeasureFn (AdditionFn ?LENGTH1 ?LENGTH2) ?UNIT))) |
Transportation.kif 510-517 |
|
(=> (and (totalLengthOfHighwaySystem ?AREA (MeasureFn ?LENGTH ?UNIT)) (lengthOfPavedHighway ?AREA (MeasureFn ?LENGTH1 ?UNIT)) (lengthOfUnpavedHighway ?AREA (MeasureFn ?LENGTH2 ?UNIT))) (equal ?LENGTH (AdditionFn ?LENGTH1 ?LENGTH2))) |
Transportation.kif 503-508 | |
(=> (conjugate ?COMPOUND1 ?COMPOUND2) (exists (?NUMBER1 ?NUMBER2) (and (protonNumber ?COMPOUND1 ?NUMBER1) (protonNumber ?COMPOUND2 ?NUMBER2) (or (equal ?NUMBER1 (AdditionFn ?NUMBER2 1)) (equal ?NUMBER2 (AdditionFn ?NUMBER1 1)))))) |
Mid-level-ontology.kif 6495-6503 |
statement |
![]() |
(forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1))) |
Merge.kif 4718-4719 | 整数 ( 整数+1) は ( 整数 + 1) と equal では %n |
![]() |
![]() |