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)就是这些数字的算术和。") Merge.kif 4864-4865
(documentation AdditionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers.") Merge.kif 4861-4863
(domain AdditionFn 1 Quantity) Merge.kif 4858-4858 加法函数 的 1 数量 是 数量instance
(domain AdditionFn 2 Quantity) Merge.kif 4859-4859 加法函数 的 2 数量 是 数量instance
(identityElement AdditionFn 0) Merge.kif 5386-5386 0 是 加法函数 的单位元
(instance AdditionFn AssociativeFunction) Merge.kif 4854-4854 加法函数结合函数instance
(instance AdditionFn BinaryFunction) Merge.kif 4853-4853 加法函数二元函数instance
(instance AdditionFn CommutativeFunction) Merge.kif 4855-4855 加法函数交换函数instance
(instance AdditionFn TotalValuedRelation) Merge.kif 4857-4857 加法函数总值关系instance
(range AdditionFn Quantity) Merge.kif 4860-4860 加法函数range数量 的实例

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


(format ChineseLanguage AdditionFn "(%*[+])") chinese_format.kif 682-682
(format EnglishLanguage AdditionFn "(%*[+])") english_format.kif 425-425
(termFormat ChineseLanguage AdditionFn "加法函数") chinese_format.kif 683-683 termFormat ChineseLanguage, 加法函数 and "加法函数"
(termFormat EnglishLanguage AdditionFn "addition") domainEnglishFormat.kif 1337-1337 termFormat EnglishLanguage, 加法函数 and "addition"

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


(=>
    (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 1166-1175
(=>
    (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 1215-1224
(=>
    (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
                (CurrencyFn ?BondAccount))
            (transactionAmount ?Payment ?Total))))
FinancialOntology.kif 2264-2278
(=>
    (and
        (instance ?Deposit Deposit)
        (time ?Deposit ?TimeOfDeposit)
        (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-437
(=>
    (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
-------------------------


(<=>
    (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 average 串列 and 实数 若且唯若 有存在 另一个 串列 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 正整数 第四 正整数 equal 那个 另外 串列 的长度 和 那个 实数 equal 那个 另外 串列 的第 那个 第四 正整数 几个元素 和 那个 第四 正整数
(<=>
    (equal
        (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (equal
        (AdditionFn
            (MultiplicationFn
                (FloorFn
                    (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
Merge.kif 5261-5263 整数 模除 另一个 整数 equal 第三 整数 若且唯若 (取 那个 整数那个 另外 整数 的底整数 和 那个 另外 整数那个 第三 整数) equal 那个 整数
(=>
    (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 3619-3636
(=>
    (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 6113-6126
(=>
    (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 6099-6111
(=>
    (and
        (instance ?UNIT UnitOfArea)
        (landAreaOnly ?AREA
            (MeasureFn ?LAND ?UNIT))
        (waterAreaOnly ?AREA
            (MeasureFn ?WATER ?UNIT)))
    (totalArea ?AREA
        (MeasureFn
            (AdditionFn ?LAND ?WATER) ?UNIT)))
Geography.kif 559-564
(=>
    (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 17554-17556
(=>
    (equal
        (RelativeTimeFn ?TIME1 EasternTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 5 HourDuration))))
Merge.kif 17563-17565
(=>
    (equal
        (RelativeTimeFn ?TIME1 MountainTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 7 HourDuration))))
Merge.kif 17545-17547
(=>
    (equal
        (RelativeTimeFn ?TIME1 PacificTimeZone) ?TIME2)
    (equal ?TIME2
        (AdditionFn ?TIME1
            (MeasureFn 8 HourDuration))))
Merge.kif 17536-17538

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


(forall (?NUMBER)
    (equal
        (SuccessorFn ?NUMBER)
        (AdditionFn ?NUMBER 1)))
Merge.kif 4867-4868 对所有 整数 (那个 整数+1) equal (那个 整数 和 1)


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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners