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 4716-4718 | |
(documentation AdditionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (AdditionFn ?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。") | japanese_format.kif 878-879 | |
(domain AdditionFn 1 RealNumber) | Merge.kif 4712-4712 | AdditionFn の数値 1 引数は 実数 の instance では %n |
(domain AdditionFn 2 RealNumber) | Merge.kif 4713-4713 | AdditionFn の数値 2 引数は 実数 の instance では %n |
(identityElement AdditionFn 0) | Merge.kif 5295-5295 | 0 は AdditionFn の identity 要素では %n |
(instance AdditionFn AssociativeFunction) | Merge.kif 4708-4708 | AdditionFn は 結合関数 の instance では %n |
(instance AdditionFn BinaryFunction) | Merge.kif 4707-4707 | AdditionFn は 2変数関数 の instance では %n |
(instance AdditionFn CommutativeFunction) | Merge.kif 4709-4709 | AdditionFn は 可換関数 の instance では %n |
(instance AdditionFn TotalValuedRelation) | Merge.kif 4711-4711 | AdditionFn は 合計値関係 の instance では %n |
(range AdditionFn RealNumber) | Merge.kif 4714-4714 | 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 5418-5418 | |
(termFormat ChineseLanguage AdditionFn "加法函数") | chinese_format.kif 683-683 | |
(termFormat ChineseTraditionalLanguage AdditionFn "加成") | domainEnglishFormat.kif 5417-5417 | |
(termFormat EnglishLanguage AdditionFn "addition") | domainEnglishFormat.kif 5416-5416 | |
(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 298-319 | 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 5993-6006 | |
(=> (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 5979-5991 | |
(=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5104-5115 | |
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3258-3268 | |
(=> (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 3083-3102 |
|
(=> (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 3068-3089 |
|
(=> (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 3190-3202 | |
(=> (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 1453-1465 | |
(=> (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 17176-17182 | |
(=> (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 17188-17194 | |
(=> (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 17164-17170 | |
(=> (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 17152-17158 | |
(=> (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 6473-6481 |
statement |
![]() |
(forall (?NUMBER) (equal (SuccessorFn ?NUMBER) (AdditionFn ?NUMBER 1))) |
Merge.kif 4720-4721 | 整数 ( 整数+1) は ( 整数 + 1) と equal では %n |
![]() |
![]() |