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 的负数。"')

 chinese_format.kif 2216-2219
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 4499-4503
s__domain(s__SubtractionFn__m,n__1,s__Quantity)

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

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

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

s__instance(s__SubtractionFn__m,s__BinaryFunction)

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

s__instance(s__SubtractionFn__m,s__TotalValuedRelation)

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

 Merge.kif 4497-4497 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 689-689
s__termFormat(s__ChineseLanguage,s__SubtractionFn__m,'"减法"')

 domainEnglishFormat.kif 55747-55747
s__termFormat(s__ChineseLanguage,s__SubtractionFn__m,'"减法函数"')

 chinese_format.kif 685-685
s__termFormat(s__ChineseTraditionalLanguage,s__SubtractionFn__m,'"減法"')

 domainEnglishFormat.kif 55746-55746
s__termFormat(s__EnglishLanguage,s__SubtractionFn__m,'"subtraction"')

 domainEnglishFormat.kif 55745-55745

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


( ! [V__Agent,V__Activity,V__ATIncome] :
   ((s__instance(V__Agent,s__Human) &
       s__instance(V__Activity,s__OrganizationalProcess) &
       s__instance(V__ATIncome,s__CurrencyMeasure))
     =>
     (( ? [V__Income, V__Tax, V__TaxAmount] :
         ((s__instance(V__Income,s__CurrencyMeasure) &
             s__instance(V__Tax,s__ChargingAFee) &
             s__instance(V__TaxAmount,s__CurrencyMeasure) &
             (s__incomeEarned(V__Agent,V__Income,V__Activity)
             &
             s__amountCharged(V__Tax,V__TaxAmount)
           &
           s__causes(V__Activity,V__Tax)
         &
         (V__ATIncome = s__SubtractionFn(V__Income,V__TaxAmount))))))
=>
s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity))
&
(s__afterTaxIncome(V__Agent,V__ATIncome,V__Activity)
=>
( ? [V__Income, V__Tax, V__TaxAmount] :
((s__instance(V__Income,s__CurrencyMeasure) &
s__instance(V__Tax,s__ChargingAFee) &
s__instance(V__TaxAmount,s__CurrencyMeasure) &
(s__incomeEarned(V__Agent,V__Income,V__Activity)
&
s__amountCharged(V__Tax,V__TaxAmount)
&
s__causes(V__Activity,V__Tax)
&
(V__ATIncome = s__SubtractionFn(V__Income,V__TaxAmount)))))))
)
)

 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
( ! [V__Date,V__Balance,V__Account,V__Overdraft] :
   ((s__instance(V__Date,s__Day) &
       s__instance(V__Balance,s__RealNumber) &
       s__instance(V__Account,s__FinancialAccount) &
       s__instance(V__Overdraft,s__RealNumber))
     =>
     (s__currentAccountBalance(V__Account,V__Date,s__MeasureFn(V__Balance,s__UnitedStatesDollar))
     &
     s__lessThan(V__Balance,n__0)
   &
   (V__Overdraft = s__SubtractionFn(n__0,V__Balance)))
=>
s__overdraft(V__Account,s__MeasureFn(V__Overdraft,s__UnitedStatesDollar),V__Date)
)
)

 FinancialOntology.kif 732-737
( ! [V__Amount,V__Loan,V__Balance,V__Value,V__Purchase] :
   ((s__instance(V__Amount,s__CurrencyMeasure) &
       s__instance(V__Loan,s__Loan) &
       s__instance(V__Balance,s__CurrencyMeasure) &
       s__instance(V__Value,s__CurrencyMeasure) &
       s__instance(V__Purchase,s__Object))
     =>
     (s__downPayment(V__Loan,V__Amount)
     &
     s__loanForPurchase(V__Loan,V__Purchase)
   &
   s__monetaryValue(V__Purchase,V__Value)
&
(V__Balance = s__SubtractionFn(V__Value,V__Amount)))
=>
s__originalBalance(V__Loan,V__Balance)
)
)

 FinancialOntology.kif 766-772
( ! [V__OUT,V__IN,V__S,V__PIVOT,V__LEN,V__NEW,V__N] :
   ((s__instance(V__OUT,s__SymbolicString) &
       s__instance(V__IN,s__SymbolicString) &
       s__instance(V__S,s__SymbolicString) &
       s__instance(V__PIVOT,s__Integer) &
       s__instance(V__LEN,s__NonnegativeInteger) &
       s__instance(V__NEW,s__NonnegativeInteger) &
       s__instance(V__N,s__NonnegativeInteger))
     =>
     ((V__OUT = s__ReverseFn(V__IN))
     &
     (V__LEN = s__StringLengthFn(V__IN))
   &
   s__greaterThan(V__LEN,n__1)
&
s__greaterThan(V__N,n__0)
&
s__lessThan(V__N,V__LEN)
&
(V__PIVOT = s__CeilingFn(s__DivisionFn(s__SubtractionFn(V__LEN,n__1)
,n__2)))
&
(V__NEW = s__AdditionFn(s__SubtractionFn(V__PIVOT,V__N)
,V__PIVOT))
&
(V__S = s__SubstringFn(V__IN,V__N,s__AdditionFn(n__1,V__N))))
=>
(V__S = s__SubstringFn(V__OUT,V__NEW,s__AdditionFn(n__1,V__NEW)))
)
)

 Media.kif 3036-3057
( ! [V__R,V__S,V__E,V__L] :
   ((s__instance(V__R,s__List) &
       s__instance(V__S,s__Integer) &
       s__instance(V__E,s__Integer) &
       s__instance(V__L,s__List))
     =>
     ((V__R = s__SubListFn(V__S,V__E,V__L))
     &
     (s__SubtractionFn(V__E,V__S)
     = n__0))
=>
(V__R = s__NullList__m) )
)

 Merge.kif 3058-3065
( ! [V__R,V__S,V__E,V__L] :
   ((s__instance(V__R,s__List) &
       s__instance(V__S,s__PositiveInteger) &
       s__instance(V__E,s__Integer) &
       s__instance(V__L,s__List))
     =>
     ((V__R = s__SubListFn(V__S,V__E,V__L))
     &
     (s__SubtractionFn(V__E,V__S)
     = n__1))
=>
(V__R = s__ListFn__1Fn(s__ListOrderFn(V__L,V__S)))
)
)

 Merge.kif 3067-3076
( ! [V__R,V__S,V__E,V__L] :
   ((s__instance(V__R,s__List) &
       s__instance(V__S,s__PositiveInteger) &
       s__instance(V__E,s__Integer) &
       s__instance(V__L,s__List))
     =>
     ((V__R = s__SubListFn(V__S,V__E,V__L))
     &
     s__greaterThan(s__SubtractionFn(V__E,V__S)
  ,n__1))
=>
(V__R = s__ListConcatenateFn(s__ListFn__1Fn(s__ListOrderFn(V__L,V__S))
,s__SubListFn(s__AdditionFn(n__1,V__S)
,V__E,V__L)))
)
)

 Merge.kif 3078-3090
( ! [V__NUMBER1,V__MONTH,V__DAY2,V__NUMBER2,V__DAY1] :
   ((s__instance(V__NUMBER1,s__PositiveInteger) &
       s__subclass(V__MONTH,s__Month) &
       s__instance(V__DAY2,s__TimeInterval) &
       s__instance(V__NUMBER2,s__PositiveInteger) &
       s__instance(V__DAY1,s__TimeInterval))
     =>
     (s__instance(V__DAY1,s__DayFn(V__NUMBER1,V__MONTH))
   &
   s__instance(V__DAY2,s__DayFn(V__NUMBER2,V__MONTH))
&
(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
= n__1))
=>
s__meetsTemporally(V__DAY1,V__DAY2)
)
)

 Merge.kif 8030-8035
( ! [V__DAY,V__NUMBER1,V__HOUR2,V__NUMBER2,V__HOUR1] :
   ((s__subclass(V__DAY,s__Day) &
       s__instance(V__NUMBER1,s__NonnegativeInteger) &
       s__instance(V__HOUR2,s__TimeInterval) &
       s__instance(V__NUMBER2,s__NonnegativeInteger) &
       s__instance(V__HOUR1,s__TimeInterval))
     =>
     (s__instance(V__HOUR1,s__HourFn(V__NUMBER1,V__DAY))
   &
   s__instance(V__HOUR2,s__HourFn(V__NUMBER2,V__DAY))
&
(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
= n__1))
=>
s__meetsTemporally(V__HOUR1,V__HOUR2)
)
)

 Merge.kif 8056-8061
( ! [V__MINUTE1,V__NUMBER1,V__MINUTE2,V__NUMBER2,V__HOUR] :
   ((s__instance(V__MINUTE1,s__TimeInterval) &
       s__instance(V__NUMBER1,s__NonnegativeInteger) &
       s__instance(V__MINUTE2,s__TimeInterval) &
       s__instance(V__NUMBER2,s__NonnegativeInteger) &
       s__subclass(V__HOUR,s__Hour))
     =>
     (s__instance(V__MINUTE1,s__MinuteFn(V__NUMBER1,V__HOUR))
   &
   s__instance(V__MINUTE2,s__MinuteFn(V__NUMBER2,V__HOUR))
&
(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
= n__1))
=>
s__meetsTemporally(V__MINUTE1,V__MINUTE2)
)
)

 Merge.kif 8083-8088
( ! [V__Amount,V__Balance2,V__Balance1,V__Account,V__Payment] :
   ((s__instance(V__Amount,s__CurrencyMeasure) &
       s__instance(V__Balance2,s__CurrencyMeasure) &
       s__instance(V__Balance1,s__CurrencyMeasure))
     =>
     (s__instance(V__Payment,s__Payment) &
       s__origin(V__Payment,s__CurrencyFn(V__Account))
   &
   s__instance(V__Account,s__FinancialAccount) &
   s__transactionAmount(V__Payment,V__Amount)
&
s__currentAccountBalance(V__Account,s__ImmediatePastFn(s__WhenFn(V__Payment))
,V__Balance1)
&
(V__Balance2 = s__SubtractionFn(V__Balance1,V__Amount)))
=>
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__instance(V__NUMBER2,s__PositiveInteger) &
       s__subclass(V__MINUTE,s__Minute) &
       s__instance(V__SECOND1,s__TimeInterval) &
       s__instance(V__SECOND2,s__TimeInterval))
     =>
     (s__instance(V__SECOND1,s__SecondFn(V__NUMBER1,V__MINUTE))
   &
   s__instance(V__SECOND2,s__SecondFn(V__NUMBER2,V__MINUTE))
&
(s__SubtractionFn(V__NUMBER2,V__NUMBER1)
= n__1))
=>
s__meetsTemporally(V__SECOND1,V__SECOND2)
)
)

 Merge.kif 8110-8115
( ! [V__Amount,V__Balance2,V__Balance1,V__Account,V__Withdrawal] :
   ((s__instance(V__Amount,s__CurrencyMeasure) &
       s__instance(V__Balance2,s__CurrencyMeasure) &
       s__instance(V__Balance1,s__CurrencyMeasure))
     =>
     (s__instance(V__Withdrawal,s__Withdrawal) &
       s__instance(V__Account,s__FinancialAccount) &
       s__origin(V__Withdrawal,V__Account)
     &
     s__transactionAmount(V__Withdrawal,V__Amount)
   &
   s__currentAccountBalance(V__Account,s__ImmediatePastFn(s__WhenFn(V__Withdrawal))
,V__Balance1)
&
(V__Balance2 = s__SubtractionFn(V__Balance1,V__Amount)))
=>
s__currentAccountBalance(V__Account,s__ImmediateFutureFn(s__FutureFn(V__Withdrawal))
,V__Balance2)
)
)

 FinancialOntology.kif 449-457
( ! [V__YEAR2,V__YEAR1] :
   ((s__instance(V__YEAR1,s__Year) &
       s__instance(V__YEAR2,s__Year) &
       (s__SubtractionFn(V__YEAR2,V__YEAR1)
       = s__MeasureFn(n__1,s__YearDuration)))
   =>
   s__meetsTemporally(V__YEAR1,V__YEAR2)
)
)

 Merge.kif 8175-8180
( ! [V__REGION,V__OBJ,V__FAR,V__ZONE,V__UNIT,V__LIMIT] :
   ((s__instance(V__REGION,s__Region) &
       s__instance(V__OBJ,s__Object) &
       s__instance(V__FAR,s__RealNumber) &
       s__instance(V__LIMIT,s__RealNumber))
     =>
     (s__orientation(V__OBJ,V__REGION,s__Outside) &
       s__instance(V__ZONE,s__PerimeterAreaFn(V__REGION))
   &
   s__instance(V__ZONE,s__UniformPerimeterArea) &
   s__width(V__ZONE,s__MeasureFn(V__LIMIT,V__UNIT))
&
s__distance(V__OBJ,V__REGION,s__MeasureFn(V__FAR,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfMeasure) &
s__greaterThan(s__SubtractionFn(V__FAR,V__LIMIT)
,n__0))
=>
~(s__located(V__OBJ,V__ZONE))
)
)

 Geography.kif 862-871
( ! [V__REGION,V__OBJ,V__FAR,V__ZONE,V__UNIT,V__LIMIT] :
   ((s__instance(V__REGION,s__Region) &
       s__instance(V__OBJ,s__Object) &
       s__instance(V__FAR,s__RealNumber) &
       s__instance(V__LIMIT,s__RealNumber))
     =>
     (s__orientation(V__OBJ,V__REGION,s__Outside) &
       s__instance(V__ZONE,s__PerimeterAreaFn(V__REGION))
   &
   s__instance(V__ZONE,s__UniformPerimeterArea) &
   s__width(V__ZONE,s__MeasureFn(V__LIMIT,V__UNIT))
&
s__distance(V__OBJ,V__REGION,s__MeasureFn(V__FAR,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfMeasure) &
s__lessThanOrEqualTo(s__SubtractionFn(V__FAR,V__LIMIT)
,n__0))
=>
s__located(V__OBJ,V__ZONE)
)
)

 Geography.kif 851-860

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


( ! [V__NUMBER1,V__NUMBER2] :
   ((((s__AbsoluteValueFn(V__NUMBER1)
         = V__NUMBER2)
       &
       s__instance(V__NUMBER1,s__RealNumber) &
       s__instance(V__NUMBER2,s__RealNumber))
     =>
     ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
         (V__NUMBER1 = V__NUMBER2))
       |
       (s__instance(V__NUMBER1,s__NegativeRealNumber) &
         (V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1)))))
&
(((s__instance(V__NUMBER1,s__NonnegativeRealNumber) &
       (V__NUMBER1 = V__NUMBER2))
     |
     (s__instance(V__NUMBER1,s__NegativeRealNumber) &
       (V__NUMBER2 = s__SubtractionFn(n__0,V__NUMBER1))))
=>
((s__AbsoluteValueFn(V__NUMBER1)
   = V__NUMBER2)
&
s__instance(V__NUMBER1,s__RealNumber) &
s__instance(V__NUMBER2,s__RealNumber)))
)
)

 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)
( ! [V__LASTPLACE,V__LIST1,V__AVERAGE] :
   ((s__instance(V__LASTPLACE,s__PositiveInteger) &
       s__instance(V__LIST1,s__List) &
       s__instance(V__AVERAGE,s__RealNumber))
     =>
     (s__average(V__LIST1,V__AVERAGE)
     =>
     ( ? [V__LIST2] :
       ((s__instance(V__LIST2,s__List) &
           ((s__ListLengthFn(V__LIST2)
             = s__ListLengthFn(V__LIST1))
         &
         (s__ListOrderFn(V__LIST2,n__1)
         = s__ListOrderFn(V__LIST1,n__1))
     &
     ( ! [V__ITEMFROM2] :
       (s__instance(V__ITEMFROM2,s__PositiveInteger) =>
         s__inList(V__ITEMFROM2,V__LIST2)
       =>
       ( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
         ((s__instance(V__POSITION,s__Quantity) &
             s__instance(V__POSITIONMINUSONE,s__Quantity) &
             s__instance(V__ITEMFROM1,s__PositiveInteger) &
             s__instance(V__PRIORFROM2,s__PositiveInteger) &
             (s__greaterThan(V__POSITION,n__1)
             &
             s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
         &
         (s__ListOrderFn(V__LIST2,V__ITEMFROM2)
         = V__POSITION)
       &
       s__inList(V__ITEMFROM1,V__LIST1)
     &
     (V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))
   &
   s__inList(V__PRIORFROM2,V__LIST2)
&
(V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))))
&
(( ? [V__LIST2] :
((s__instance(V__LIST2,s__List) &
((s__ListLengthFn(V__LIST2)
= s__ListLengthFn(V__LIST1))
&
(s__ListOrderFn(V__LIST2,n__1)
= s__ListOrderFn(V__LIST1,n__1))
&
( ! [V__ITEMFROM2] :
(s__instance(V__ITEMFROM2,s__PositiveInteger) =>
s__inList(V__ITEMFROM2,V__LIST2)
=>
( ? [V__POSITION, V__POSITIONMINUSONE, V__ITEMFROM1, V__PRIORFROM2] :
((s__instance(V__POSITION,s__Quantity) &
s__instance(V__POSITIONMINUSONE,s__Quantity) &
s__instance(V__ITEMFROM1,s__PositiveInteger) &
s__instance(V__PRIORFROM2,s__PositiveInteger) &
(s__greaterThan(V__POSITION,n__1)
&
s__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
&
(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
= V__POSITION)
&
s__inList(V__ITEMFROM1,V__LIST1)
&
(V__POSITION = s__ListOrderFn(V__LIST1,V__ITEMFROM1))
&
s__inList(V__PRIORFROM2,V__LIST2)
&
(V__POSITIONMINUSONE = s__SubtractionFn(V__POSITION,n__1))
&
(V__POSITIONMINUSONE = s__ListOrderFn(V__LIST2,V__PRIORFROM2))
&
(V__ITEMFROM2 = s__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
&
(V__LASTPLACE = s__ListLengthFn(V__LIST2))
&
(V__AVERAGE = s__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE))))))
=>
s__average(V__LIST1,V__AVERAGE))
)
)

 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__instance(V__OBJ1,s__Physical) &
       s__instance(V__OBJ2,s__Physical) &
       s__instance(V__MAGDEGREE,s__PlaneAngleMeasure) &
       s__instance(V__AREA,s__GeographicArea) &
       s__instance(V__DIRECTION,s__DirectionalAttribute))
     =>
     (s__courseWRTMagneticNorth(V__OBJ1,V__OBJ2,V__MAGDEGREE)
     &
     s__partlyLocated(V__OBJ1,V__AREA)
   &
   s__partlyLocated(V__OBJ2,V__AREA)
&
s__magneticVariation(V__AREA,V__DEGREE,V__DIRECTION))
=>
( ? [V__DIFFDEGREE, V__TRUEDEGREE] :
((s__instance(V__DIFFDEGREE,s__Quantity) &
   s__instance(V__TRUEDEGREE,s__PlaneAngleMeasure) &
   (((V__DIRECTION = s__East) &
         (V__DIFFDEGREE = s__AdditionFn(V__MAGDEGREE,V__DEGREE)))
     =>
     s__courseWRTTrueNorth(V__OBJ1,V__OBJ2,V__TRUEDEGREE)
   &
   ((V__DIRECTION = s__West) &
       (V__DIFFDEGREE = s__SubtractionFn(V__MAGDEGREE,V__DEGREE)))
   =>
   s__courseWRTTrueNorth(V__OBJ1,V__OBJ2,V__TRUEDEGREE)))))
)
)

 Geography.kif 3632-3649
( ! [V__QUANTITY2,V__QUANTITY1] :
   ((s__instance(V__QUANTITY1,s__Quantity) &
       s__instance(V__QUANTITY2,s__Quantity))
     =>
     (s__LiftFn(V__QUANTITY1,V__QUANTITY2)
     = s__DivisionFn(s__SubtractionFn(V__QUANTITY1,V__QUANTITY2)
  ,V__QUANTITY2))
)
)

 UXExperimentalTerms.kif 4761-4769
( ! [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__instance(V__Rate,s__InterestRate) &
       s__instance(V__Balance,s__CurrencyMeasure) &
       s__instance(V__Account,s__FinancialAccount) &
       s__instance(V__Interest,s__Interest) &
       s__instance(V__Multiply,s__Quantity) &
       s__instance(V__Exponent,s__RealNumber) &
       s__instance(V__Rate_Decimal,s__Quantity) &
       s__instance(V__Add,s__RealNumber))
     =>
     (s__principalAmount(V__Account,V__Balance)
     &
     s__fixedInterestRate(V__Account,V__Rate)
   &
   s__compoundInterest(V__Account,V__Interest,V__Period)
&
(V__Rate_Decimal = s__DivisionFn(V__Rate,n__100))
&
(V__Add = s__AdditionFn(n__1,V__Rate_Decimal))
&
(V__Exponent = s__ExponentiationFn(V__Add,s__MagnitudeFn(V__Period)))
&
(V__Multiply = s__MultiplicationFn(V__Exponent,V__Balance)))
=>
(V__Interest = s__SubtractionFn(V__Multiply,V__Balance))
)
)

 FinancialOntology.kif 531-540

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


( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__CelsiusDegree) = s__MeasureFn(s__DivisionFn(s__SubtractionFn(V__NUMBER,n__32)
    ,n__1_8)
  ,s__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)
( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__RealNumber) =>
     (s__MeasureFn(V__NUMBER,s__CelsiusDegree) = s__MeasureFn(s__SubtractionFn(V__NUMBER,n__273_15)
    ,s__KelvinDegree))
   )
)

 Merge.kif 6677-6679 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
( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__Integer) =>
     (s__PredecessorFn(V__NUMBER)
     = s__SubtractionFn(V__NUMBER,n__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