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 4410-4414
(domain SubtractionFn 1 Quantity)	Merge.kif 4406-4406	domain SubtractionFn, 1 and Quantity
(domain SubtractionFn 2 Quantity)	Merge.kif 4407-4407	domain SubtractionFn, 2 and Quantity
(identityElement SubtractionFn 0)	Merge.kif 4883-4883	identityElement SubtractionFn and 0
(instance SubtractionFn AssociativeFunction)	Merge.kif 4403-4403	instance SubtractionFn and AssociativeFunction
(instance SubtractionFn BinaryFunction)	Merge.kif 4402-4402	instance SubtractionFn and BinaryFunction
(instance SubtractionFn TotalValuedRelation)	Merge.kif 4405-4405	instance SubtractionFn and TotalValuedRelation
(range SubtractionFn Quantity)	Merge.kif 4408-4408	range SubtractionFn and 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 55795-55795	termFormat ChineseLanguage, SubtractionFn and "减法"
(termFormat ChineseLanguage SubtractionFn "减法函数")	chinese_format.kif 685-685	termFormat ChineseLanguage, SubtractionFn and "减法函数"
(termFormat ChineseTraditionalLanguage SubtractionFn "減法")	domainEnglishFormat.kif 55794-55794	termFormat ChineseTraditionalLanguage, SubtractionFn and "減法"
(termFormat EnglishLanguage SubtractionFn "subtraction")	domainEnglishFormat.kif 55793-55793	termFormat EnglishLanguage, SubtractionFn and "subtraction"

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 3228-3235	CurrencyMeasure ChargingAFee and ChargingAFeeAmount incomeEarned Human, CurrencyMeasure and OrganizationalProcess amountCharged ChargingAFee and ChargingAFeeAmount causes OrganizationalProcess and ChargingAFee equal CurrencyMeasure and SubtractionFn CurrencyMeasure and ChargingAFeeAmount afterTaxIncome Human, CurrencyMeasure and OrganizationalProcess
(=> (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	currentAccountBalance FinancialAccount, Day and MeasureFn RealNumber and UnitedStatesDollar lessThan RealNumber and 0 equal RealNumber and SubtractionFn 0 and RealNumber overdraft FinancialAccount, MeasureFn RealNumber and UnitedStatesDollar and Day
(=> (and (downPayment ?Loan ?Amount) (loanForPurchase ?Loan ?Purchase) (monetaryValue ?Purchase ?Value) (equal ?Balance (SubtractionFn ?Value ?Amount))) (originalBalance ?Loan ?Balance))	FinancialOntology.kif 766-772	downPayment Loan and CurrencyMeasure loanForPurchase Loan and Object monetaryValue Object and CurrencyMeasure equal CurrencyMeasure and SubtractionFn CurrencyMeasure and CurrencyMeasure originalBalance Loan and CurrencyMeasure
(=> (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	equal SymbolicString and ReverseFn SymbolicString equal NonnegativeInteger and StringLengthFn SymbolicString greaterThan NonnegativeInteger and 1 greaterThan NonnegativeInteger and 0 lessThan NonnegativeInteger and NonnegativeInteger equal Integer and CeilingFn DivisionFn SubtractionFn NonnegativeInteger and 1 and 2 equal NonnegativeIntegerEW and AdditionFn SubtractionFn Integer and NonnegativeInteger and Integer equal SymbolicString and SubstringFn SymbolicString, NonnegativeInteger and AdditionFn 1 and NonnegativeInteger equal SymbolicString and SubstringFn SymbolicString, NonnegativeIntegerEW and AdditionFn 1 and NonnegativeIntegerEW
(=> (and (instance ?DAY1 (DayFn ?NUMBER1 ?MONTH)) (instance ?DAY2 (DayFn ?NUMBER2 ?MONTH)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?DAY1 ?DAY2))	Merge.kif 7939-7944	instance TimeInterval and DayFn PositiveInteger and Month instance TimeInterval and DayFn PositiveInteger and Month equal SubtractionFn PositiveInteger and PositiveInteger and 1 meetsTemporally TimeInterval and TimeInterval
(=> (and (instance ?HOUR1 (HourFn ?NUMBER1 ?DAY)) (instance ?HOUR2 (HourFn ?NUMBER2 ?DAY)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?HOUR1 ?HOUR2))	Merge.kif 7965-7970	instance TimeInterval and HourFn NonnegativeInteger and Day instance TimeInterval and HourFn NonnegativeInteger and Day equal SubtractionFn NonnegativeInteger and NonnegativeInteger and 1 meetsTemporally TimeInterval and TimeInterval
(=> (and (instance ?MINUTE1 (MinuteFn ?NUMBER1 ?HOUR)) (instance ?MINUTE2 (MinuteFn ?NUMBER2 ?HOUR)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?MINUTE1 ?MINUTE2))	Merge.kif 7992-7997	instance TimeInterval and MinuteFn NonnegativeInteger and Hour instance TimeInterval and MinuteFn NonnegativeInteger and Hour equal SubtractionFn NonnegativeInteger and NonnegativeInteger and 1 meetsTemporally TimeInterval and TimeInterval
(=> (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	instance FinancialTransaction and Payment origin FinancialTransaction and CurrencyFn FinancialAccount instance FinancialAccount and FinancialAccount transactionAmount FinancialTransaction and CurrencyMeasure currentAccountBalance FinancialAccount, ImmediatePastFn WhenFn FinancialTransaction and CurrencyMeasure equal CurrencyMeasure and SubtractionFn CurrencyMeasure and CurrencyMeasure currentAccountBalance FinancialAccount, ImmediateFutureFn WhenFn FinancialTransaction and CurrencyMeasure
(=> (and (instance ?SECOND1 (SecondFn ?NUMBER1 ?MINUTE)) (instance ?SECOND2 (SecondFn ?NUMBER2 ?MINUTE)) (equal (SubtractionFn ?NUMBER2 ?NUMBER1) 1)) (meetsTemporally ?SECOND1 ?SECOND2))	Merge.kif 8019-8024	instance TimeInterval and SecondFn PositiveInteger and Minute instance TimeInterval and SecondFn PositiveInteger and Minute equal SubtractionFn PositiveInteger and PositiveInteger and 1 meetsTemporally TimeInterval and TimeInterval
(=> (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	instance FinancialTransaction and Withdrawal instance FinancialAccount and FinancialAccount origin FinancialTransaction and FinancialAccount transactionAmount FinancialTransaction and CurrencyMeasure currentAccountBalance FinancialAccount, ImmediatePastFn WhenFn FinancialTransaction and CurrencyMeasure equal CurrencyMeasure and SubtractionFn CurrencyMeasure and CurrencyMeasure currentAccountBalance FinancialAccount, ImmediateFutureFn FutureFn FinancialTransaction and CurrencyMeasure
(=> (and (instance ?YEAR1 Year) (instance ?YEAR2 Year) (equal (SubtractionFn ?YEAR2 ?YEAR1) (MeasureFn 1 YearDuration))) (meetsTemporally ?YEAR1 ?YEAR2))	Merge.kif 8084-8089	instance TimeInterval and Year instance TimeInterval and Year equal SubtractionFn TimeInterval and TimeInterval and MeasureFn 1 and YearDuration meetsTemporally TimeInterval and TimeInterval
(=> (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	orientation Object, Region and Outside instance Object and PerimeterAreaFn Region instance Object and UniformPerimeterArea width Object and MeasureFn RealNumber and UnitOfMeasure distance Object, Region and MeasureFn RealNumber and UnitOfMeasure instance UnitOfMeasure and UnitOfMeasure greaterThan SubtractionFn RealNumber and RealNumber and 0 located Object and 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	orientation Object, Region and Outside instance Object and PerimeterAreaFn Region instance Object and UniformPerimeterArea width Object and MeasureFn RealNumber and UnitOfMeasure distance Object, Region and MeasureFn RealNumber and UnitOfMeasure instance UnitOfMeasure and UnitOfMeasure lessThanOrEqualTo SubtractionFn RealNumber and RealNumber and 0 located Object and 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 4449-4460	equal AbsoluteValueFn RealNumber and NonnegativeRealNumber instance RealNumber and RealNumber instance NonnegativeRealNumber and RealNumber instance RealNumber and NonnegativeRealNumber equal RealNumber and NonnegativeRealNumber instance RealNumber and NegativeRealNumber equal NonnegativeRealNumber and SubtractionFn 0 and RealNumber
(<=> (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 List and RealNumber List equal ListLengthFn List and ListLengthFn List equal ListOrderFn List and 1 and ListOrderFn List and 1 PositiveInteger inList PositiveInteger and List Quantity QuantityMINUSONE, PositiveInteger and PositiveInteger greaterThan Quantity and 1 lessThanOrEqualTo Quantity and ListLengthFn List equal ListOrderFn List and PositiveInteger and Quantity inList PositiveInteger and List equal Quantity and ListOrderFn List and PositiveInteger inList PositiveInteger and List equal QuantityMINUSONE and SubtractionFn Quantity and 1 equal QuantityMINUSONE and ListOrderFn List and PositiveInteger equal PositiveInteger and AdditionFn PositiveInteger and PositiveInteger equal PositiveInteger and ListLengthFn List equal RealNumber and DivisionFn ListOrderFn List and PositiveInteger and PositiveInteger
(<=> (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	equal MigrantsPerThousandFn GeopoliticalArea and YearFn Integer and RealNumber equal SubtractionFn Integer and Quantity and 1 holdsDuring YearFn Integer and equal PopulationFn GeopoliticalArea and Quantity equal DivisionFn Quantity and 1000 and Quantity equal Integer and CardinalityFn KappaFn SymbolicString and instance SymbolicString and Human holdsDuring YearFn Quantity and inhabits SymbolicString and GeopoliticalArea holdsDuring YearFn Integer and inhabits SymbolicString and GeopoliticalArea equal Integer and CardinalityFn KappaFn SymbolicString and instance SymbolicString and Human holdsDuring YearFn Quantity and inhabits SymbolicString and GeopoliticalArea holdsDuring YearFn Integer and inhabits SymbolicString and GeopoliticalArea equal SubtractionFn Integer and Integer and Quantity equal DivisionFn Quantity and Quantity and RealNumber
(<=> (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	equal PopulationGrowthFn GeopoliticalArea and YearFn Integer and RealNumber equal SubtractionFn Integer and Integer and 1 holdsDuring YearFn Integer and equal PopulationFn GeopoliticalArea and Quantity holdsDuring YearFn Integer and equal PopulationFn GeopoliticalArea and Quantity equal DivisionFn Quantity and Quantity and Quantity equal SubtractionFn Quantity and 1 and RealNumber
(=> (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	courseWRTMagneticNorth Physical, Physical and PlaneAngleMeasure partlyLocated Physical and GeographicArea partlyLocated Physical and GeographicArea magneticVariation GeographicArea, PlaneAngleMeasure and DirectionalAttribute Quantity PlaneAngleMeasure equal DirectionalAttribute and East equal Quantity and AdditionFn PlaneAngleMeasure and PlaneAngleMeasure courseWRTTrueNorth Physical, Physical and PlaneAngleMeasure equal DirectionalAttribute and West equal Quantity and SubtractionFn PlaneAngleMeasure and PlaneAngleMeasure courseWRTTrueNorth Physical, Physical and PlaneAngleMeasure
(=> (and (instance ?QUANTITY1 Quantity) (instance ?QUANTITY2 Quantity)) (equal (LiftFn ?QUANTITY1 ?QUANTITY2) (DivisionFn (SubtractionFn ?QUANTITY1 ?QUANTITY2) ?QUANTITY2)))	UXExperimentalTerms.kif 4761-4769	instance Quantity and Quantity instance Quantity and Quantity equal LiftFn Quantity and Quantity and DivisionFn SubtractionFn Quantity and Quantity and 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	principalAmount FinancialAccount and CurrencyMeasure fixedInterestRate FinancialAccount and InterestRate compoundInterest FinancialAccount, Interest and TimeInterval equal InterestRate-Decimal and DivisionFn InterestRate and 100 equal RealNumber and AdditionFn 1 and InterestRate-Decimal equal RealNumber and ExponentiationFn RealNumber and MagnitudeFn TimeInterval equal Quantity and MultiplicationFn RealNumber and CurrencyMeasure equal Interest and SubtractionFn Quantity and CurrencyMeasure

statement

(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (DivisionFn (SubtractionFn ?NUMBER 32) 1.8) FahrenheitDegree))	Merge.kif 6595-6597	equal MeasureFn RealNumber and CelsiusDegree and MeasureFn DivisionFn SubtractionFn RealNumber and 32 and 1.8 and FahrenheitDegree
(equal (MeasureFn ?NUMBER CelsiusDegree) (MeasureFn (SubtractionFn ?NUMBER 273.15) KelvinDegree))	Merge.kif 6591-6593	equal MeasureFn RealNumber and CelsiusDegree and MeasureFn SubtractionFn RealNumber and 273.15 and KelvinDegree
(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	equal ReachingMilitaryAgeAnnuallyMaleFn GeopoliticalArea and Year and CardinalityFn KappaFn SymbolicString and instance SymbolicString and Human attribute SymbolicString and Male militaryAge GeopoliticalArea and entity equal entity and SubtractionFn entity and 1 holdsDuring Year and age SymbolicString and entity age SymbolicString and entity equal entity and entity inhabits SymbolicString and GeopoliticalArea
(forall (?NUMBER) (equal (PredecessorFn ?NUMBER) (SubtractionFn ?NUMBER 1)))	Merge.kif 4416-4417	Integer equal PredecessorFn Integer and SubtractionFn 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