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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - greaterThan
greaterThan

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


s__documentation(s__greaterThan__m,s__ChineseLanguage,'"(greaterThan ?NUMBER1 ?NUMBER2) 是真的以防 ?NUMBER1 的 Quantity 比 ?NUMBER2 的 Quantity 要大。"')

 chinese_format.kif 1731-1732
s__documentation(s__greaterThan__m,s__EnglishLanguage,'"(greaterThan ?NUMBER1 ?NUMBER2) is true just in case the Quantity ?NUMBER1 is greater than the Quantity ?NUMBER2."')

 Merge.kif 1799-1801
s__domain(s__greaterThan__m,n__1,s__Quantity)

 Merge.kif 1795-1795 The number 1 argument of greater than is an instance of quantity
s__domain(s__greaterThan__m,n__2,s__Quantity)

 Merge.kif 1796-1796 The number 2 argument of greater than is an instance of quantity
s__instance(s__BinaryPredicate,s__Class)

s__instance(s__greaterThan__m,s__BinaryPredicate)

 Merge.kif 1789-1789 greater than is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__Class)

s__instance(s__greaterThan__m,s__IrreflexiveRelation)

 Merge.kif 1792-1792 greater than is an instance of irreflexive relation
s__instance(s__greaterThan__m,s__RelationExtendedToQuantities)

s__instance(s__RelationExtendedToQuantities,s__Class)

 Merge.kif 1793-1793 greater than is an instance of relation extended to quantities
s__instance(s__TotalValuedRelation,s__Class)

s__instance(s__greaterThan__m,s__TotalValuedRelation)

 Merge.kif 1790-1790 greater than is an instance of total valued relation
s__instance(s__greaterThan__m,s__TransitiveRelation)

s__instance(s__TransitiveRelation,s__Class)

 Merge.kif 1791-1791 greater than is an instance of transitive relation
s__inverse(s__greaterThan__m,s__lessThan__m)

 Merge.kif 1797-1797 greater than is an inverse of less than
s__trichotomizingOn(s__greaterThan__m,s__RealNumber)

 Merge.kif 1794-1794 greater than is trichotomizing on real number

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


s__comparativeArea(s__SouthernOcean,s__greaterThan__m,n__2,s__UnitedStates)

 Geography.kif 4479-4479 Southern ocean comparative area greater than for 2 with united states
s__format(s__ChineseLanguage,s__greaterThan__m,'"%1 %n 是 greaterThan %2"')

 chinese_format.kif 111-111
s__format(s__EnglishLanguage,s__greaterThan__m,'"%1 is %n greater than %2"')

 english_format.kif 111-111
s__termFormat(s__ChineseLanguage,s__greaterThan__m,'"大于"')

 chinese_format.kif 112-112
s__termFormat(s__ChineseLanguage,s__greaterThan__m,'"比较多"')

 domainEnglishFormat.kif 26523-26523
s__termFormat(s__ChineseTraditionalLanguage,s__greaterThan__m,'"比較多"')

 domainEnglishFormat.kif 26522-26522
s__termFormat(s__EnglishLanguage,s__greaterThan__m,'"greater than"')

 domainEnglishFormat.kif 26521-26521

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


No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 961-965 An entity is an instance of personal account and the number of instances in the class described by a symbolic string is greater than 1 if and only if the entity is an instance of joint account
( ! [V__P,V__S,V__PM] :
   (((s__instance(V__P,s__SelfConnectedObject) &
         s__instance(V__S,s__RealNumber))
       =>
       ((((s__instance(V__PM,s__ParticulateMatter) &
               s__part(V__P,V__PM)
             &
             s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
           &
           s__greaterThan(n__10,V__S)
         &
         s__greaterThan(V__S,n__2_5))
     =>
     ( ? [V__PM10] :
       ((s__instance(V__PM10,s__CoarseParticulateMatter) &
           s__part(V__PM10,V__PM)))))
&
(( ? [V__PM10] :
     ((s__instance(V__PM10,s__CoarseParticulateMatter) &
         s__part(V__PM10,V__PM))))
=>
(s__instance(V__PM,s__ParticulateMatter) &
   s__part(V__P,V__PM)
&
s__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
&
s__greaterThan(n__10,V__S)
&
s__greaterThan(V__S,n__2_5))))))
)
)

 Geography.kif 6998-7009 An object is an instance of PM and a self connected object is a part of the object and the approximate diameter of the self connected object is a real number micrometer(s) and 10 is greater than the real number and the real number is greater than 2.5 if and only if there exists the object10 such that the object10 is an instance of PM10 and the object10 is a part of the object
No TPTP formula. May not be expressible in strict first order. Cars.kif 809-825
( ! [V__TEXT,V__EDITION1,V__CBO2,V__EDITION2,V__CBO1,V__INT2,V__PUB2,V__DATE1,V__INT1,V__DATE2,V__PUB1] :
   (((s__subclass(V__TEXT,s__ContentBearingObject) &
         s__subclass(V__EDITION1,s__ContentBearingObject) &
         s__instance(V__EDITION1,s__Class) &
         s__subclass(V__EDITION2,s__ContentBearingObject) &
         s__instance(V__EDITION2,s__Class) &
         s__instance(V__INT2,s__PositiveInteger) &
         s__instance(V__DATE1,s__Day) &
         s__instance(V__INT1,s__PositiveInteger) &
         s__instance(V__DATE2,s__Day))
       =>
       ((((s__EditionFn(V__TEXT,V__INT1)
             = V__EDITION1)
           &
           (s__EditionFn(V__TEXT,V__INT2)
           = V__EDITION2)
         &
         s__greaterThan(V__INT2,V__INT1)
       &
       s__instance(V__PUB1,s__Publication) &
       s__instance(V__PUB2,s__Publication) &
       s__instance(V__CBO1,V__EDITION1)
     &
     s__instance(V__CBO2,V__EDITION2)
   &
   s__patient(V__PUB1,V__CBO1)
&
s__patient(V__PUB2,V__CBO2)
&
s__date(V__PUB1,V__DATE1)
&
s__date(V__PUB2,V__DATE2))
=>
(s__before(s__EndFn(V__DATE1)
,s__EndFn(V__DATE2))))))
)
)

 Merge.kif 14861-14878
( ! [V__A,V__L] :
   (((s__instance(V__A,s__RealNumber) &
         s__instance(V__L,s__List))
       =>
       ((((V__A = s__AverageFn(V__L))
           &
           s__greaterThan(s__ListLengthFn(V__L)
        ,n__0))
     =>
     ((V__A = s__DivisionFn(s__ListSumFn(V__L)
      ,s__ListLengthFn(V__L)))))))
)
)

 Merge.kif 3201-3208
( ! [V__A,V__L] :
   (((s__instance(V__A,s__RealNumber) &
         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 3182-3192
( ! [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__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
( ! [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__COUNT,V__HOME,V__REGISTER,V__MM] :
   (((s__instance(V__COUNT,s__NonnegativeInteger) &
         s__instance(V__HOME,s__GeopoliticalArea) &
         s__instance(V__REGISTER,s__ShipRegister) &
         s__instance(V__MM,s__MerchantMarine))
       =>
       (((s__fOCShipsByOrigin(V__MM,V__HOME,V__COUNT)
           &
           s__greaterThan(V__COUNT,n__0)
         &
         s__marineInventory(V__MM,V__REGISTER))
     =>
     (s__instance(V__REGISTER,s__FlagOfConvenienceRegister)))))
)
)

 Transportation.kif 1070-1075
No TPTP formula. May not be expressible in strict first order. Cars.kif 2884-2902
( ! [V__MO,V__AREA,V__TEMP] :
   (((s__instance(V__MO,s__Class) &
         s__instance(V__MO,s__TimeDuration) &
         s__instance(V__TEMP,s__RealNumber))
       =>
       (((s__instance(V__AREA,s__DesertClimateZone) &
             s__subclass(V__MO,s__Month) &
             s__averageTemperatureForPeriod(V__AREA,V__MO,s__MeasureFn(V__TEMP,s__CelsiusDegree))
           &
           s__greaterThan(V__TEMP,n__18))
       =>
       (s__instance(V__AREA,s__SubtropicalDesertClimateZone)))))
)
)

 Geography.kif 1360-1367
( ! [V__MO,V__AREA,V__TEMP] :
   (((s__instance(V__MO,s__Class) &
         s__instance(V__MO,s__TimeDuration) &
         s__instance(V__TEMP,s__RealNumber))
       =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__subclass(V__MO,s__Month) &
             s__averageTemperatureForPeriod(V__AREA,V__MO,s__MeasureFn(V__TEMP,s__CelsiusDegree))
           &
           s__greaterThan(n__10,V__TEMP))
       =>
       (s__instance(V__AREA,s__PolarClimateZone)))))
)
)

 Geography.kif 1546-1553
( ! [V__OFFER1,V__U,V__OFFER2,V__ITEM,V__BIDDER2,V__BIDDER1,V__AUCTIONING] :
   (((s__instance(V__OFFER1,s__RealNumber) &
         s__instance(V__OFFER2,s__RealNumber))
       =>
       (((s__instance(V__AUCTIONING,s__Auctioning) &
             s__instance(V__BIDDER1,s__Agent) &
             s__instance(V__BIDDER2,s__Agent) &
             s__instance(V__ITEM,s__Object) &
             s__instance(V__U,s__UnitOfCurrency) &
             s__patient(V__AUCTIONING,V__ITEM)
           &
           s__bidPrice(V__ITEM,s__MeasureFn(V__OFFER1,V__U)
        ,V__BIDDER1)
       &
       s__bidPrice(V__ITEM,s__MeasureFn(V__OFFER2,V__U)
    ,V__BIDDER2)
   &
   s__greaterThan(V__OFFER1,V__OFFER2))
=>
(s__destination(V__AUCTIONING,V__BIDDER1)))))
)
)

 UXExperimentalTerms.kif 437-448
( ! [V__N1,V__N2,V__Y,V__D1,V__T1,V__D2,V__T2,V__M] :
   (((s__instance(V__N1,s__PositiveInteger) &
         s__instance(V__N2,s__PositiveInteger) &
         s__instance(V__Y,s__Integer) &
         s__instance(V__D1,s__TimeInterval) &
         s__instance(V__T1,s__TimePoint) &
         s__instance(V__D2,s__TimeInterval) &
         s__instance(V__T2,s__TimePoint) &
         s__subclass(V__M,s__Month))
       =>
       (((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y))))
     &
     s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y))))
&
(V__T1 = s__BeginFn(V__D1))
&
(V__T2 = s__BeginFn(V__D2))
&
s__greaterThan(V__N2,V__N1))
=>
(s__before(V__T1,V__T2)))))
)
)

 Merge.kif 8373-8380
( ! [V__N1,V__N2,V__Y,V__D1,V__D2,V__M] :
   (((s__instance(V__N1,s__PositiveInteger) &
         s__instance(V__N2,s__PositiveInteger) &
         s__instance(V__Y,s__Integer) &
         s__instance(V__D1,s__TimeInterval) &
         s__instance(V__D2,s__TimeInterval) &
         s__subclass(V__M,s__Month))
       =>
       (((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y))))
     &
     s__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y))))
&
s__greaterThan(V__N2,V__N1))
=>
(s__earlier(V__D1,V__D2)))))
)
)

 Merge.kif 8382-8387
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 320-326
( ! [V__HARBOR,V__NUM] :
   ((s__instance(V__NUM,s__Quantity) =>
       (((s__instance(V__HARBOR,s__Harbor) &
             s__equipmentCount(V__HARBOR,s__ShipBerth,V__NUM)
           &
           s__greaterThan(V__NUM,n__0))
       =>
       (s__capability(s__ShipBerthing,s__path__m,V__HARBOR)))))
)
)

 Transportation.kif 2949-2954
No TPTP formula. May not be expressible in strict first order. Merge.kif 13244-13259
( ! [V__SZ,V__X] :
   (((s__instance(V__SZ,s__SurfZone) &
         s__instance(V__X,s__LengthMeasure) &
         s__significantWaveHeight(V__SZ,s__WhenFn(V__SZ)
      ,s__MeasureFn(V__X,s__FootLength))
     &
     s__greaterThan(V__X,n__8))
=>
(s__attribute(V__SZ,s__RedFlagSwimmingCondition)))
)
)

 Weather.kif 1396-1404
( ! [V__PRES,V__X,V__BOIL,V__Y,V__TEMP] :
   (((s__instance(V__PRES,s__RealNumber) &
         s__instance(V__X,s__Object) &
         s__instance(V__BOIL,s__RealNumber) &
         s__instance(V__Y,s__Class) &
         s__subclass(V__Y,s__PureSubstance) &
         s__instance(V__TEMP,s__RealNumber))
       =>
       (((s__instance(V__X,V__Y)
           &
           s__subclass(V__Y,s__PureSubstance) &
           s__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
         &
         s__greaterThan(n__29_92,V__PRES)
       &
       s__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
     &
     s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
   &
   s__greaterThan(V__TEMP,V__BOIL))
=>
(s__attribute(V__X,s__Gas)))))
)
)

 Merge.kif 13179-13188
( ! [V__MELT,V__X,V__BOIL,V__Y,V__TEMP] :
   (((s__instance(V__MELT,s__RealNumber) &
         s__instance(V__X,s__Object) &
         s__instance(V__BOIL,s__RealNumber) &
         s__instance(V__Y,s__Class) &
         s__subclass(V__Y,s__PureSubstance) &
         s__instance(V__TEMP,s__RealNumber))
       =>
       (((s__instance(V__X,V__Y)
           &
           s__subclass(V__Y,s__PureSubstance) &
           s__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
         &
         s__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
       &
       s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
     &
     s__greaterThan(V__TEMP,V__MELT)
   &
   s__lessThan(V__TEMP,V__BOIL))
=>
(s__attribute(V__X,s__Liquid)))))
)
)

 Merge.kif 13190-13199
( ! [V__PRES,V__MELT,V__X,V__Y,V__TEMP] :
   (((s__instance(V__PRES,s__RealNumber) &
         s__instance(V__MELT,s__RealNumber) &
         s__instance(V__X,s__Object) &
         s__instance(V__Y,s__Class) &
         s__subclass(V__Y,s__PureSubstance) &
         s__instance(V__TEMP,s__RealNumber))
       =>
       (((s__instance(V__X,V__Y)
           &
           s__subclass(V__Y,s__PureSubstance) &
           s__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
         &
         s__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
       &
       s__greaterThan(V__PRES,n__29_92)
     &
     s__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
   &
   s__lessThan(V__TEMP,V__MELT))
=>
(s__attribute(V__X,s__Solid)))))
)
)

 Merge.kif 13201-13210
( ! [V__N1,V__N2,V__Y1,V__Y2,V__T1,V__T2] :
   (((s__instance(V__N1,s__Integer) &
         s__instance(V__N2,s__Integer) &
         s__instance(V__Y1,s__TimeInterval) &
         s__instance(V__Y2,s__TimeInterval) &
         s__instance(V__T1,s__TimePoint) &
         s__instance(V__T2,s__TimePoint))
       =>
       (((s__instance(V__Y1,s__YearFn(V__N1))
         &
         s__instance(V__Y2,s__YearFn(V__N2))
     &
     (V__T1 = s__BeginFn(V__Y1))
   &
   (V__T2 = s__BeginFn(V__Y2))
&
s__greaterThan(V__N2,V__N1))
=>
(s__before(V__T1,V__T2)))))
)
)

 Merge.kif 8341-8348
( ! [V__N1,V__N2,V__Y1,V__Y2] :
   (((s__instance(V__N1,s__Integer) &
         s__instance(V__N2,s__Integer) &
         s__instance(V__Y1,s__TimeInterval) &
         s__instance(V__Y2,s__TimeInterval))
       =>
       (((s__instance(V__Y1,s__YearFn(V__N1))
         &
         s__instance(V__Y2,s__YearFn(V__N2))
     &
     s__greaterThan(V__N2,V__N1))
=>
(s__earlier(V__Y1,V__Y2)))))
)
)

 Merge.kif 8350-8355

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ! [V__LAND,V__WATER,V__DIST] :
   (((s__instance(V__LAND,s__Physical) &
         s__instance(V__WATER,s__Object) &
         s__instance(V__DIST,s__RealNumber))
       =>
       (((s__attribute(V__WATER,s__OpenSea) =>
             (s__instance(V__WATER,s__SaltWaterArea) &
               ~(s__instance(V__WATER,s__LandlockedWater))
               &
               s__distance(V__LAND,V__WATER,s__MeasureFn(V__DIST,s__NauticalMile))
             &
             s__greaterThan(V__DIST,n__5)))
       &
       ((s__instance(V__WATER,s__SaltWaterArea) &
           ~(s__instance(V__WATER,s__LandlockedWater))
           &
           s__distance(V__LAND,V__WATER,s__MeasureFn(V__DIST,s__NauticalMile))
         &
         s__greaterThan(V__DIST,n__5))
     =>
     s__attribute(V__WATER,s__OpenSea)))))
)
)

 Geography.kif 4506-4514 Open sea is an attribute of an object if and only if the object is an instance of salt water area and the object is not an instance of landlocked water and the distance between a physical and the object is a real number nautical mile(s) and the real number is greater than 5
( ! [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
( ! [V__NUMBER1,V__NUMBER2] :
   (((s__instance(V__NUMBER1,s__Quantity) &
         s__instance(V__NUMBER2,s__Quantity))
       =>
       (((s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2)
           =>
           ((V__NUMBER1 = V__NUMBER2)
             |
             s__greaterThan(V__NUMBER1,V__NUMBER2)))
       &
       (((V__NUMBER1 = V__NUMBER2)
           |
           s__greaterThan(V__NUMBER1,V__NUMBER2))
       =>
       s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2)))))
)
)

 Merge.kif 1832-1836 A quantity is greater than or equal to another quantity if and only if the quantity is equal to the other quantity or the quantity is greater than the other quantity
( ! [V__NUMBER] :
   (((s__instance(V__NUMBER,s__PositiveRealNumber) =>
         (s__greaterThan(V__NUMBER,n__0)
         &
         s__instance(V__NUMBER,s__RealNumber)))
     &
     ((s__greaterThan(V__NUMBER,n__0)
       &
       s__instance(V__NUMBER,s__RealNumber))
     =>
     s__instance(V__NUMBER,s__PositiveRealNumber)))
)
)

 Merge.kif 1884-1888 A quantity is an instance of positive real number if and only if the quantity is greater than 0 and the quantity is an instance of real number
( ! [V__OBJ1,V__OBJ2] :
   (((s__instance(V__OBJ1,s__Object) &
         s__instance(V__OBJ2,s__Object))
       =>
       (((s__larger(V__OBJ1,V__OBJ2)
           =>
           ( ! [V__QUANT1, V__QUANT2, V__UNIT] :
             (((s__instance(V__QUANT1,s__RealNumber) &
                   s__instance(V__QUANT2,s__RealNumber))
                 =>
                 (((s__measure(V__OBJ1,s__MeasureFn(V__QUANT1,V__UNIT))
                   &
                   s__measure(V__OBJ2,s__MeasureFn(V__QUANT2,V__UNIT))
               &
               s__instance(V__UNIT,s__UnitOfLength))
             =>
             (s__greaterThan(V__QUANT1,V__QUANT2))))))))
&
(( ! [V__QUANT1, V__QUANT2, V__UNIT] :
   (((s__instance(V__QUANT1,s__RealNumber) &
         s__instance(V__QUANT2,s__RealNumber))
       =>
       (((s__measure(V__OBJ1,s__MeasureFn(V__QUANT1,V__UNIT))
         &
         s__measure(V__OBJ2,s__MeasureFn(V__QUANT2,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfLength))
   =>
   (s__greaterThan(V__QUANT1,V__QUANT2)))))))
=>
s__larger(V__OBJ1,V__OBJ2)))))
)
)

 Merge.kif 7544-7552 An object is larger than another object if and only if for all a real number, another real number and an unit of measure
( ! [V__AREA,V__ZONE,V__SLOPE] :
   (((s__instance(V__AREA,s__Object) &
         s__instance(V__ZONE,s__LandArea) &
         s__instance(V__SLOPE,s__NonnegativeRealNumber))
       =>
       (((s__attribute(V__AREA,s__FlatTerrain) &
             s__part(V__ZONE,V__AREA)
           &
           s__slopeGradient(V__ZONE,V__SLOPE))
       =>
       (s__greaterThan(n__0_005,V__SLOPE)))))
)
)

 Geography.kif 1725-1730
( ! [V__AREA,V__ZONE,V__SLOPE] :
   (((s__instance(V__AREA,s__Object) &
         s__instance(V__ZONE,s__LandArea) &
         s__instance(V__SLOPE,s__NonnegativeRealNumber))
       =>
       (((s__attribute(V__AREA,s__LowTerrain) &
             s__part(V__ZONE,V__AREA)
           &
           s__slopeGradient(V__ZONE,V__SLOPE))
       =>
       (s__greaterThan(n__0_03,V__SLOPE)))))
)
)

 Geography.kif 1737-1742
( ! [V__FOOD1,V__FOOD2,V__MEAS1,V__U,V__MEAS2,V__CLASS] :
   (((s__instance(V__FOOD1,s__Object) &
         s__instance(V__FOOD2,s__Object) &
         s__instance(V__MEAS1,s__RealNumber) &
         s__instance(V__MEAS2,s__RealNumber) &
         s__instance(V__CLASS,s__Class))
       =>
       (((s__attribute(V__FOOD1,s__FamilyStylePortion) &
             s__measure(V__FOOD1,s__MeasureFn(V__MEAS1,V__U))
         &
         ~(s__attribute(V__FOOD2,s__FamilyStylePortion))
         &
         s__measure(V__FOOD2,s__MeasureFn(V__MEAS2,V__U))
     &
     s__instance(V__FOOD1,V__CLASS)
   &
   s__instance(V__FOOD2,V__CLASS)
&
s__instance(V__U,s__UnitOfMeasure))
=>
(s__greaterThan(V__MEAS1,V__MEAS2)))))
)
)

 Dining.kif 1118-1129
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 193-212
( ! [V__ROOM,V__HOTELUNIT] :
   (((s__instance(V__ROOM,s__Object) &
         s__instance(V__HOTELUNIT,s__Class))
       =>
       (((s__attribute(V__ROOM,s__Oversized) &
             s__immediateInstance(V__ROOM,V__HOTELUNIT)
           &
           s__subclass(V__HOTELUNIT,s__HotelUnit))
         =>
         (( ? [V__NORMAL, V__AREA1, V__AREA2, V__U] :
             ((s__instance(V__NORMAL,s__Physical) &
                 (s__immediateInstance(V__NORMAL,V__HOTELUNIT)
                 &
                 s__instance(V__U,s__UnitOfArea) &
                 s__measure(V__NORMAL,s__MeasureFn(V__AREA1,V__U))
             &
             s__measure(V__ROOM,s__MeasureFn(V__AREA2,V__U))
         &
         s__instance(V__AREA1,s__AreaMeasure) &
         s__instance(V__AREA2,s__AreaMeasure) &
         s__greaterThan(V__AREA2,V__AREA1)))))))))
)
)

 Hotel.kif 1164-1179
( ! [V__CAPAMOUNT,V__AREA,V__PERIOD,V__TOTALAMOUNT] :
   (((s__instance(V__CAPAMOUNT,s__CurrencyMeasure) &
         s__instance(V__AREA,s__GeopoliticalArea) &
         s__subclass(V__PERIOD,s__TimeInterval) &
         s__instance(V__TOTALAMOUNT,s__CurrencyMeasure))
       =>
       (((s__capitalExpendituresOfAreaInPeriod(V__AREA,V__CAPAMOUNT,V__PERIOD)
           &
           s__annualExpendituresOfAreaInPeriod(V__AREA,V__TOTALAMOUNT,V__PERIOD))
       =>
       (s__greaterThan(V__TOTALAMOUNT,V__CAPAMOUNT)))))
)
)

 Economy.kif 1544-1548
No TPTP formula. May not be expressible in strict first order. Cars.kif 809-825
No TPTP formula. May not be expressible in strict first order. Merge.kif 17729-17734
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12873-12882
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12884-12895
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12823-12833
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 12903-12912
No TPTP formula. May not be expressible in strict first order. Merge.kif 17712-17717
No TPTP formula. May not be expressible in strict first order. Cars.kif 2585-2603
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17583-17597
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3670-3678
No TPTP formula. May not be expressible in strict first order. Cars.kif 2884-2902
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 23209-23226
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 5578-5585
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 29894-29915

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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