SubtractionFn - Sigma Knowledge base Browser

Browsing Interface : Welcome guest : log in

[ Home | Graph | ] KB: Language:
Formal Language:

KB Term:			Term intersection

English Word:

Sigma KEE - SubtractionFn

SubtractionFn

appearance as argument number 1

(documentation SubtractionFn ChineseLanguage "如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (SubtractionFn ?NUMBER1 ?NUMBER2) 就是 ?NUMBER1 和 ?NUMBER2 的算术差，即使 ?NUMBER1 减 ?NUMBER2，除了在 ?NUMBER1 等于0时，那么(SubtractionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER2 的负数。")	chinese_format.kif 2216-2219
(documentation SubtractionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (SubtractionFn ?NUMBER1 ?NUMBER2) is the arithmetical difference between ?NUMBER1 and ?NUMBER2, i.e. ?NUMBER1 minus ?NUMBER2. An exception occurs when ?NUMBER1 is equal to 0, in which case (SubtractionFn ?NUMBER1 ?NUMBER2) is the negation of ?NUMBER2.")	Merge.kif 4499-4503
(domain SubtractionFn 1 Quantity)	Merge.kif 4495-4495	The number 1 argument of subtraction is an instance of quantity
(domain SubtractionFn 2 Quantity)	Merge.kif 4496-4496	The number 2 argument of subtraction is an instance of quantity
(identityElement SubtractionFn 0)	Merge.kif 4971-4971	0 is an identity element of subtraction
(instance SubtractionFn BinaryFunction)	Merge.kif 4492-4492	Subtraction is an instance of binary function
(instance SubtractionFn TotalValuedRelation)	Merge.kif 4494-4494	Subtraction is an instance of total valued relation
(range SubtractionFn Quantity)	Merge.kif 4497-4497	The range of subtraction is an instance of quantity

appearance as argument number 2

(format ChineseLanguage SubtractionFn "(%*[-])")	chinese_format.kif 684-684
(format EnglishLanguage SubtractionFn "(%*[-])")	english_format.kif 689-689
(termFormat ChineseLanguage SubtractionFn "减法")	domainEnglishFormat.kif 55747-55747
(termFormat ChineseLanguage SubtractionFn "减法函数")	chinese_format.kif 685-685
(termFormat ChineseTraditionalLanguage SubtractionFn "減法")	domainEnglishFormat.kif 55746-55746
(termFormat EnglishLanguage SubtractionFn "subtraction")	domainEnglishFormat.kif 55745-55745

antecedent

(<=> (exists (?Income ?Tax ?TaxAmount) (and (incomeEarned ?Agent ?Income ?Activity) (amountCharged ?Tax ?TaxAmount) (causes ?Activity ?Tax) (equal ?ATIncome (SubtractionFn ?Income ?TaxAmount)))) (afterTaxIncome ?Agent ?ATIncome ?Activity))	FinancialOntology.kif 3229-3236	There exist a currency measure, a chargingA fee and the chargingA feeAmount such that a human is income earned the currency measure for an organizational process and the chargingA feeAmount is the amount charged in the chargingA fee and the organizational process causes the chargingA fee and a third currency measure is equal to (the currency measure and the chargingA feeAmount) if and only if the after tax income derived by the human from the organizational process is the third currency measure
(=> (and (currentAccountBalance ?Account ?Date (MeasureFn ?Balance UnitedStatesDollar)) (lessThan ?Balance 0) (equal ?Overdraft (SubtractionFn 0 ?Balance))) (overdraft ?Account (MeasureFn ?Overdraft UnitedStatesDollar) ?Date))	FinancialOntology.kif 732-737	If a financial account current account balance a day for a real number united states dollar(s) and the real number is less than 0 and another real number is equal to (0 and the real number), then the financial account is overdraft the other real number united states dollar(s) for the day
(=> (and (downPayment ?Loan ?Amount) (loanForPurchase ?Loan ?Purchase) (monetaryValue ?Purchase ?Value) (equal ?Balance (SubtractionFn ?Value ?Amount))) (originalBalance ?Loan ?Balance))	FinancialOntology.kif 766-772	If a currency measure is a down payment of a loan and an object is a loan for purchase of the loan and value of the object is another currency measure and a third currency measure is equal to (the other currency measure and the currency measure), then the third currency measure is an original balance of the loan
(=> (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)) (equal (SubtractionFn ?E ?S) 0)) (equal ?R NullList))	Merge.kif 3058-3065	If a list is equal to the sub-list from an integer to another integer of another list and (the other integer and the integer) is equal to 0, then the list is equal to null list
(=> (and (equal ?R (SubListFn ?S ?E ?L)) (equal (SubtractionFn ?E ?S) 1)) (equal ?R (ListFn (ListOrderFn ?L ?S))))	Merge.kif 3067-3076	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 equal to 1, then the list is equal to (the positive integerth element of the other list)
(=> (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 ?DAY1 (DayFn ?NUMBER1 ?MONTH)) (instance ?DAY2 (DayFn ?NUMBER2 ?MONTH)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?DAY1 ?DAY2))	Merge.kif 8030-8035	If a time interval is an instance of the day a positive integer and another time interval is an instance of the day another positive integer and (the other positive integer and the positive integer) is equal to 1, then the time interval meets the other time interval
(=> (and (instance ?HOUR1 (HourFn ?NUMBER1 ?DAY)) (instance ?HOUR2 (HourFn ?NUMBER2 ?DAY)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?HOUR1 ?HOUR2))	Merge.kif 8056-8061	If a time interval is an instance of the hour a nonnegative integer and another time interval is an instance of the hour another nonnegative integer and (the other nonnegative integer and the nonnegative integer) is equal to 1, then the time interval meets the other time interval
(=> (and (instance ?MINUTE1 (MinuteFn ?NUMBER1 ?HOUR)) (instance ?MINUTE2 (MinuteFn ?NUMBER2 ?HOUR)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?MINUTE1 ?MINUTE2))	Merge.kif 8083-8088	If a time interval is an instance of the minute a nonnegative integer and another time interval is an instance of the minute another nonnegative integer and (the other nonnegative integer and the nonnegative integer) is equal to 1, then the time interval meets the other time interval
(=> (and (instance ?Payment Payment) (origin ?Payment (CurrencyFn ?Account)) (instance ?Account FinancialAccount) (transactionAmount ?Payment ?Amount) (currentAccountBalance ?Account (ImmediatePastFn (WhenFn ?Payment)) ?Balance1) (equal ?Balance2 (SubtractionFn ?Balance1 ?Amount))) (currentAccountBalance ?Account (ImmediateFutureFn (WhenFn ?Payment)) ?Balance2))	FinancialOntology.kif 408-416	If a financial transaction is an instance of payment and the financial transaction originates at the currency of a financial account and the financial account is an instance of 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 the time of existence of the financial transaction for the third currency measure
(=> (and (instance ?SECOND1 (SecondFn ?NUMBER1 ?MINUTE)) (instance ?SECOND2 (SecondFn ?NUMBER2 ?MINUTE)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?SECOND1 ?SECOND2))	Merge.kif 8110-8115	If a time interval is an instance of the second a positive integer and another time interval is an instance of the second another positive integer and (the other positive integer and the positive integer) is equal to 1, then the time interval meets the other time interval
(=> (and (instance ?Withdrawal Withdrawal) (instance ?Account FinancialAccount) (origin ?Withdrawal ?Account) (transactionAmount ?Withdrawal ?Amount) (currentAccountBalance ?Account (ImmediatePastFn (WhenFn ?Withdrawal)) ?Balance1) (equal ?Balance2 (SubtractionFn ?Balance1 ?Amount))) (currentAccountBalance ?Account (ImmediateFutureFn (FutureFn ?Withdrawal)) ?Balance2))	FinancialOntology.kif 449-457	If a financial transaction is an instance of withdrawal and a financial account is an instance of financial account and the financial transaction originates at 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 (instance ?YEAR1 Year) (instance ?YEAR2 Year) (equal (SubtractionFn ?YEAR2 ?YEAR1) (MeasureFn 1 YearDuration))) (meetsTemporally ?YEAR1 ?YEAR2))	Merge.kif 8175-8180	If a time interval is an instance of year and another time interval is an instance of year and (the other time interval and the time interval) is equal to 1 year duration(s), then the time interval meets the other time interval
(=> (and (orientation ?OBJ ?REGION Outside) (instance ?ZONE (PerimeterAreaFn ?REGION)) (instance ?ZONE UniformPerimeterArea) (width ?ZONE (MeasureFn ?LIMIT ?UNIT)) (distance ?OBJ ?REGION (MeasureFn ?FAR ?UNIT)) (instance ?UNIT UnitOfMeasure) (greaterThan (SubtractionFn ?FAR ?LIMIT) 0)) (not (located ?OBJ ?ZONE)))	Geography.kif 862-871	If an object is outside to a region and another object is an instance of the perimeter area of the region and the other object is an instance of uniform perimeter area and the width of the other object is a real number an unit of measure(s) and the distance between the object and the region is another real number the unit of measure(s) and the unit of measure is an instance of unit of measure and (the other real number and the real number) is greater than 0, then the object is not located at the other object
(=> (and (orientation ?OBJ ?REGION Outside) (instance ?ZONE (PerimeterAreaFn ?REGION)) (instance ?ZONE UniformPerimeterArea) (width ?ZONE (MeasureFn ?LIMIT ?UNIT)) (distance ?OBJ ?REGION (MeasureFn ?FAR ?UNIT)) (instance ?UNIT UnitOfMeasure) (lessThanOrEqualTo (SubtractionFn ?FAR ?LIMIT) 0)) (located ?OBJ ?ZONE))	Geography.kif 851-860	If an object is outside to a region and another object is an instance of the perimeter area of the region and the other object is an instance of uniform perimeter area and the width of the other object is a real number an unit of measure(s) and the distance between the object and the region is another real number the unit of measure(s) and the unit of measure is an instance of unit of measure and (the other real number and the real number) is less than or equal to 0, then the object is located at the other object

consequent

(<=> (and (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber)) (or (and (instance ?NUMBER1 NonnegativeRealNumber) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeRealNumber) (equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1)))))	Merge.kif 4537-4548	The absolute value of a real number is equal to a nonnegative real number and the real number is an instance of real number and the nonnegative real number is an instance of real number if and only if the real number is an instance of nonnegative real number and the real number is equal to the nonnegative real number or the real number is an instance of negative real number and the nonnegative real number is equal to (0 and the real number)
(<=> (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 (MigrantsPerThousandFn ?AREA (YearFn ?YEAR)) ?REALNUMBER) (and (equal (SubtractionFn ?YEAR ?PREVIOUSYEAR) 1) (holdsDuring (YearFn ?YEAR) (equal (PopulationFn ?AREA) ?POPULATION)) (equal (DivisionFn ?POPULATION 1000) ?THOUSANDS) (equal ?IMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring (YearFn ?PREVIOUSYEAR) (not (inhabits ?PERSON ?AREA))) (holdsDuring (YearFn ?YEAR) (inhabits ?PERSON ?AREA)))))) (equal ?EMMIGRATION (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (holdsDuring (YearFn ?PREVIOUSYEAR) (inhabits ?PERSON ?AREA)) (holdsDuring (YearFn ?YEAR) (not (inhabits ?PERSON ?AREA))))))) (equal (SubtractionFn ?IMMIGRATION ?EMMIGRATION) ?MIGRATIONCOUNT) (equal (DivisionFn ?MIGRATIONCOUNT ?THOUSANDS) ?REALNUMBER)))	People.kif 174-202	The migrants per thousand of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and a quantity) is equal to 1 and the population of the geopolitical area is equal to another quantity holds during the year the integer and the other quantity and 1000 is equal to a third quantity and another integer is equal to the number of instances in the class described by a symbolic string and a third integer is equal to the number of instances in the class described by the symbolic string and (the other integer and the third integer) is equal to a fourth quantity and the fourth quantity and the third quantity is equal to the real number
(<=> (equal (PopulationGrowthFn ?AREA (YearFn ?YEAR)) ?ADJUSTEDPERCENT) (and (equal (SubtractionFn ?YEAR ?PREVIOUSYEAR) 1) (holdsDuring (YearFn ?YEAR) (equal (PopulationFn ?AREA) ?POPULATION)) (holdsDuring (YearFn ?PREVIOUSYEAR) (equal (PopulationFn ?AREA) ?PREVIOUSPOPULATION)) (equal (DivisionFn ?POPULATION ?PREVIOUSPOPULATION) ?PERCENT) (equal (SubtractionFn ?PERCENT 1) ?ADJUSTEDPERCENT)))	People.kif 77-86	The population growth of a geopolitical area and the year an integer is equal to a real number if and only if (the integer and another integer) is equal to 1 and the population of the geopolitical area is equal to a quantity holds during the year the integer and the population of the geopolitical area is equal to another quantity holds during the year the other integer and the quantity and the other quantity is equal to a third quantity and (the third quantity and 1) is equal to the real number
(=> (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 (instance ?QUANTITY1 Quantity) (instance ?QUANTITY2 Quantity)) (equal (LiftFn ?QUANTITY1 ?QUANTITY2) (DivisionFn (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2)))	UXExperimentalTerms.kif 4761-4769	If a quantity is an instance of quantity and another quantity is an instance of quantity, then the financial improvement percentage of the quantity over the other quantity is equal to (the quantity and the other quantity) and the other quantity
(=> (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)

statement

(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree))	Merge.kif 6681-6683	A real number celsius degree(s) is equal to (the real number and 32) and 1.8 fahrenheit degree(s)
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree))	Merge.kif 6677-6679	A real number celsius degree(s) is equal to (the real number and 273.15) kelvin degree(s)
(equal (ReachingMilitaryAgeAnnuallyMaleFn ?AREA ?YEAR) (CardinalityFn (KappaFn ?PERSON (and (instance ?PERSON Human) (attribute ?PERSON Male) (militaryAge ?AREA ?MILITARYAGE) (equal ?AGEMINUSONE (SubtractionFn ?AGE 1)) (holdsDuring ?YEAR (or (age ?PERSON ?AGEMINUSONE) (age ?PERSON ?AGE))) (equal ?AGE ?MILITARYAGE) (inhabits ?PERSON ?AREA)))))	Military.kif 928-941	The reaching military age annually male of a geopolitical area and a year is equal to the number of instances in the class described by a symbolic string
(forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1)))	Merge.kif 4505-4506	For all an integer (the integer+2) 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