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
-------------------------


s__documentation(s__SubtractionFn__m,s__ChineseLanguage,'如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (SubtractionFn ?NUMBER1 ?NUMBER2) 就是 ?NUMBER1 和 ?NUMBER2 的算术差，即使 ?NUMBER1 减 ?NUMBER2，除了在 ?NUMBER1 等于0时，那么(SubtractionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER2 的负数。')

 Merge.kif 4882-4885
s__documentation(s__SubtractionFn__m,s__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 4877-4881
s__domain(s__SubtractionFn__m,1,s__Quantity)

 Merge.kif 4874-4874 The number 1 argument of subtraction is an instance of quantity
s__domain(s__SubtractionFn__m,2,s__Quantity)

 Merge.kif 4875-4875 The number 2 argument of subtraction is an instance of quantity
s__identityElement(s__SubtractionFn__m,0)

 Merge.kif 5387-5387 0 is an identity element of subtraction
s__instance(s__AssociativeFunction,s__SetOrClass)

s__instance(s__SubtractionFn__m,s__AssociativeFunction)

 Merge.kif 4871-4871 Subtraction is an instance of associative function
s__instance(s__BinaryFunction,s__SetOrClass)

s__instance(s__SubtractionFn__m,s__BinaryFunction)

 Merge.kif 4870-4870 Subtraction is an instance of binary function
s__instance(s__TotalValuedRelation,s__SetOrClass)

s__instance(s__SubtractionFn__m,s__TotalValuedRelation)

 Merge.kif 4873-4873 Subtraction is an instance of total valued relation
s__range(s__SubtractionFn__m,s__Quantity)

 Merge.kif 4876-4876 The range of subtraction is an instance of quantity

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


s__format(s__ChineseLanguage,s__SubtractionFn__m,'(%*[-])')

 chinese_format.kif 684-684
s__format(s__EnglishLanguage,s__SubtractionFn__m,'(%*[-])')

 english_format.kif 426-426
s__termFormat(s__ChineseLanguage,s__SubtractionFn__m,'减法函数')

 chinese_format.kif 685-685 "减法函数" is the printable form of subtraction in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__SubtractionFn__m,'subtraction')

 domainEnglishFormat.kif 9733-9733 "subtraction" is the printable form of subtraction in english language

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


( ! [V__Agent,V__Activity,V__ATIncome] :
   ((s__instance(V__Agent,s__Human)s__and__ms__instance(V__Activity,s__OrganizationalProcess)s__and__ms__instance(V__ATIncome,s__CurrencyMeasure))
    s__=>((s__exists__m[V__Income,V__Tax,V__TaxAmount] :
         (s__instance(V__Income,s__CurrencyMeasure)s__and__ms__instance(V__Tax,s__ChargingAFee)s__and__ms__instance(V__TaxAmount,s__CurrencyMeasure)s__and__m(s__incomeEarned(V__Agent,V__Income,V__Activity)
        s__and__ms__amountCharged(V__Tax,V__TaxAmount)
      s__and__ms__causes(V__Activity,V__Tax)
    s__and__m(V__ATIncomes__equal__ms__SubtractionFn(V__Income,V__TaxAmount)))))
s__<=>
s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity)))
)

 FinancialOntology.kif 3222-3229 There exist a currency measure, a chargingA fee and the chargingA feeAmount such that a human 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
( ! [V__Date,V__Balance,V__Account,V__Overdraft] :
   ((s__instance(V__Date,s__Day)s__and__ms__instance(V__Balance,s__RealNumber)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__Overdraft,s__RealNumber))
    s__=>((s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Balance,s__UnitedStatesDollar))
      s__and__ms__lessThan(V__Balance,0)
    s__and__m(V__Overdrafts__equal__ms__SubtractionFn(0,V__Balance)))
s__=>s__overdraft(V__Account,s__MeasureFn(V__Overdraft,s__UnitedStatesDollar),V__Date)))
)

 FinancialOntology.kif 733-738
( ! [V__Amount,V__Loan,V__Balance,V__Value,V__Purchase] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Loan,s__Loan)s__and__ms__instance(V__Balance,s__CurrencyMeasure)s__and__ms__instance(V__Value,s__CurrencyMeasure)s__and__ms__instance(V__Purchase,s__Object))
    s__=>((s__downPayment(V__Loan,V__Amount)
      s__and__ms__loanForPurchase(V__Loan,V__Purchase)
    s__and__ms__monetaryValue(V__Purchase,V__Value)
  s__and__m(V__Balances__equal__ms__SubtractionFn(V__Value,V__Amount)))
s__=>s__originalBalance(V__Loan,V__Balance)))
)

 FinancialOntology.kif 767-773
( ! [V__NUMBER1,V__MONTH,V__DAY2,V__NUMBER2,V__DAY1] :
   ((s__instance(V__NUMBER1,s__PositiveInteger)s__and__ms__subclass(V__MONTH,s__Month)s__and__ms__instance(V__DAY2,s__TimeInterval)s__and__ms__instance(V__NUMBER2,s__PositiveInteger)s__and__ms__instance(V__DAY1,s__TimeInterval))
    s__=>((s__instance(V__DAY1,s__DayFn(V__NUMBER1,V__MONTH))
    s__and__ms__instance(V__DAY2,s__DayFn(V__NUMBER2,V__MONTH))
s__and__m(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
s__equal__m1))
s__=>s__meetsTemporally(V__DAY1,V__DAY2)))
)

 Merge.kif 8726-8731
( ! [V__DAY,V__NUMBER1,V__HOUR2,V__NUMBER2,V__HOUR1] :
   ((s__subclass(V__DAY,s__Day)s__and__ms__instance(V__NUMBER1,s__NonnegativeInteger)s__and__ms__instance(V__HOUR2,s__TimeInterval)s__and__ms__instance(V__NUMBER2,s__NonnegativeInteger)s__and__ms__instance(V__HOUR1,s__TimeInterval))
    s__=>((s__instance(V__HOUR1,s__HourFn(V__NUMBER1,V__DAY))
    s__and__ms__instance(V__HOUR2,s__HourFn(V__NUMBER2,V__DAY))
s__and__m(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
s__equal__m1))
s__=>s__meetsTemporally(V__HOUR1,V__HOUR2)))
)

 Merge.kif 8756-8761
( ! [V__MINUTE1,V__NUMBER1,V__MINUTE2,V__NUMBER2,V__HOUR] :
   ((s__instance(V__MINUTE1,s__TimeInterval)s__and__ms__instance(V__NUMBER1,s__NonnegativeInteger)s__and__ms__instance(V__MINUTE2,s__TimeInterval)s__and__ms__instance(V__NUMBER2,s__NonnegativeInteger)s__and__ms__subclass(V__HOUR,s__Hour))
    s__=>((s__instance(V__MINUTE1,s__MinuteFn(V__NUMBER1,V__HOUR))
    s__and__ms__instance(V__MINUTE2,s__MinuteFn(V__NUMBER2,V__HOUR))
s__and__m(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
s__equal__m1))
s__=>s__meetsTemporally(V__MINUTE1,V__MINUTE2)))
)

 Merge.kif 8788-8793
( ! [V__Amount,V__Balance2,V__Balance1,V__Payment,V__Account] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Balance2,s__CurrencyMeasure)s__and__ms__instance(V__Balance1,s__CurrencyMeasure))
    s__=>((s__instance(V__Payment,s__Payment)s__and__ms__origin(V__Payment,s__CurrencyFn(V__Account))
    s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__transactionAmount(V__Payment,V__Amount)
  s__and__ms__currentAccountBalance(V__Account,s__ImmediatePastFn(s__WhenFn(V__Payment))
,V__Balance1)
s__and__m(V__Balance2s__equal__ms__SubtractionFn(V__Balance1,V__Amount)))
s__=>s__currentAccountBalance(V__Account,s__ImmediateFutureFn(s__WhenFn(V__Payment))
,V__Balance2)))
)

 FinancialOntology.kif 408-416
( ! [V__NUMBER1,V__NUMBER2,V__MINUTE,V__SECOND1,V__SECOND2] :
   ((s__instance(V__NUMBER1,s__PositiveInteger)s__and__ms__instance(V__NUMBER2,s__PositiveInteger)s__and__ms__subclass(V__MINUTE,s__Minute)s__and__ms__instance(V__SECOND1,s__TimeInterval)s__and__ms__instance(V__SECOND2,s__TimeInterval))
    s__=>((s__instance(V__SECOND1,s__SecondFn(V__NUMBER1,V__MINUTE))
    s__and__ms__instance(V__SECOND2,s__SecondFn(V__NUMBER2,V__MINUTE))
s__and__m(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
s__equal__m1))
s__=>s__meetsTemporally(V__SECOND1,V__SECOND2)))
)

 Merge.kif 8820-8825
( ! [V__Amount,V__Balance2,V__TimeOfWithdrawal,V__Balance1,V__Withdrawal,V__Account] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Balance2,s__CurrencyMeasure)s__and__ms__instance(V__TimeOfWithdrawal,s__TimePosition)s__and__ms__instance(V__Balance1,s__CurrencyMeasure))
    s__=>((s__instance(V__Withdrawal,s__Withdrawal)s__and__ms__time(V__Withdrawal,V__TimeOfWithdrawal)
      s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__origin(V__Withdrawal,V__Account)
    s__and__ms__transactionAmount(V__Withdrawal,V__Amount)
  s__and__ms__currentAccountBalance(V__Account,s__ImmediatePastFn(s__WhenFn(V__Withdrawal))
,V__Balance1)
s__and__m(V__Balance2s__equal__ms__SubtractionFn(V__Balance1,V__Amount)))
s__=>s__currentAccountBalance(V__Account,s__ImmediateFutureFn(s__FutureFn(V__Withdrawal))
,V__Balance2)))
)

 FinancialOntology.kif 450-459
( ! [V__YEAR1,V__YEAR2] :
   ((s__instance(V__YEAR1,s__Year)s__and__ms__instance(V__YEAR2,s__Year)s__and__m(s__SubtractionFn(V__YEAR2,V__YEAR1)
    s__equal__ms__MeasureFn(1,s__YearDuration)))
s__=>s__meetsTemporally(V__YEAR1,V__YEAR2))
)

 Merge.kif 8885-8890
( ! [V__REGION,V__OBJ,V__FAR,V__LIMIT,V__ZONE,V__UNIT] :
   ((s__instance(V__REGION,s__Region)s__and__ms__instance(V__OBJ,s__Object)s__and__ms__instance(V__FAR,s__RealNumber)s__and__ms__instance(V__LIMIT,s__RealNumber))
    s__=>((s__orientation(V__OBJ,V__REGION,s__Outside)s__and__ms__instance(V__ZONE,s__PerimeterAreaFn(V__REGION))
    s__and__ms__instance(V__ZONE,s__UniformPerimeterArea)s__and__ms__width(V__ZONE,s__MeasureFn(V__LIMIT,V__UNIT))
s__and__ms__distance(V__OBJ,V__REGION,s__MeasureFn(V__FAR,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfMeasure)s__and__ms__greaterThan(s__SubtractionFn(V__FAR,V__LIMIT)
,0))
s__=>(s__not__ms__located(V__OBJ,V__ZONE))))
)

 Geography.kif 849-858
( ! [V__REGION,V__OBJ,V__FAR,V__LIMIT,V__ZONE,V__UNIT] :
   ((s__instance(V__REGION,s__Region)s__and__ms__instance(V__OBJ,s__Object)s__and__ms__instance(V__FAR,s__RealNumber)s__and__ms__instance(V__LIMIT,s__RealNumber))
    s__=>((s__orientation(V__OBJ,V__REGION,s__Outside)s__and__ms__instance(V__ZONE,s__PerimeterAreaFn(V__REGION))
    s__and__ms__instance(V__ZONE,s__UniformPerimeterArea)s__and__ms__width(V__ZONE,s__MeasureFn(V__LIMIT,V__UNIT))
s__and__ms__distance(V__OBJ,V__REGION,s__MeasureFn(V__FAR,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfMeasure)s__and__ms__lessThanOrEqualTo(s__SubtractionFn(V__FAR,V__LIMIT)
,0))
s__=>s__located(V__OBJ,V__ZONE)))
)

 Geography.kif 838-847

consequent
-------------------------


( ! [V__NUMBER1,V__NUMBER2] :
   (((s__AbsoluteValueFn(V__NUMBER1)
      s__equal__mV__NUMBER2)s__and__ms__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__NUMBER2,s__RealNumber))
    s__<=>
    ((s__instance(V__NUMBER1,s__NonnegativeRealNumber)s__and__m(V__NUMBER1s__equal__mV__NUMBER2))
      s__or__m(s__instance(V__NUMBER1,s__NegativeRealNumber)s__and__m(V__NUMBER2s__equal__ms__SubtractionFn(0,V__NUMBER1)))))
)

 Merge.kif 4924-4935 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)
( ! [V__LASTPLACE,V__LIST1,V__AVERAGE] :
   ((s__instance(V__LASTPLACE,s__PositiveInteger)s__and__ms__instance(V__LIST1,s__List)s__and__ms__instance(V__AVERAGE,s__RealNumber))
    s__=>(s__average(V__LIST1,V__AVERAGE)
    s__<=>
    (s__exists__m[V__LIST2] :
       (s__instance(V__LIST2,s__List)s__and__m((s__ListLengthFn(V__LIST2)
        s__equal__ms__ListLengthFn(V__LIST1))
    s__and__m(s__ListOrderFn(V__LIST2,1)
  s__equal__ms__ListOrderFn(V__LIST1,1))
s__and__m(s__forall__m[V__ITEMFROM2] :
(s__instance(V__ITEMFROM2,s__PositiveInteger)s__=>(s__inList(V__ITEMFROM2,V__LIST2)
s__=>(s__exists__m[V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2] :
   (s__instance(V__POSITION,s__Quantity)s__and__ms__instance(V__POSITIONMINUSONE,s__Quantity)s__and__ms__instance(V__ITEMFROM1,s__PositiveInteger)s__and__ms__instance(V__PRIORFROM2,s__PositiveInteger)s__and__m(s__greaterThan(V__POSITION,1)
  s__and__ms__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
s__and__m(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
s__equal__mV__POSITION)s__and__ms__inList(V__ITEMFROM1,V__LIST1)
s__and__m(V__POSITIONs__equal__ms__ListOrderFn(V__LIST1,V__ITEMFROM1))
s__and__ms__inList(V__PRIORFROM2,V__LIST2)
s__and__m(V__POSITIONMINUSONEs__equal__ms__SubtractionFn(V__POSITION,1))
s__and__m(V__POSITIONMINUSONEs__equal__ms__ListOrderFn(V__LIST2,V__PRIORFROM2))
s__and__m(V__ITEMFROM2s__equal__ms__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
s__and__m(V__LASTPLACEs__equal__ms__ListLengthFn(V__LIST2))
s__and__m(V__AVERAGEs__equal__ms__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__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 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
No TPTP formula. May not be expressible in strict first order. 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
No TPTP formula. May not be expressible in strict first order. 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
( ! [V__DEGREE,V__OBJ1,V__OBJ2,V__MAGDEGREE,V__AREA,V__DIRECTION] :
   ((s__instance(V__DEGREE,s__PlaneAngleMeasure)s__and__ms__instance(V__OBJ1,s__Physical)s__and__ms__instance(V__OBJ2,s__Physical)s__and__ms__instance(V__MAGDEGREE,s__PlaneAngleMeasure)s__and__ms__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__DIRECTION,s__DirectionalAttribute))
    s__=>((s__courseWRTMagneticNorth(V__OBJ1,V__OBJ2,V__MAGDEGREE)
      s__and__ms__partlyLocated(V__OBJ1,V__AREA)
    s__and__ms__partlyLocated(V__OBJ2,V__AREA)
  s__and__ms__magneticVariation(V__AREA,V__DEGREE,V__DIRECTION))
s__=>(s__exists__m[V__DIFFDEGREE,V__TRUEDEGREE] :
(s__instance(V__DIFFDEGREE,s__Quantity)s__and__ms__instance(V__TRUEDEGREE,s__PlaneAngleMeasure)s__and__m((((V__DIRECTIONs__equal__ms__East)s__and__m(V__DIFFDEGREEs__equal__ms__AdditionFn(V__MAGDEGREE,V__DEGREE)))
  s__=>s__courseWRTTrueNorth(V__OBJ1,V__OBJ2,V__TRUEDEGREE))
s__and__m(((V__DIRECTIONs__equal__ms__West)s__and__m(V__DIFFDEGREEs__equal__ms__SubtractionFn(V__MAGDEGREE,V__DEGREE)))
s__=>s__courseWRTTrueNorth(V__OBJ1,V__OBJ2,V__TRUEDEGREE)))))))
)

 Geography.kif 3619-3636
( ! [V__QUANTITY1,V__QUANTITY2] :
   ((s__instance(V__QUANTITY1,s__Quantity)s__and__ms__instance(V__QUANTITY2,s__Quantity))
    s__=>(s__LiftFn(V__QUANTITY1,V__QUANTITY2)
    s__equal__ms__DivisionFn(s__SubtractionFn(V__QUANTITY1,V__QUANTITY2)
  ,V__QUANTITY2)))
)

 UXExperimentalTerms.kif 4754-4762
( ! [V__Period,V__Rate,V__Balance,V__Account,V__Interest,V__Multiply,V__Exponent,V__Rate_Decimal,V__Add] :
   ((s__instance(V__Period,s__TimeInterval)s__and__ms__instance(V__Rate,s__InterestRate)s__and__ms__instance(V__Balance,s__CurrencyMeasure)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__Interest,s__Interest)s__and__ms__instance(V__Multiply,s__Quantity)s__and__ms__instance(V__Exponent,s__RealNumber)s__and__ms__instance(V__Rate_Decimal,s__Quantity)s__and__ms__instance(V__Add,s__RealNumber))
    s__=>((s__principalAmount(V__Account,V__Balance)
      s__and__ms__fixedInterestRate(V__Account,V__Rate)
    s__and__ms__compoundInterest(V__Account,V__Interest,V__Period)
  s__and__m(V__Rate_Decimals__equal__ms__DivisionFn(V__Rate,100))
s__and__m(V__Adds__equal__ms__AdditionFn(1,V__Rate_Decimal))
s__and__m(V__Exponents__equal__ms__ExponentiationFn(V__Add,s__MagnitudeFn(V__Period)))
s__and__m(V__Multiplys__equal__ms__MultiplicationFn(V__Exponent,V__Balance)))
s__=>(V__Interests__equal__ms__SubtractionFn(V__Multiply,V__Balance))))
)

 FinancialOntology.kif 532-541

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


( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__RealNumber)s__=>(s__MeasureFn(V__NUMBER,s__CelsiusDegree)s__equal__ms__MeasureFn(s__DivisionFn(s__SubtractionFn(V__NUMBER,32)
    ,1.8)
  ,s__FahrenheitDegree)))
)

 Merge.kif 7270-7272 A real number celsius degree(s) is equal to (the real number and 32) and 1.8 fahrenheit degree(s)
( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__RealNumber)s__=>(s__MeasureFn(V__NUMBER,s__CelsiusDegree)s__equal__ms__MeasureFn(s__SubtractionFn(V__NUMBER,273.15)
    ,s__KelvinDegree)))
)

 Merge.kif 7266-7268 A real number celsius degree(s) is equal to (the real number and 273.15) kelvin degree(s)
No TPTP formula. May not be expressible in strict first order. 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
(s__forall__m[V__NUMBER] :
   (s__instance(V__NUMBER,s__Integer)s__=>(s__PredecessorFn(V__NUMBER)
    s__equal__ms__SubtractionFn(V__NUMBER,1))))

 Merge.kif 4887-4888 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