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 4578-4580
(domain AdditionFn 1 Number) Merge.kif 4574-4574 The number 1 argument of addition is an instance of number
(domain AdditionFn 2 Number) Merge.kif 4575-4575 The number 2 argument of addition is an instance of number
(identityElement AdditionFn 0) Merge.kif 5097-5097 0 is an identity element of addition
(instance AdditionFn AssociativeFunction) Merge.kif 4570-4570 Addition is an instance of associative function
(instance AdditionFn BinaryFunction) Merge.kif 4569-4569 Addition is an instance of binary function
(instance AdditionFn CommutativeFunction) Merge.kif 4571-4571 Addition is an instance of commutative function
(instance AdditionFn TotalValuedRelation) Merge.kif 4573-4573 Addition is an instance of total valued relation
(range AdditionFn Number) Merge.kif 4576-4576 The range of addition is an instance of number

appearance as argument number 2
-------------------------


(format ChineseLanguage AdditionFn "(%*[+])") chinese_format.kif 682-682
(format EnglishLanguage AdditionFn "(%*[+])") english_format.kif 684-684
(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

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)
        (equal ?A1
            (AdditionFn
                (YearDuration 49) ?B))
        (equal ?A2
            (AdditionFn
                (YearDuration 52) ?B))
        (equal ?START
            (BeginFn ?T)))
    (modalAttribute
        (and
            (greaterThan ?START ?A1)
            (greaterThan ?A2 ?START)) Likely))
Mid-level-ontology.kif 23209-23226
(=>
    (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 1178-1187
(=>
    (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 1227-1236
(=>
    (and
        (instance ?Bond ZeroCouponBond)
        (maturityDate
            (AccountFn ?Bond) ?Date)
        (possesses ?BondHolder ?Bond)
        (principalAmount
            (AccountFn ?Bond) ?Principal)
        (agreementPeriod
            (AccountFn ?Bond) ?Period)
        (interestEarned
            (AccountFn ?Bond) ?Interest ?Period)
        (equal ?Total
            (AdditionFn ?Principal ?Interest)))
    (exists (?Payment)
        (and
            (instance ?Payment Payment)
            (destination ?Payment ?BondHolder)
            (origin ?Payment
                (AccountFn ?Bond))
            (transactionAmount ?Payment ?Total))))
FinancialOntology.kif 2303-2317
(=>
    (and
        (instance ?Deposit Deposit)
        (instance ?Account FinancialAccount)
        (destination ?Deposit
            (CurrencyFn ?Account))
        (transactionAmount ?Deposit ?Amount)
        (currentAccountBalance ?Account
            (ImmediatePastFn
                (WhenFn ?Deposit)) ?Balance1)
        (equal ?Balance2
            (AdditionFn ?Balance1 ?Amount)))
    (currentAccountBalance ?Account
        (ImmediateFutureFn
            (FutureFn ?Deposit)) ?Balance2))
FinancialOntology.kif 428-436
(=>
    (and
        (principalAmount ?Account ?Balance)
        (fixedInterestRate ?Account ?Rate)
        (compoundInterest ?Account ?Interest ?Period)
        (equal ?Rate-Decimal
            (DivisionFn ?Rate 100))
        (equal ?Add
            (AdditionFn 1 ?Rate-Decimal))
        (equal ?Exponent
            (ExponentiationFn ?Add
                (MagnitudeFn ?Period)))
        (equal ?Multiply
            (MultiplicationFn ?Exponent ?Balance)))
    (equal ?Interest
        (SubtractionFn ?Multiply ?Balance)))
FinancialOntology.kif 532-541

consequent
-------------------------


(<=>
    (and
        (equal ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
        (not
            (equal ?LIST1 NullList))
        (not
            (equal ?LIST2 NullList)))
    (forall (?NUMBER1 ?NUMBER2)
        (=>
            (and
                (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 3012-3028 A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer
(<=>
    (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 289-310 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
(<=>
    (equal
        (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (equal
        (AdditionFn
            (MultiplicationFn
                (FloorFn
                    (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 4943-4945 An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer
(=>
    (and
        (courseWRTMagneticNorth ?OBJ1 ?OBJ2 ?MAGDEGREE)
        (partlyLocated ?OBJ1 ?AREA)
        (partlyLocated ?OBJ2 ?AREA)
        (magneticVariation ?AREA ?DEGREE ?DIRECTION))
    (exists (?DIFFDEGREE ?TRUEDEGREE)
        (and
            (=>
                (and
                    (equal ?DIRECTION East)
                    (equal ?DIFFDEGREE
                        (AdditionFn ?MAGDEGREE ?DEGREE)))
                (courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE))
            (=>
                (and
                    (equal ?DIRECTION West)
                    (equal ?DIFFDEGREE
                        (SubtractionFn ?MAGDEGREE ?DEGREE)))
                (courseWRTTrueNorth ?OBJ1 ?OBJ2 ?TRUEDEGREE)))))
Geography.kif 3675-3692
(=>
    (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 5762-5775
(=>
    (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 5748-5760
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Merge.kif 3182-3192
(=>
    (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 3118-3130
(=>
    (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 1452-1464
(=>
    (and
        (instance ?UNIT UnitOfArea)
        (landAreaOnly ?AREA
            (MeasureFn ?LAND ?UNIT))
        (waterAreaOnly ?AREA
            (MeasureFn ?WATER ?UNIT)))
    (totalArea ?AREA
        (MeasureFn
            (AdditionFn ?LAND ?WATER) ?UNIT)))
Geography.kif 562-567
(=>
    (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 ?LENGTH)
        (lengthOfPavedHighway ?AREA ?LENGTH1)
        (lengthOfUnpavedHighway ?AREA ?LENGTH2))
    (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 6146-6154
(=>
    (equal
        (RelativeTimeFn ?TIME1 CentralTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 6 HourDuration))))
Merge.kif 16524-16526
(=>
    (equal
        (RelativeTimeFn ?TIME1 EasternTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 5 HourDuration))))
Merge.kif 16532-16534
(=>
    (equal
        (RelativeTimeFn ?TIME1 MountainTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 7 HourDuration))))
Merge.kif 16516-16518
(=>
    (equal
        (RelativeTimeFn ?TIME1 PacificTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 8 HourDuration))))
Merge.kif 16505-16510
(=>
    (instance ?LIST ConsecutiveTimeIntervalList)
    (and
        (equal ?T1
            (ListOrderFn ?N ?LIST))
        (equal ?T2
            (ListOrderFn
                (AdditionFn ?N ?1) ?LIST))
        (equal
            (BeginFn ?T2)
            (EndFn ?T1))))
Weather.kif 1934-1943

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


(forall (?NUMBER)
    (equal
        (SuccessorFn ?NUMBER)
        (AdditionFn ?NUMBER 1)))
Merge.kif 4582-4583 For all an integer (the integer+1) is equal to (the integer and 1)


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