Browsing Interface : Welcome guest : log in		 [  Home |  Graph |  ]  KB:  Language:   

Formal Language: 


KB Term:  Term intersection
English Word: 

Sigma KEE - AdditionFn
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 4729-4731
(documentation AdditionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (AdditionFn ?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。") japanese_format.kif 878-879
(domain AdditionFn 1 RealNumber) Merge.kif 4725-4725 AdditionFn の数値 1 引数は 実数 の instance では
(domain AdditionFn 2 RealNumber) Merge.kif 4726-4726 AdditionFn の数値 2 引数は 実数 の instance では
(identityElement AdditionFn 0) Merge.kif 5308-5308 0 は AdditionFn の identity 要素では
(instance AdditionFn AssociativeFunction) Merge.kif 4721-4721 AdditionFn は 結合関数 の instance では
(instance AdditionFn BinaryFunction) Merge.kif 4720-4720 AdditionFn は 2変数関数 の instance では
(instance AdditionFn CommutativeFunction) Merge.kif 4722-4722 AdditionFn は 可換関数 の instance では
(instance AdditionFn TotalValuedRelation) Merge.kif 4724-4724 AdditionFn は 合計値関係 の instance では
(range AdditionFn RealNumber) Merge.kif 4727-4727 AdditionFn の range は 実数 のインスタンス では

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 5427-5427
(termFormat ChineseLanguage AdditionFn "加法函数") chinese_format.kif 683-683
(termFormat ChineseTraditionalLanguage AdditionFn "加成") domainEnglishFormat.kif 5426-5426
(termFormat EnglishLanguage AdditionFn "addition") domainEnglishFormat.kif 5425-5425
(termFormat de AdditionFn "AdditionFn") terms-de.txt 263-263
(termFormat tg AdditionFn "tungkulin ng pagsasama") relations-tg.txt 57-57

antecedent
-------------------------


(=>
    (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 3052-3073
(=>
    (and
        (holdsDuring ?T
            (attribute ?F Menopausal))
        (birthdate ?F ?B)
        (instance ?B
            (DayFn ?D
                (MonthFn ?M
                    (YearFn ?Y))))
        (equal ?A1
            (AdditionFn 49 ?Y))
        (equal ?A2
            (AdditionFn 52 ?Y))
        (equal ?START
            (BeginFn ?T)))
    (modalAttribute
        (and
            (greaterThan ?START ?A1)
            (greaterThan ?A2 ?START)) Likely))		 Mid-level-ontology.kif 25564-25580
(=>
    (and
        (instance ?Account CreditAccount)
        (accountHolder ?Account ?Agent)
        (principalAmount ?Account ?Principal)
        (agreementPeriod ?Account ?Period)
        (interestEarned ?Account ?Interest ?Period)
        (equal ?Total
            (AdditionFn ?Principal ?Interest)))
    (holdsObligation
        (KappaFn ?Payment
            (transactionAmount ?Payment ?Total)) ?Agent))		 FinancialOntology.kif 1240-1249
(=>
    (and
        (instance ?Account Loan)
        (borrower ?Account ?Agent)
        (principalAmount ?Account ?Principal)
        (agreementPeriod ?Account ?Period)
        (interestEarned ?Account ?Interest ?Period)
        (equal ?Total
            (AdditionFn ?Principal ?Interest)))
    (holdsObligation
        (KappaFn ?Payment
            (transactionAmount ?Payment ?Total)) ?Agent))		 FinancialOntology.kif 1289-1298
(=>
    (and
        (instance ?Bond ZeroCouponBond)
        (maturityDate
            (AccountFn ?Bond) ?Date)
        (possesses ?BondHolder ?Bond)
        (principalAmount
            (AccountFn ?Bond)
            (MeasureFn ?Principal ?CUNIT))
        (agreementPeriod
            (AccountFn ?Bond) ?Period)
        (interestEarned
            (AccountFn ?Bond)
            (MeasureFn ?Interest ?CUNIT) ?Period)
        (equal ?Total
            (AdditionFn ?Principal ?Interest)))
    (exists (?Payment)
        (and
            (instance ?Payment Payment)
            (destination ?Payment ?BondHolder)
            (origin ?Payment
                (AccountFn ?Bond))
            (transactionAmount ?Payment
                (MeasureFn ?Total ?CUNIT)))))		 FinancialOntology.kif 2350-2372
(=>
    (and
        (instance ?Deposit Deposit)
        (instance ?Account FinancialAccount)
        (destination ?Deposit
            (CurrencyFn ?Account))
        (transactionAmount ?Deposit
            (MeasureFn ?Amount ?CUNIT))
        (currentAccountBalance ?Account
            (ImmediatePastFn
                (WhenFn ?Deposit))
            (MeasureFn ?Balance1 ?CUNIT))
        (equal ?Balance2
            (AdditionFn ?Balance1 ?Amount)))
    (currentAccountBalance ?Account
        (ImmediateFutureFn
            (FutureFn ?Deposit))
        (MeasureFn ?Balance2 ?CUNIT)))		 FinancialOntology.kif 438-455
(=>
    (and
        (instance ?LIST ConsecutiveTimeIntervalList)
        (equal ?T1
            (ListOrderFn ?LIST ?N))
        (equal ?T2
            (ListOrderFn ?LIST
                (AdditionFn ?N 1))))
    (equal
        (BeginFn ?T2)
        (EndFn ?T1)))		 Weather.kif 2451-2460
(=>
    (and
        (not
            (equal ?NUMBER2 0))
        (equal
            (AdditionFn
                (MultiplicationFn
                    (FloorFn
                        (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
    (equal
        (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER))		 Merge.kif 5130-5141

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 では リスト の 1th element は リスト の 1th element と equal では 正の整数 正の整数 は リスト の length と equal では 実数 は リスト の 正の整数th element + 正の整数 と equal では
(=>
    (and
        (arcLength ?SEMI
            (MeasureFn ?L ?U))
        (equal ?SEMI SemicircularArc))
    (exists (?CIR ?C)
        (and
            (equal ?CIR Circle)
            (geometricPart ?SEMI ?CIR)
            (circumference ?CIR
                (MeasureFn ?C ?U))
            (equal ?C
                (AdditionFn ?L ?L)))))		 Mid-level-ontology.kif 5700-5710
(=>
    (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 6003-6016
(=>
    (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 5989-6001
(=>
    (and
        (equal
            (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
        (not
            (equal ?NUMBER2 0)))
    (equal
        (AdditionFn
            (MultiplicationFn
                (FloorFn
                    (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))		 Merge.kif 5117-5128
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))		 Merge.kif 3256-3266
(=>
    (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 3081-3100
(=>
    (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 3052-3073
(=>
    (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 3188-3200
(=>
    (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 1970-1982
(=>
    (and
        (instance ?AREA GeographicArea)
        (objectGeographicCoordinates ?AREA ?LAT ?LONG)
        (equal
            (MeasureFn ?DEG AngularDegree)
            (MagneticDeclinationFn ?LAT ?LONG)))
    (exists (?MN)
        (and
            (headingWRTMagneticNorth ?AREA
                (MeasureFn ?MN AngularDegree))
            (headingWRTTrueNorth ?AREA
                (MeasureFn
                    (AdditionFn ?MN ?DEG) AngularDegree)))))		 Geography.kif 3780-3792
(=>
    (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 1249-1263
(=>
    (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 71-87
(=>
    (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 102-118
(=>
    (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 17366-17372
(=>
    (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 17378-17384
(=>
    (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 17354-17360
(=>
    (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 17342-17348
(=>
    (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 7438-7446

statement
-------------------------


(forall (?NUMBER)
    (equal
        (SuccessorFn ?NUMBER)
        (AdditionFn ?NUMBER 1)))		 Merge.kif 4733-4734 整数 ( 整数+1) は ( 整数 + 1) と equal では


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