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 4485-4487
(domain AdditionFn 1 Quantity) Merge.kif 4481-4481 The number 1 argument of addition is an instance of quantity
(domain AdditionFn 2 Quantity) Merge.kif 4482-4482 The number 2 argument of addition is an instance of quantity
(identityElement AdditionFn 0) Merge.kif 4970-4970 0 is an identity element of addition
(instance AdditionFn AssociativeFunction) Merge.kif 4477-4477 Addition is an instance of associative function
(instance AdditionFn BinaryFunction) Merge.kif 4476-4476 Addition is an instance of binary function
(instance AdditionFn CommutativeFunction) Merge.kif 4478-4478 Addition is an instance of commutative function
(instance AdditionFn TotalValuedRelation) Merge.kif 4480-4480 Addition is an instance of total valued relation
(range AdditionFn Quantity) Merge.kif 4483-4483 The range of addition is an instance of quantity

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


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

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 3036-3057
(=>
    (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 1165-1174
(=>
    (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 1214-1223
(=>
    (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 2263-2277
(=>
    (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 531-540

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 2972-2988 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 285-306 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 4850-4852 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 3632-3649
(=>
    (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 5638-5651
(=>
    (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 5624-5636
(=>
    (and
        (equal ?A
            (ListSumFn ?L))
        (greaterThan
            (ListLengthFn ?L) 1))
    (equal ?A
        (AdditionFn
            (FirstFn ?L)
            (ListSumFn
                (SubListFn 2
                    (ListLengthFn ?L) ?L)))))
Merge.kif 3111-3121
(=>
    (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 3036-3057
(=>
    (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 3078-3090
(=>
    (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 504-511
(=>
    (and
        (totalLengthOfHighwaySystem ?AREA ?LENGTH)
        (lengthOfPavedHighway ?AREA ?LENGTH1)
        (lengthOfUnpavedHighway ?AREA ?LENGTH2))
    (equal ?LENGTH
        (AdditionFn ?LENGTH1 ?LENGTH2)))
Transportation.kif 497-502
(=>
    (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 6189-6197
(=>
    (equal
        (RelativeTimeFn ?TIME1 CentralTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 6 HourDuration))))
Merge.kif 15980-15982
(=>
    (equal
        (RelativeTimeFn ?TIME1 EasternTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 5 HourDuration))))
Merge.kif 15988-15990
(=>
    (equal
        (RelativeTimeFn ?TIME1 MountainTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 7 HourDuration))))
Merge.kif 15972-15974
(=>
    (equal
        (RelativeTimeFn ?TIME1 PacificTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 8 HourDuration))))
Merge.kif 15964-15966

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


(forall (?NUMBER)
    (equal
        (SuccessorFn ?NUMBER)
        (AdditionFn ?NUMBER 1)))
Merge.kif 4489-4490 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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners