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

Formal Language: 



KB Term:  Term intersection
English Word: 

  AdditionFn

 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 4717-4719
(documentation AdditionFn JapaneseLanguage "?NUMBER1 と ?NUMBER2 が Number の場合、 (AdditionFn ?NUMBER1 ?NUMBER2) はこれらの数値の算術合計である。") japanese_format.kif 878-879
(domain AdditionFn 1 RealNumber) Merge.kif 4713-4713
(domain AdditionFn 2 RealNumber) Merge.kif 4714-4714
(identityElement AdditionFn 0) Merge.kif 5296-5296
(instance AdditionFn AssociativeFunction) Merge.kif 4709-4709
(instance AdditionFn BinaryFunction) Merge.kif 4708-4708
(instance AdditionFn CommutativeFunction) Merge.kif 4710-4710
(instance AdditionFn TotalValuedRelation) Merge.kif 4712-4712
(range AdditionFn RealNumber) Merge.kif 4715-4715

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
-------------------------


(=>
    (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
        (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 23973-23989
(=>
    (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 1224-1233
(=>
    (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 1273-1282
(=>
    (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 2333-2355
(=>
    (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 436-453
(=>
    (and
        (instance ?LIST ConsecutiveTimeIntervalList)
        (equal ?T1
            (ListOrderFn ?LIST ?N))
        (equal ?T2
            (ListOrderFn ?LIST
                (AdditionFn ?N 1))))
    (equal
        (BeginFn ?T2)
        (EndFn ?T1)))		 Weather.kif 1918-1927
(=>
    (and
        (not
            (equal ?NUMBER2 0))
        (equal
            (AdditionFn
                (MultiplicationFn
                    (FloorFn
                        (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
    (equal
        (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER))		 Merge.kif 5118-5129

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
(=>
    (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 5994-6007
(=>
    (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 5980-5992
(=>
    (and
        (equal
            (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
        (not
            (equal ?NUMBER2 0)))
    (equal
        (AdditionFn
            (MultiplicationFn
                (FloorFn
                    (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))		 Merge.kif 5105-5116
(=>
    (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 17277-17283
(=>
    (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 17289-17295
(=>
    (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 17265-17271
(=>
    (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 17253-17259
(=>
    (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 4721-4722


Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree


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