AdditionFn - Sigma Knowledge base Browser

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	If a symbolic string is equal to the reverse of another symbolic string and a nonnegative integer is equal to the length of the other symbolic string and the nonnegative integer is greater than 1 and another nonnegative integer is greater than 0 and the other nonnegative integer is less than the nonnegative integer and an integer is equal to the ceiling of (the nonnegative integer and 1) and 2 and the other nonnegative integerEW is equal to ((the integer and the other nonnegative integer) and the integer) and a third symbolic string is equal to the sub-string of the other symbolic string from the other nonnegative integer to (1 and the other nonnegative integer), then the third symbolic string is equal to the sub-string of the symbolic string from the other nonnegative integerEW to (1 and the other nonnegative integerEW)
(=> (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	If menopause is an attribute of a human holds during a time interval and a number is a birthdate of the human and another number is equal to (year duration 49 and the number) and a third number is equal to (year duration 52 and the number) and a time point is equal to the beginning of the time interval, then the statement the time point is greater than the other number and the third number is greater than the time point has the modal force of likely
(=> (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	If a financial account is an instance of credit account and a cognitive agent holds account the financial account and a number is a principal amount of the financial account and a time interval is an agreement period of the financial account and the financial account is interest earned an interest for the time interval and another number is equal to (the number and the interest), then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
(=> (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	If a loan is an instance of loan and the loan is the borrower of a cognitive agent and a number is a principal amount of the loan and a time interval is an agreement period of the loan and the loan is interest earned an interest for the time interval and another number is equal to (the number and the interest), then the cognitive agent is obliged to perform tasks of type the class described by a symbolic string
(=> (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	If a financial asset is an instance of zero coupon bond and a day is a maturity date of the account of the financial asset and the financial assetHolder possesses the financial asset and a number is a principal amount of the account of the financial asset and a time interval is an agreement period of the account of the financial asset and the account of the financial asset is interest earned an interest for the time interval and another number is equal to (the number and the interest), then there exists a financial transaction such that the financial transaction is an instance of payment and the financial transaction ends up at the financial assetHolder and the financial transaction originates at the account of the financial asset and the other number is a transaction amount of the financial transaction
(=> (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	If a financial transaction is an instance of deposit and a financial account is an instance of financial account and the financial transaction ends up at the currency of the financial account and a number is a transaction amount of the financial transaction and the financial account current account balance immediately before the time of existence of the financial transaction for another number and a third number is equal to (the other number and the number), then the financial account current account balance immediately after after the financial transaction for the third number
(=> (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	If a number is a principal amount of a financial account and another number is a fixed interest rate of the financial account and the financial account compound interest an interest for a time interval and the other number-Decimal is equal to the other number and 100 and a real number is equal to (1 and the other number-Decimal) and another real number is equal to the real number raised to the power the magnitude of the time interval and a third number is equal to the other real number and the number, then the interest is equal to (the third number and the number)

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 if the positive integer is less than or equal to length of the other list and the other positive integer is less than or equal to length of the third list and the positive integer is an instance of positive integer and the other positive integer is an instance of positive integer, then the positive integerth element of the list is equal to the positive integerth element of the other list and (length of the other list and the other positive integer)th element of the list is equal to the other positive integerth element of the third list
(<=> (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 if the positive integer is a member of the other list, then there exist a number, the numberMINUSONE,, , another positive integer and a third positive integer such that the number is greater than 1 and the number is less than or equal to length of the other list and the positive integerth element of the other list is equal to the number and the other positive integer is a member of the list and the number is equal to the other positive integerth element of the list and the third positive integer is a member of the other list and the numberMINUSONE is equal to (the number and 1) and the numberMINUSONE is equal to the third positive integerth element of the other list and the positive integer is equal to (the other positive integer and the third 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	If a physical courseWRT magnetic north another physical for a number and the physical is partly located in a geographic area and the other physical is partly located in the geographic area and the geographic area magnetic variation another number for a directional attribute, then there exist a third number and a plane angle measure such that if the directional attribute is equal to east and the third number is equal to (the number and the other number), then the physical courseWRT true north the other physical for the plane angle measure and if the directional attribute is equal to west and the third number is equal to (the number and the other number), then the physical courseWRT true north the other physical for the plane angle measure
(=> (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	If the value of a graph path is equal to a real number and a graph arc is a part of the graph path and another graph arc is a part of the graph path and the value of the graph arc is another real number and the value of the other graph arc is a third real number and for all a graph element if the graph element is a part of the graph path, then the graph element is equal to the graph arc or the graph element is equal to the other graph arc , then the value of the graph path is equal to (the other real number and the third real number)
(=> (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	If the value of a graph path is equal to a real number and another graph path is a subgraph of the graph path and a graph arc is a part of the graph path and the value of the graph arc is another real number and for all a graph element if the graph element is a part of the graph path, then the graph element is a part of the other graph path or the graph element is equal to the graph arc , then the real number is equal to (the value of the other graph path and the other real number)
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L)))))	Merge.kif 3182-3192	If a real number is equal to the sum of a list and length of the list is greater than 1, then the real number is equal to (the first of the list and the sum of the sub-list from 2 to length of the list of the list)
(=> (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	If a symbolic string is equal to the reverse of another symbolic string and a nonnegative integer is equal to the length of the other symbolic string and the nonnegative integer is greater than 1 and another nonnegative integer is greater than 0 and the other nonnegative integer is less than the nonnegative integer and an integer is equal to the ceiling of (the nonnegative integer and 1) and 2 and the other nonnegative integerEW is equal to ((the integer and the other nonnegative integer) and the integer) and a third symbolic string is equal to the sub-string of the other symbolic string from the other nonnegative integer to (1 and the other nonnegative integer), then the third symbolic string is equal to the sub-string of the symbolic string from the other nonnegative integerEW to (1 and the other nonnegative integerEW)
(=> (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	If a list is equal to the sub-list from a positive integer to an integer of another list and (the integer and the positive integer) is greater than 1, then the list is equal to the list composed of (the positive integerth element of the other list) and the sub-list from (1 and the positive integer) to the integer of the other list
(=> (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	If a number is equal to VarianceAverageFn of a list with the mean of another number and length of the list is greater than 1, then the number is equal to (VarianceAverageFn of 1th element of the list with the mean of the other number and VarianceAverageFn of the sub-list from 2 to length of the list of the list with the mean of the other number)
(=> (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	If an unit of measure is an instance of UnitOfArea and a real number the unit of measure(s) is a land area only of a geographic area and another real number the unit of measure(s) is a water area only of the geographic area, then (the real number and the other real number) the unit of measure(s) is a total area of the geographic area
(=> (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	If a real number an unit of measure(s) is a total length of highway system of a geographic area and the real number1 the unit of measure(s) is a length of paved highway of the geographic area and the real number2 the unit of measure(s) is a length of unpaved highway of the geographic area and the unit of measure is an instance of UnitOfLength, then (the real number1 and the real number2) the unit of measure(s) is a total length of highway system of the geographic area
(=> (and (totalLengthOfHighwaySystem ?AREA ?LENGTH) (lengthOfPavedHighway ?AREA ?LENGTH1) (lengthOfUnpavedHighway ?AREA ?LENGTH2)) (equal ?LENGTH (AdditionFn ?LENGTH1 ?LENGTH2)))	Transportation.kif 503-508	If a number is a total length of highway system of a geographic area and the number1 is a length of paved highway of the geographic area and the number2 is a length of unpaved highway of the geographic area, then the number is equal to (the number1 and the number2)
(=> (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	If a compound substance is a conjugate of another compound substance, then there exist a positive integer and another positive integer such that the positive integer is a proton number of the other compound substance and the other positive integer is a proton number of the compound substance and the positive integer is equal to (the other positive integer and 1) or the other positive integer is equal to (the positive integer and 1)
(=> (equal (RelativeTimeFn ?TIME1 CentralTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 6 HourDuration))))	Merge.kif 16524-16526	If the time a number in zone central time zone is equal to another number, then the other number is equal to (the number and 6 hour duration(s))
(=> (equal (RelativeTimeFn ?TIME1 EasternTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 5 HourDuration))))	Merge.kif 16532-16534	If the time a number in zone eastern time zone is equal to another number, then the other number is equal to (the number and 5 hour duration(s))
(=> (equal (RelativeTimeFn ?TIME1 MountainTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 7 HourDuration))))	Merge.kif 16516-16518	If the time a number in zone mountain time zone is equal to another number, then the other number is equal to (the number and 7 hour duration(s))
(=> (equal (RelativeTimeFn ?TIME1 PacificTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 8 HourDuration))))	Merge.kif 16505-16510	If the time a number in zone pacific time zone is equal to another number, then the other number is equal to (the number and 8 hour duration(s))
(=> (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	If a positive integer is an instance of consecutive time interval list, then a time interval is equal to the positive integerth element of a number and another time interval is equal to the positive integerth element of (the number and another number) and the beginning of the other time interval is equal to the end of the time interval

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