Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - AdditionFn
AdditionFn

appearance as argument number 1
-------------------------


s__documentation(s__AdditionFn__m,s__ChineseLanguage,'"如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (AdditionFn ?NUMBER1 ?NUMBER2)就是这些数字的算术和。"')

chinese_format.kif 2214-2215
s__documentation(s__AdditionFn__m,s__EnglishLanguage,'"If ?NUMBER1 and ?NUMBER2 are Numbers, then (AdditionFn ?NUMBER1 ?NUMBER2) is the arithmetical sum of these numbers."')

Merge.kif 4543-4545
s__domain(s__AdditionFn__m,n__1,s__Number)

Merge.kif 4539-4539 The number 1 argument of addition is an instance of number
s__domain(s__AdditionFn__m,n__2,s__Number)

Merge.kif 4540-4540 The number 2 argument of addition is an instance of number
s__identityElement(s__AdditionFn__m,n__0)

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

s__instance(s__AdditionFn__m,s__AssociativeFunction)

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

s__instance(s__AdditionFn__m,s__BinaryFunction)

Merge.kif 4534-4534 Addition is an instance of binary function
s__instance(s__CommutativeFunction,s__SetOrClass)

s__instance(s__AdditionFn__m,s__CommutativeFunction)

Merge.kif 4536-4536 Addition is an instance of commutative function
s__instance(s__TotalValuedRelation,s__SetOrClass)

s__instance(s__AdditionFn__m,s__TotalValuedRelation)

Merge.kif 4538-4538 Addition is an instance of total valued relation
s__range(s__AdditionFn__m,s__Number)

Merge.kif 4541-4541 The range of addition is an instance of number

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


s__format(s__ChineseLanguage,s__AdditionFn__m,'"(%*[+])"')

chinese_format.kif 682-682
s__format(s__EnglishLanguage,s__AdditionFn__m,'"(%*[+])"')

english_format.kif 687-687
s__termFormat(s__ChineseLanguage,s__AdditionFn__m,'"加成"')

domainEnglishFormat.kif 5427-5427
s__termFormat(s__ChineseLanguage,s__AdditionFn__m,'"加法函数"')

chinese_format.kif 683-683
s__termFormat(s__ChineseTraditionalLanguage,s__AdditionFn__m,'"加成"')

domainEnglishFormat.kif 5426-5426
s__termFormat(s__EnglishLanguage,s__AdditionFn__m,'"addition"')

domainEnglishFormat.kif 5425-5425

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


( ! [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 3038-3059
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 22673-22690
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 1178-1187
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 1227-1236
( ! [V__Period,V__Total,V__BondHolder,V__Date,V__Bond,V__Interest,V__Principal] :
   (((s__instance(V__Period,s__TimeInterval) &
         s__instance(V__Total,s__Number) &
         s__instance(V__Total,s__CurrencyMeasure) &
         s__instance(V__BondHolder,s__Agent) &
         s__instance(V__Date,s__Day) &
         s__instance(V__Interest,s__Interest) &
         s__instance(V__Interest,s__Number) &
         s__instance(V__Principal,s__Number) &
         s__instance(V__Principal,s__CurrencyMeasure))
       =>
       (((s__instance(V__Bond,s__ZeroCouponBond) &
             s__maturityDate(s__AccountFn(V__Bond)
          ,V__Date)
         &
         s__possesses(V__BondHolder,V__Bond)
       &
       s__principalAmount(s__AccountFn(V__Bond)
    ,V__Principal)
   &
   s__agreementPeriod(s__AccountFn(V__Bond)
,V__Period)
&
s__interestEarned(s__AccountFn(V__Bond)
,V__Interest,V__Period)
&
(V__Total = s__AdditionFn(V__Principal,V__Interest)))
=>
(( ? [V__Payment] :
((s__instance(V__Payment,s__Payment) &
s__destination(V__Payment,V__BondHolder)
&
s__origin(V__Payment,s__AccountFn(V__Bond))
&
s__transactionAmount(V__Payment,V__Total))))))))
)
)

FinancialOntology.kif 2303-2317
( ! [V__Amount,V__Balance2,V__Balance1,V__Deposit,V__Account] :
   (((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__Deposit,s__Deposit) &
             s__instance(V__Account,s__FinancialAccount) &
             s__destination(V__Deposit,s__CurrencyFn(V__Account))
         &
         s__transactionAmount(V__Deposit,V__Amount)
       &
       s__currentAccountBalance(V__Account,s__ImmediatePastFn(s__WhenFn(V__Deposit))
  ,V__Balance1)
&
(V__Balance2 = s__AdditionFn(V__Balance1,V__Amount)))
=>
(s__currentAccountBalance(V__Account,s__ImmediateFutureFn(s__FutureFn(V__Deposit))
,V__Balance2)))))
)
)

FinancialOntology.kif 428-436
( ! [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

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


( ! [V__LIST3,V__LIST1,V__LIST2] :
   (((s__instance(V__LIST3,s__List) &
         s__instance(V__LIST1,s__List) &
         s__instance(V__LIST2,s__List))
       =>
       (((((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
             &
             ~((V__LIST1 = s__NullList))
               &
               ~((V__LIST2 = s__NullList)))
               =>
               ( ! [V__NUMBER1, V__NUMBER2] :
                 (((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
                   &
                   s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
               &
               s__instance(V__NUMBER1,s__PositiveInteger) &
               s__instance(V__NUMBER2,s__PositiveInteger))
             =>
             (((s__ListOrderFn(V__LIST3,V__NUMBER1)
                 = s__ListOrderFn(V__LIST1,V__NUMBER1))
             &
             (s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
            ,V__NUMBER2))
         = s__ListOrderFn(V__LIST2,V__NUMBER2))))))))
&
(( ! [V__NUMBER1, V__NUMBER2] :
(((s__lessThanOrEqualTo(V__NUMBER1,s__ListLengthFn(V__LIST1))
&
s__lessThanOrEqualTo(V__NUMBER2,s__ListLengthFn(V__LIST2))
&
s__instance(V__NUMBER1,s__PositiveInteger) &
s__instance(V__NUMBER2,s__PositiveInteger))
=>
(((s__ListOrderFn(V__LIST3,V__NUMBER1)
= s__ListOrderFn(V__LIST1,V__NUMBER1))
&
(s__ListOrderFn(V__LIST3,s__AdditionFn(s__ListLengthFn(V__LIST1)
,V__NUMBER2))
= s__ListOrderFn(V__LIST2,V__NUMBER2)))))))
=>
((V__LIST3 = s__ListConcatenateFn(V__LIST1,V__LIST2))
&
~((V__LIST1 = s__NullList))
&
~((V__LIST2 = s__NullList)))))))
)
)

Merge.kif 2979-2995 A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer
( ! [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 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
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
   (((s__instance(V__NUMBER1,s__Integer) &
         s__instance(V__NUMBER2,s__Integer) &
         s__instance(V__NUMBER,s__Integer))
       =>
       ((((s__RemainderFn(V__NUMBER1,V__NUMBER2)
             = V__NUMBER)
           =>
           (s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
        ,V__NUMBER2)
      ,V__NUMBER)
     = V__NUMBER1))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)

Merge.kif 4908-4910 An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer
( ! [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__SUM,V__NUMBER1,V__NUMBER2,V__ARC1,V__PATH,V__ARC2] :
   (((s__instance(V__SUM,s__Number) &
         s__instance(V__NUMBER1,s__Number) &
         s__instance(V__NUMBER2,s__Number) &
         s__instance(V__ARC1,s__GraphArc) &
         s__instance(V__PATH,s__GraphPath) &
         s__instance(V__ARC2,s__GraphArc))
       =>
       ((((s__PathWeightFn(V__PATH)
             = V__SUM)
           &
           s__graphPart(V__ARC1,V__PATH)
         &
         s__graphPart(V__ARC2,V__PATH)
       &
       s__arcWeight(V__ARC1,V__NUMBER1)
     &
     s__arcWeight(V__ARC2,V__NUMBER2)
   &
   ( ! [V__ARC3] :
     ((s__instance(V__ARC3,s__GraphElement) =>
         ((s__graphPart(V__ARC3,V__PATH)
           =>
           (((V__ARC3 = V__ARC1)
               |
               (V__ARC3 = V__ARC2)))))))))
=>
((s__PathWeightFn(V__PATH)
= s__AdditionFn(V__NUMBER1,V__NUMBER2))))))
)
)

Merge.kif 5727-5740
( ! [V__SUM,V__NUMBER1,V__SUBPATH,V__ARC1,V__PATH] :
   (((s__instance(V__SUM,s__Number) &
         s__instance(V__NUMBER1,s__Number) &
         s__instance(V__SUBPATH,s__GraphPath) &
         s__instance(V__ARC1,s__GraphArc) &
         s__instance(V__PATH,s__GraphPath))
       =>
       ((((s__PathWeightFn(V__PATH)
             = V__SUM)
           &
           s__subGraph(V__SUBPATH,V__PATH)
         &
         s__graphPart(V__ARC1,V__PATH)
       &
       s__arcWeight(V__ARC1,V__NUMBER1)
     &
     ( ! [V__ARC2] :
       ((s__instance(V__ARC2,s__GraphElement) =>
           ((s__graphPart(V__ARC2,V__PATH)
             =>
             ((s__graphPart(V__ARC2,V__SUBPATH)
               |
               (V__ARC2 = V__ARC1)))))))))
=>
((V__SUM = s__AdditionFn(s__PathWeightFn(V__SUBPATH)
,V__NUMBER1))))))
)
)

Merge.kif 5713-5725
( ! [V__A,V__L] :
   (((s__instance(V__A,s__Number) &
         s__instance(V__L,s__List))
       =>
       ((((V__A = s__ListSumFn(V__L))
           &
           s__greaterThan(s__ListLengthFn(V__L)
        ,n__1))
     =>
     ((V__A = s__AdditionFn(s__FirstFn(V__L)
      ,s__ListSumFn(s__SubListFn(n__2,s__ListLengthFn(V__L)
    ,V__L))))))))
)
)

Merge.kif 3149-3159
( ! [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 3038-3059
( ! [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__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 3085-3097
( ! [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))
           &
           s__greaterThan(s__ListLengthFn(V__L)
        ,n__1))
     =>
     ((V__VA = s__AdditionFn(s__VarianceAverageFn(V__M,s__ListOrderFn(V__L,n__1))
    ,s__VarianceAverageFn(V__M,s__SubListFn(n__2,s__ListLengthFn(V__L)
  ,V__L))))))))
)
)

Weather.kif 1452-1464
( ! [V__LAND,V__WATER,V__AREA,V__UNIT] :
   (((s__instance(V__LAND,s__RealNumber) &
         s__instance(V__WATER,s__RealNumber) &
         s__instance(V__AREA,s__GeographicArea))
       =>
       (((s__instance(V__UNIT,s__UnitOfArea) &
             s__landAreaOnly(V__AREA,s__MeasureFn(V__LAND,V__UNIT))
         &
         s__waterAreaOnly(V__AREA,s__MeasureFn(V__WATER,V__UNIT)))
   =>
   (s__totalArea(V__AREA,s__MeasureFn(s__AdditionFn(V__LAND,V__WATER)
  ,V__UNIT))))))
)
)

Geography.kif 562-567
( ! [V__LENGTH1,V__LENGTH2,V__AREA,V__LENGTH,V__UNIT] :
   (((s__instance(V__LENGTH1,s__RealNumber) &
         s__instance(V__LENGTH2,s__RealNumber) &
         s__instance(V__AREA,s__GeographicArea) &
         s__instance(V__LENGTH,s__RealNumber))
       =>
       (((s__totalLengthOfHighwaySystem(V__AREA,s__MeasureFn(V__LENGTH,V__UNIT))
         &
         s__lengthOfPavedHighway(V__AREA,s__MeasureFn(V__LENGTH1,V__UNIT))
     &
     s__lengthOfUnpavedHighway(V__AREA,s__MeasureFn(V__LENGTH2,V__UNIT))
&
s__instance(V__UNIT,s__UnitOfLength))
=>
(s__totalLengthOfHighwaySystem(V__AREA,s__MeasureFn(s__AdditionFn(V__LENGTH1,V__LENGTH2)
,V__UNIT))))))
)
)

Transportation.kif 510-517
( ! [V__LENGTH1,V__LENGTH2,V__AREA,V__LENGTH] :
   (((s__instance(V__LENGTH1,s__Number) &
         s__instance(V__LENGTH1,s__LengthMeasure) &
         s__instance(V__LENGTH2,s__Number) &
         s__instance(V__LENGTH2,s__LengthMeasure) &
         s__instance(V__AREA,s__GeographicArea) &
         s__instance(V__LENGTH,s__Number) &
         s__instance(V__LENGTH,s__LengthMeasure))
       =>
       (((s__totalLengthOfHighwaySystem(V__AREA,V__LENGTH)
           &
           s__lengthOfPavedHighway(V__AREA,V__LENGTH1)
         &
         s__lengthOfUnpavedHighway(V__AREA,V__LENGTH2))
     =>
     ((V__LENGTH = s__AdditionFn(V__LENGTH1,V__LENGTH2))))))
)
)

Transportation.kif 503-508
( ! [V__COMPOUND2,V__COMPOUND1] :
   (((s__instance(V__COMPOUND2,s__CompoundSubstance) &
         s__instance(V__COMPOUND1,s__CompoundSubstance))
       =>
       ((s__conjugate(V__COMPOUND1,V__COMPOUND2)
         =>
         (( ? [V__NUMBER1, V__NUMBER2] :
             ((s__instance(V__NUMBER1,s__PositiveInteger) &
                 s__instance(V__NUMBER2,s__PositiveInteger) &
                 (s__protonNumber(V__COMPOUND1,V__NUMBER1)
                 &
                 s__protonNumber(V__COMPOUND2,V__NUMBER2)
               &
               ((V__NUMBER1 = s__AdditionFn(V__NUMBER2,n__1))
               |
               (V__NUMBER2 = s__AdditionFn(V__NUMBER1,n__1)))))))))))
)
)

Mid-level-ontology.kif 6122-6130
( ! [V__TIME2,V__TIME1] :
   (((s__instance(V__TIME2,s__Number) &
         s__instance(V__TIME2,s__TimePosition) &
         s__instance(V__TIME1,s__Number) &
         s__instance(V__TIME1,s__TimePosition))
       =>
       (((s__RelativeTimeFn(V__TIME1,s__CentralTimeZone) = V__TIME2)
           =>
           ((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__6,s__HourDuration)))))))
   )
)

Merge.kif 16407-16409
( ! [V__TIME2,V__TIME1] :
   (((s__instance(V__TIME2,s__Number) &
         s__instance(V__TIME2,s__TimePosition) &
         s__instance(V__TIME1,s__Number) &
         s__instance(V__TIME1,s__TimePosition))
       =>
       (((s__RelativeTimeFn(V__TIME1,s__EasternTimeZone) = V__TIME2)
           =>
           ((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__5,s__HourDuration)))))))
   )
)

Merge.kif 16415-16417
( ! [V__TIME2,V__TIME1] :
   (((s__instance(V__TIME2,s__Number) &
         s__instance(V__TIME2,s__TimePosition) &
         s__instance(V__TIME1,s__Number) &
         s__instance(V__TIME1,s__TimePosition))
       =>
       (((s__RelativeTimeFn(V__TIME1,s__MountainTimeZone) = V__TIME2)
           =>
           ((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__7,s__HourDuration)))))))
   )
)

Merge.kif 16399-16401
( ! [V__TIME2,V__TIME1] :
   (((s__instance(V__TIME2,s__Number) &
         s__instance(V__TIME2,s__TimePosition) &
         s__instance(V__TIME1,s__Number) &
         s__instance(V__TIME1,s__TimePosition))
       =>
       (((s__RelativeTimeFn(V__TIME1,s__PacificTimeZone) = V__TIME2)
           =>
           ((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__8,s__HourDuration)))))))
   )
)

Merge.kif 16388-16393
( ! [V__1,V__LIST,V__T1,V__T2,V__N] :
   (((s__instance(V__1,s__Number) &
         s__instance(V__T1,s__TimeInterval) &
         s__instance(V__T2,s__TimeInterval) &
         s__instance(V__N,s__Number) &
         s__instance(V__N,s__List))
       =>
       ((s__instance(V__LIST,s__ConsecutiveTimeIntervalList) =>
           (((V__T1 = s__ListOrderFn(V__N,V__LIST))
             &
             (V__T2 = s__ListOrderFn(s__AdditionFn(V__N,V__1)
            ,V__LIST))
         &
         (s__BeginFn(V__T2)
         = s__EndFn(V__T1)))))))
)
)

Weather.kif 1934-1943

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


( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__Integer) =>
       ((s__SuccessorFn(V__NUMBER)
         = s__AdditionFn(V__NUMBER,n__1))))))

Merge.kif 4547-4548 For all an integer (the integer+1) 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