TreeView Knowledge Base Browser - AdditionFn

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 4495-4497
(domain AdditionFn 1 Quantity)	Merge.kif 4491-4491	The number 1 argument of addition is an instance of quantity
(domain AdditionFn 2 Quantity)	Merge.kif 4492-4492	The number 2 argument of addition is an instance of quantity
(identityElement AdditionFn 0)	Merge.kif 4980-4980	0 is an identity element of addition
(instance AdditionFn AssociativeFunction)	Merge.kif 4487-4487	Addition is an instance of associative function
(instance AdditionFn BinaryFunction)	Merge.kif 4486-4486	Addition is an instance of binary function
(instance AdditionFn CommutativeFunction)	Merge.kif 4488-4488	Addition is an instance of commutative function
(instance AdditionFn TotalValuedRelation)	Merge.kif 4490-4490	Addition is an instance of total valued relation
(range AdditionFn Quantity)	Merge.kif 4493-4493	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	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 (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	If a financial account is an instance of credit account and a cognitive agent holds account the financial account and a currency measure 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 a quantity is equal to (the currency measure 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 1214-1223	If a loan is an instance of loan and the loan is the borrower of a cognitive agent and a currency measure 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 a quantity is equal to (the currency measure 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 2263-2277	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 currency measure 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 currency measure is equal to (the currency measure 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 currency measure 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 currency measure 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 currency measure and a third currency measure is equal to (the other currency measure and the currency measure), then the financial account current account balance immediately after after the financial transaction for the third currency measure
(=> (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	If a currency measure is a principal amount of a financial account and an interest rate is a fixed interest rate of the financial account and the financial account compound interest an interest for a time interval and the interest rate-Decimal is equal to the interest rate and 100 and a real number is equal to (1 and the interest rate-Decimal) and another real number is equal to the real number raised to the power the magnitude of the time interval and a quantity is equal to the other real number and the currency measure, then the interest is equal to (the quantity and the currency measure)

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 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 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 if the positive integer is a member of the other list, then there exist a quantity, the quantityMINUSONE,, , another positive integer and a third positive integer such that the quantity is greater than 1 and the quantity is less than or equal to length of the other list and the positive integerth element of the other list is equal to the quantity and the other positive integer is a member of the list and the quantity 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 quantityMINUSONE is equal to (the quantity and 1) and the quantityMINUSONE 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 4860-4862	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	If a physical courseWRT magnetic north another physical for a plane angle measure 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 plane angle measure for a directional attribute, then there exist a quantity and a third plane angle measure such that if the directional attribute is equal to east and the quantity is equal to (the plane angle measure and the other plane angle measure), then the physical courseWRT true north the other physical for the third plane angle measure and if the directional attribute is equal to west and the quantity is equal to (the plane angle measure and the other plane angle measure), then the physical courseWRT true north the other physical for the third 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 5648-5661	If the value of a graph path is equal to a quantity 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 quantity and the value of the other graph arc is a third quantity 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 quantity and the third quantity)
(=> (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 5634-5646	If the value of a graph path is equal to a quantity 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 quantity 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 quantity is equal to (the value of the other graph path and the other quantity)
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L)))))	Merge.kif 3111-3121	If a number is equal to the sum of a list and length of the list is greater than 1, then the 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 3036-3057	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 3078-3090	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 (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 504-511	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 497-502	If a length measure is a total length of highway system of a geographic area and the length measure1 is a length of paved highway of the geographic area and the length measure2 is a length of unpaved highway of the geographic area, then the length measure is equal to (the length measure1 and the length measure2)
(=> (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 6195-6203	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 15990-15992	If the time a time position in zone central time zone is equal to another time position, then the other time position is equal to (the time position and 6 hour duration(s))
(=> (equal (RelativeTimeFn ?TIME1 EasternTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 5 HourDuration))))	Merge.kif 15998-16000	If the time a time position in zone eastern time zone is equal to another time position, then the other time position is equal to (the time position and 5 hour duration(s))
(=> (equal (RelativeTimeFn ?TIME1 MountainTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 7 HourDuration))))	Merge.kif 15982-15984	If the time a time position in zone mountain time zone is equal to another time position, then the other time position is equal to (the time position and 7 hour duration(s))
(=> (equal (RelativeTimeFn ?TIME1 PacificTimeZone) ?TIME2) (equal ?TIME2 (AdditionFn ?TIME1 (MeasureFn 8 HourDuration))))	Merge.kif 15974-15976	If the time a time position in zone pacific time zone is equal to another time position, then the other time position is equal to (the time position and 8 hour duration(s))

statement

(forall (?NUMBER)
    (equal
        (SuccessorFn ?NUMBER)
        (AdditionFn ?NUMBER 1)))

Merge.kif 4499-4500

For all an integer (the integer+1) is equal to (the integer and 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