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 4592-4596
s__domain(s__SubtractionFn__m,n__1,s__Number)

Merge.kif 4588-4588 The number 1 argument of subtraction is an instance of number
s__domain(s__SubtractionFn__m,n__2,s__Number)

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

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

s__instance(s__SubtractionFn__m,s__BinaryFunction)

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

s__instance(s__SubtractionFn__m,s__TotalValuedRelation)

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

Merge.kif 4590-4590 The range of subtraction is an instance of number

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 686-686
s__termFormat(s__ChineseLanguage,s__SubtractionFn__m,'"减法"')

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

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

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

domainEnglishFormat.kif 55831-55831

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


( ! [V__Agent,V__Activity,V__ATIncome] :
   (((s__instance(V__Agent,s__Human) &
         s__instance(V__Activity,s__OrganizationalProcess) &
         s__instance(V__ATIncome,s__Number) &
         s__instance(V__ATIncome,s__CurrencyMeasure))
       =>
       (((( ? [V__Income, V__Tax, V__TaxAmount] :
               ((s__instance(V__Income,s__Number) &
                   s__instance(V__Income,s__CurrencyMeasure) &
                   s__instance(V__Tax,s__ChargingAFee) &
                   s__instance(V__TaxAmount,s__Number) &
                   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__Number) &
       s__instance(V__Income,s__CurrencyMeasure) &
       s__instance(V__Tax,s__ChargingAFee) &
       s__instance(V__TaxAmount,s__Number) &
       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 3292-3299 There exist a number, a chargingA fee and the chargingA feeAmount such that a human is income earned the number 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 number is equal to (the number and the chargingA feeAmount) if and only if the after tax income derived by the human from the organizational process is the third number
( ! [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 742-747
( ! [V__Amount,V__Loan,V__Balance,V__Value,V__Purchase] :
   (((s__instance(V__Amount,s__Number) &
         s__instance(V__Amount,s__CurrencyMeasure) &
         s__instance(V__Loan,s__Loan) &
         s__instance(V__Balance,s__Number) &
         s__instance(V__Balance,s__CurrencyMeasure) &
         s__instance(V__Value,s__Number) &
         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 776-782
( ! [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 3050-3071
( ! [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)))))
   )
)

Merge.kif 3098-3105
( ! [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 3107-3116
( ! [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 3118-3130
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 23183-23197
( ! [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 8254-8259
( ! [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 8280-8285
( ! [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 8307-8312
( ! [V__Amount,V__Balance2,V__Balance1,V__Account,V__Payment] :
   (((s__instance(V__Amount,s__Number) &
         s__instance(V__Amount,s__CurrencyMeasure) &
         s__instance(V__Balance2,s__Number) &
         s__instance(V__Balance2,s__CurrencyMeasure) &
         s__instance(V__Balance1,s__Number) &
         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 8334-8339
( ! [V__Amount,V__Balance2,V__Balance1,V__Account,V__Withdrawal] :
   (((s__instance(V__Amount,s__Number) &
         s__instance(V__Amount,s__CurrencyMeasure) &
         s__instance(V__Balance2,s__Number) &
         s__instance(V__Balance2,s__CurrencyMeasure) &
         s__instance(V__Balance1,s__Number) &
         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 8399-8404
( ! [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_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_0,V__NUMBER1))))
   =>
   ((s__AbsoluteValueFn(V__NUMBER1)
     = V__NUMBER2)
   &
   s__instance(V__NUMBER1,s__RealNumber) &
   s__instance(V__NUMBER2,s__RealNumber))))
)
)

Merge.kif 4630-4641 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.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__Number) &
                           s__instance(V__POSITIONMINUSONE,s__Number) &
                           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__Number) &
s__instance(V__POSITIONMINUSONE,s__Number) &
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 289-310 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 178-206 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 number) is equal to 1 and the population of the geopolitical area is equal to another number holds during the year the integer and the other number and 1000 is equal to a third number 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 number and the fourth number and the third number is equal to the real number
No TPTP formula. May not be expressible in strict first order. People.kif 78-90 The population growth of a geopolitical area and the year an integer is equal to a real number if and only if there exist a kind of year and another kind of year such that (the integer and another integer) is equal to 1 and a kind of year is equal to the year the integer and another kind of year is equal to the year the other integer and the population of the geopolitical area is equal to a number holds during the kind of year and the population of the geopolitical area is equal to another number holds during the other kind of year and the number and the other number is equal to a third number and (the third number 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__Number) &
         s__instance(V__DEGREE,s__PlaneAngleMeasure) &
         s__instance(V__OBJ1,s__Physical) &
         s__instance(V__OBJ2,s__Physical) &
         s__instance(V__MAGDEGREE,s__Number) &
         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__Number) &
           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 3675-3692
( ! [V__VA,V__L,V__M] :
   (((s__instance(V__VA,s__Number) &
         s__instance(V__L,s__List) &
         s__instance(V__M,s__Number))
       =>
       ((((V__VA = s__VarianceAverageFn(V__M,V__L))
           &
           (n__1 = s__ListLengthFn(V__L)))
       =>
       ((V__VA = s__MultiplicationFn(s__SubtractionFn(V__M,s__ListOrderFn(V__L,n__1))
      ,s__SubtractionFn(V__M,s__ListOrderFn(V__L,n__1))))))))
)
)

Weather.kif 1485-1496
( ! [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 4764-4772
( ! [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__Number) &
         s__instance(V__Balance,s__Number) &
         s__instance(V__Balance,s__CurrencyMeasure) &
         s__instance(V__Account,s__FinancialAccount) &
         s__instance(V__Interest,s__Interest) &
         s__instance(V__Interest,s__Number) &
         s__instance(V__Multiply,s__Number) &
         s__instance(V__Exponent,s__RealNumber) &
         s__instance(V__Rate_Decimal,s__Number) &
         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 532-541
( ! [V__O1,V__O2,V__N1,V__N2,V__N3,V__U,V__E1,V__E2,V__E3,V__E4,V__N] :
   (((s__instance(V__O1,s__Object) &
         s__instance(V__O2,s__Object) &
         s__instance(V__N1,s__RealNumber) &
         s__instance(V__N2,s__RealNumber) &
         s__instance(V__N3,s__RealNumber) &
         s__instance(V__U,s__UnitOfMeasure) &
         s__instance(V__E1,s__Object) &
         s__instance(V__E2,s__Object) &
         s__instance(V__E3,s__Object) &
         s__instance(V__E4,s__Object) &
         s__instance(V__N,s__RealNumber))
       =>
       (((s__relativeAngle(V__O1,V__O2,s__MeasureFn(V__N,s__AngularDegree))
           &
           s__physicalEnd(V__E1,V__O1)
         &
         s__physicalEnd(V__E2,V__O1)
       &
       ~((V__E1 = V__E2))
       &
       s__length(V__O1,s__MeasureFn(V__N1,V__U))
   &
   s__length(V__O2,s__MeasureFn(V__N2,V__U))
&
s__distance(V__E1,V__E3,s__MeasureFn(V__N3,V__U))
&
s__physicalEnd(V__E3,V__O2)
&
s__physicalEnd(V__E4,V__O2)
&
~((V__E3 = V__E4))
&
~(s__meetsSpatially(V__E1,V__E3)))
=>
((V__N = s__ArcCosineFn(s__DivisionFn(s__SubtractionFn(s__SubtractionFn(s__MultiplicationFn(V__N3,V__N3)
,s__MultiplicationFn(V__N1,V__N1))
,s__MultiplicationFn(V__N2,V__N2))
,s__MultiplicationFn(n__2,s__MultiplicationFn(V__N1,V__N2)))))))))
)
)

Merge.kif 17201-17227
( ! [V__TI,V__WF] :
   (((s__instance(V__TI,s__TimeInterval) &
         s__instance(V__WF,s__Week))
       =>
       (((V__WF = s__WeekBeforeFn(V__TI))
         =>
         ((V__WF = s__TimeIntervalFn(s__SubtractionFn(s__BeginFn(V__TI)
          ,s__MeasureFn(n__1,s__WeekDuration))
        ,s__BeginFn(V__TI)))))))
)
)

Mid-level-ontology.kif 14138-14145

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 6804-6806 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 6800-6802 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 4598-4599 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 3.0 is open source software produced by Articulate Software and its partners