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

Formal Language: 



KB Term:  Term intersection
English Word: 

  greaterThan

Sigma KEE - greaterThan
greaterThan

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


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

Merge.kif 1919-1920
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 1916-1918
s__domain(s__greaterThan__m,1,s__Quantity)

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

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

s__instance(s__greaterThan__m,s__BinaryPredicate)

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

s__instance(s__greaterThan__m,s__IrreflexiveRelation)

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

s__instance(s__RelationExtendedToQuantities,s__SetOrClass)

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

s__instance(s__greaterThan__m,s__TotalValuedRelation)

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

s__instance(s__greaterThan__m,s__TransitiveRelation)

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

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

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

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


s__comparativeArea(s__SouthernOcean,s__greaterThan__m,2,s__UnitedStates)

Geography.kif 4381-4381 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 82-82
s__termFormat(s__ChineseLanguage,s__greaterThan__m,'大于')

chinese_format.kif 112-112 "大于" is the printable form of greater than in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__greaterThan__m,'greater than')

domainEnglishFormat.kif 4843-4843 "greater than" is the printable form of greater than in english language

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


No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 952-956 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__and__ms__instance(V__S,s__RealNumber))
    s__=>((s__instance(V__PM,s__ParticulateMatter)s__and__ms__part(V__P,V__PM)
      s__and__ms__approximateDiameter(V__P,s__MeasureFn(V__S,s__Micrometer))
    s__and__ms__greaterThan(10,V__S)
  s__and__ms__greaterThan(V__S,2.5))
s__<⇒
(s__exists__m[V__PM10]
(s__instance(V__PM10,s__CoarseParticulateMatter)s__and__ms__part(V__PM10,V__PM)))))
)

Geography.kif 6790-6801 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 802-815
( ∀ [V__TEXT,V__EDITION1,V__EDITION2,V__INT2,V__DATE1,V__INT1,V__DATE2,V__PUB1,V__PUB2,V__CBO1,V__CBO2]
   ((s__subclass(V__TEXT,s__ContentBearingObject)s__and__ms__subclass(V__EDITION1,s__ContentBearingObject)s__and__ms__instance(V__EDITION1,s__SetOrClass)s__and__ms__subclass(V__EDITION2,s__ContentBearingObject)s__and__ms__instance(V__EDITION2,s__SetOrClass)s__and__ms__instance(V__INT2,s__PositiveInteger)s__and__ms__instance(V__DATE1,s__Day)s__and__ms__instance(V__INT1,s__PositiveInteger)s__and__ms__instance(V__DATE2,s__Day))
    s__=>(((s__EditionFn(V__TEXT,V__INT1)
        s__equal__mV__EDITION1)s__and__m(s__EditionFn(V__TEXT,V__INT2)
      s__equal__mV__EDITION2)s__and__ms__greaterThan(V__INT2,V__INT1)
    s__and__ms__instance(V__PUB1,s__Publication)s__and__ms__instance(V__PUB2,s__Publication)s__and__ms__instance(V__CBO1,V__EDITION1)
  s__and__ms__instance(V__CBO2,V__EDITION2)
s__and__ms__patient(V__PUB1,V__CBO1)
s__and__ms__patient(V__PUB2,V__CBO2)
s__and__ms__date(V__PUB1,V__DATE1)
s__and__ms__date(V__PUB2,V__DATE2))
s__=>s__before(s__EndFn(V__DATE1)
,s__EndFn(V__DATE2))))
)

Merge.kif 15632-15649
( ∀ [V__COUNT,V__HOME,V__REGISTER,V__MM]
   ((s__instance(V__COUNT,s__NonnegativeInteger)s__and__ms__instance(V__HOME,s__GeopoliticalArea)s__and__ms__instance(V__REGISTER,s__ShipRegister)s__and__ms__instance(V__MM,s__MerchantMarine))
    s__=>((s__fOCShipsByOrigin(V__MM,V__HOME,V__COUNT)
      s__and__ms__greaterThan(V__COUNT,0)
    s__and__ms__marineInventory(V__MM,V__REGISTER))
s__=>s__instance(V__REGISTER,s__FlagOfConvenienceRegister)))
)

Transportation.kif 1044-1049
No TPTP formula. May not be expressible in strict first order. Cars.kif 2865-2879
( ∀ [V__MO,V__TEMP,V__AREA]
   ((s__instance(V__MO,s__TimeDuration)s__and__ms__instance(V__MO,s__SetOrClass)s__and__ms__instance(V__TEMP,s__TemperatureMeasure))
    s__=>((s__instance(V__AREA,s__DesertClimateZone)s__and__ms__subclass(V__MO,s__Month)s__and__ms__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP)
      s__and__ms__greaterThan(V__TEMP,s__MeasureFn(18,s__CelsiusDegree)))
  s__=>s__instance(V__AREA,s__SubtropicalDesertClimateZone)))
)

Geography.kif 1340-1346
( ∀ [V__MO,V__TEMP,V__AREA]
   ((s__instance(V__MO,s__TimeDuration)s__and__ms__instance(V__MO,s__SetOrClass)s__and__ms__instance(V__TEMP,s__TemperatureMeasure))
    s__=>((s__instance(V__AREA,s__GeographicArea)s__and__ms__subclass(V__MO,s__Month)s__and__ms__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP)
      s__and__ms__greaterThan(s__MeasureFn(10,s__CelsiusDegree),V__TEMP))
  s__=>s__instance(V__AREA,s__PolarClimateZone)))
)

Geography.kif 1518-1524
( ∀ [V__OFFER1,V__OFFER2,V__AUCTIONING,V__BIDDER1,V__BIDDER2,V__ITEM]
   ((s__instance(V__OFFER1,s__CurrencyMeasure)s__and__ms__instance(V__OFFER2,s__CurrencyMeasure))
    s__=>((s__instance(V__AUCTIONING,s__Auctioning)s__and__ms__instance(V__BIDDER1,s__Agent)s__and__ms__instance(V__BIDDER2,s__Agent)s__and__ms__instance(V__ITEM,s__Object)s__and__ms__patient(V__AUCTIONING,V__ITEM)
      s__and__ms__bidPrice(V__ITEM,V__OFFER1,V__BIDDER1)
    s__and__ms__bidPrice(V__ITEM,V__OFFER2,V__BIDDER2)
  s__and__ms__greaterThan(V__OFFER1,V__OFFER2))
s__=>s__destination(V__AUCTIONING,V__BIDDER1)))
)

UXExperimentalTerms.kif 437-447
( ∀ [V__N1,V__N2,V__Y,V__D1,V__T1,V__D2,V__T2,V__M]
   ((s__instance(V__N1,s__PositiveInteger)s__and__ms__instance(V__N2,s__PositiveInteger)s__and__ms__instance(V__Y,s__Integer)s__and__ms__instance(V__D1,s__TimeInterval)s__and__ms__instance(V__T1,s__TimePoint)s__and__ms__instance(V__D2,s__TimeInterval)s__and__ms__instance(V__T2,s__TimePoint)s__and__ms__subclass(V__M,s__Month))
    s__=>((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y))))
s__and__ms__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y))))
s__and__m(V__T1s__equal__ms__BeginFn(V__D1))
s__and__m(V__T2s__equal__ms__BeginFn(V__D2))
s__and__ms__greaterThan(V__N2,V__N1))
s__=>s__before(V__T1,V__T2)))
)

Merge.kif 8859-8866
( ∀ [V__N1,V__N2,V__Y,V__D1,V__D2,V__M]
   ((s__instance(V__N1,s__PositiveInteger)s__and__ms__instance(V__N2,s__PositiveInteger)s__and__ms__instance(V__Y,s__Integer)s__and__ms__instance(V__D1,s__TimeInterval)s__and__ms__instance(V__D2,s__TimeInterval)s__and__ms__subclass(V__M,s__Month))
    s__=>((s__instance(V__D1,s__DayFn(V__N1,s__MonthFn(V__M,s__YearFn(V__Y))))
s__and__ms__instance(V__D2,s__DayFn(V__N2,s__MonthFn(V__M,s__YearFn(V__Y))))
s__and__ms__greaterThan(V__N2,V__N1))
s__=>s__earlier(V__D1,V__D2)))
)

Merge.kif 8868-8873
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 492-498
( ∀ [V__NUM,V__HARBOR]
   (s__instance(V__NUM,s__Quantity)s__=>((s__instance(V__HARBOR,s__Harbor)s__and__ms__equipmentCount(V__HARBOR,s__ShipBerth,V__NUM)
      s__and__ms__greaterThan(V__NUM,0))
  s__=>s__capability(s__ShipBerthing,s__path__m,V__HARBOR)))
)

Transportation.kif 2886-2891
No TPTP formula. May not be expressible in strict first order. Merge.kif 13854-13869
( ∀ [V__PRES,V__X,V__BOIL,V__Y,V__TEMP]
   ((s__instance(V__PRES,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__instance(V__BOIL,s__RealNumber)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber))
    s__=>((s__instance(V__X,V__Y)
      s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
    s__and__ms__greaterThan(29.92,V__PRES)
  s__and__ms__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
s__and__ms__greaterThan(V__TEMP,V__BOIL))
s__=>s__attribute(V__X,s__Gas)))
)

Merge.kif 13787-13796
( ∀ [V__MELT,V__X,V__BOIL,V__Y,V__TEMP]
   ((s__instance(V__MELT,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__instance(V__BOIL,s__RealNumber)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber))
    s__=>((s__instance(V__X,V__Y)
      s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__boilingPoint(V__Y,s__MeasureFn(V__BOIL,s__KelvinDegree))
    s__and__ms__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
  s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
s__and__ms__greaterThan(V__TEMP,V__MELT)
s__and__ms__lessThan(V__TEMP,V__BOIL))
s__=>s__attribute(V__X,s__Liquid)))
)

Merge.kif 13798-13807
( ∀ [V__PRES,V__MELT,V__X,V__Y,V__TEMP]
   ((s__instance(V__PRES,s__RealNumber)s__and__ms__instance(V__MELT,s__RealNumber)s__and__ms__instance(V__X,s__Object)s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__instance(V__Y,s__SetOrClass)s__and__ms__instance(V__TEMP,s__RealNumber))
    s__=>((s__instance(V__X,V__Y)
      s__and__ms__subclass(V__Y,s__PureSubstance)s__and__ms__meltingPoint(V__Y,s__MeasureFn(V__MELT,s__KelvinDegree))
    s__and__ms__barometricPressure(V__X,s__MeasureFn(V__PRES,s__InchMercury))
  s__and__ms__greaterThan(V__PRES,29.92)
s__and__ms__measure(V__X,s__MeasureFn(V__TEMP,s__KelvinDegree))
s__and__ms__lessThan(V__TEMP,V__MELT))
s__=>s__attribute(V__X,s__Solid)))
)

Merge.kif 13809-13818
( ∀ [V__N1,V__N2,V__Y1,V__Y2,V__T1,V__T2]
   ((s__instance(V__N1,s__Integer)s__and__ms__instance(V__N2,s__Integer)s__and__ms__instance(V__Y1,s__TimeInterval)s__and__ms__instance(V__Y2,s__TimeInterval)s__and__ms__instance(V__T1,s__TimePoint)s__and__ms__instance(V__T2,s__TimePoint))
    s__=>((s__instance(V__Y1,s__YearFn(V__N1))
    s__and__ms__instance(V__Y2,s__YearFn(V__N2))
s__and__m(V__T1s__equal__ms__BeginFn(V__Y1))
s__and__m(V__T2s__equal__ms__BeginFn(V__Y2))
s__and__ms__greaterThan(V__N2,V__N1))
s__=>s__before(V__T1,V__T2)))
)

Merge.kif 8827-8834
( ∀ [V__N1,V__N2,V__Y1,V__Y2]
   ((s__instance(V__N1,s__Integer)s__and__ms__instance(V__N2,s__Integer)s__and__ms__instance(V__Y1,s__TimeInterval)s__and__ms__instance(V__Y2,s__TimeInterval))
    s__=>((s__instance(V__Y1,s__YearFn(V__N1))
    s__and__ms__instance(V__Y2,s__YearFn(V__N2))
s__and__ms__greaterThan(V__N2,V__N1))
s__=>s__earlier(V__Y1,V__Y2)))
)

Merge.kif 8836-8841
( ∀ [V__AREA,V__LENGTH,V__UNIT]
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__LENGTH,s__RealNumber))
    s__=>((s__lengthOfBroadGaugeRailway(V__AREA,s__MeasureFn(V__LENGTH,V__UNIT))
    s__and__ms__instance(V__UNIT,s__UnitOfLength)s__and__ms__greaterThan(V__LENGTH,0))
s__=>(s__exists__m[V__RAILWAY]
   (s__instance(V__RAILWAY,s__BroadGaugeRailway)s__and__ms__located(V__RAILWAY,V__AREA)))))
)

Transportation.kif 188-196
( ∀ [V__AREA,V__LENGTH,V__UNIT]
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__LENGTH,s__RealNumber))
    s__=>((s__lengthOfDualGaugeRailway(V__AREA,s__MeasureFn(V__LENGTH,V__UNIT))
    s__and__ms__instance(V__UNIT,s__UnitOfLength)s__and__ms__greaterThan(V__LENGTH,0))
s__=>(s__exists__m[V__RAILWAY]
   (s__instance(V__RAILWAY,s__DualGaugeRailway)s__and__ms__located(V__RAILWAY,V__AREA)))))
)

Transportation.kif 216-224
( ∀ [V__AREA,V__LENGTH]
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__LENGTH,s__LengthMeasure))
    s__=>((s__lengthOfElectrifiedRailway(V__AREA,V__LENGTH)
      s__and__ms__greaterThan(V__LENGTH,0))
  s__=>(s__exists__m[V__RAILWAY]
     (s__instance(V__RAILWAY,s__ElectrifiedRailway)s__and__ms__located(V__RAILWAY,V__AREA)))))
)

Transportation.kif 134-141
( ∀ [V__AREA,V__LENGTH,V__UNIT]
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__LENGTH,s__RealNumber))
    s__=>((s__lengthOfExpresswaySystem(V__AREA,s__MeasureFn(V__LENGTH,V__UNIT))
    s__and__ms__instance(V__UNIT,s__UnitOfLength)s__and__ms__greaterThan(V__LENGTH,0))
s__=>(s__exists__m[V__HIGHWAY]
   (s__instance(V__HIGHWAY,s__Expressway)s__and__ms__located(V__HIGHWAY,V__AREA)))))
)

Transportation.kif 567-575
( ∀ [V__AREA,V__LENGTH]
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__LENGTH,s__LengthMeasure))
    s__=>((s__lengthOfMultipleTrackRailway(V__AREA,V__LENGTH)
      s__and__ms__greaterThan(V__LENGTH,0))
  s__=>(s__exists__m[V__RAILWAY]
     (s__instance(V__RAILWAY,s__MultipleTrackRailway)s__and__ms__located(V__RAILWAY,V__AREA)))))
)

Transportation.kif 161-168
( ∀ [V__AREA,V__LENGTH,V__UNIT]
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__LENGTH,s__RealNumber))
    s__=>((s__lengthOfNarrowGaugeRailway(V__AREA,s__MeasureFn(V__LENGTH,V__UNIT))
    s__and__ms__instance(V__UNIT,s__UnitOfLength)s__and__ms__greaterThan(V__LENGTH,0))
s__=>(s__exists__m[V__RAILWAY]
   (s__instance(V__RAILWAY,s__NarrowGaugeRailway)s__and__ms__located(V__RAILWAY,V__AREA)))))
)

Transportation.kif 243-251

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


( ∀ [V__WATER,V__DIST,V__AREA]
   ((s__instance(V__WATER,s__Object)s__and__ms__instance(V__DIST,s__LengthMeasure))
    s__=>(s__attribute(V__WATER,s__OpenSea)s__<⇒
      (s__forall__m[V__LAND]
         (s__instance(V__LAND,s__Physical)s__=>(s__instance(V__AREA,s__SaltWaterArea)s__and__m(s__not__ms__instance(V__WATER,s__LandlockedWater))
          s__and__ms__distance(V__LAND,V__WATER,V__DIST)
        s__and__ms__greaterThan(V__DIST,s__MeasureFn(5,s__NauticalMile)))))))
)

Geography.kif 4408-4415 Open sea is an attribute of an object if and only if for all a physical an entity is an instance of salt water area and the object is not an instance of landlocked water and the distance between the physical and the object is a length measure and the length measure is greater than 5 nautical mile(s)
( ∀ [V__LASTPLACE,V__LIST1,V__AVERAGE]
   ((s__instance(V__LASTPLACE,s__PositiveInteger)s__and__ms__instance(V__LIST1,s__List)s__and__ms__instance(V__AVERAGE,s__RealNumber))
    s__=>(s__average(V__LIST1,V__AVERAGE)
    s__<⇒
    (s__exists__m[V__LIST2]
       (s__instance(V__LIST2,s__List)s__and__m((s__ListLengthFn(V__LIST2)
        s__equal__ms__ListLengthFn(V__LIST1))
    s__and__m(s__ListOrderFn(V__LIST2,1)
  s__equal__ms__ListOrderFn(V__LIST1,1))
s__and__m(s__forall__m[V__ITEMFROM2]
(s__instance(V__ITEMFROM2,s__PositiveInteger)s__=>(s__inList(V__ITEMFROM2,V__LIST2)
s__=>(s__exists__m[V__POSITION,V__POSITIONMINUSONE,V__ITEMFROM1,V__PRIORFROM2]
   (s__instance(V__POSITION,s__Quantity)s__and__ms__instance(V__POSITIONMINUSONE,s__Quantity)s__and__ms__instance(V__ITEMFROM1,s__PositiveInteger)s__and__ms__instance(V__PRIORFROM2,s__PositiveInteger)s__and__m(s__greaterThan(V__POSITION,1)
  s__and__ms__lessThanOrEqualTo(V__POSITION,s__ListLengthFn(V__LIST2))
s__and__m(s__ListOrderFn(V__LIST2,V__ITEMFROM2)
s__equal__mV__POSITION)s__and__ms__inList(V__ITEMFROM1,V__LIST1)
s__and__m(V__POSITIONs__equal__ms__ListOrderFn(V__LIST1,V__ITEMFROM1))
s__and__ms__inList(V__PRIORFROM2,V__LIST2)
s__and__m(V__POSITIONMINUSONEs__equal__ms__SubtractionFn(V__POSITION,1))
s__and__m(V__POSITIONMINUSONEs__equal__ms__ListOrderFn(V__LIST2,V__PRIORFROM2))
s__and__m(V__ITEMFROM2s__equal__ms__AdditionFn(V__ITEMFROM1,V__PRIORFROM2))))))))
s__and__m(V__LASTPLACEs__equal__ms__ListLengthFn(V__LIST2))
s__and__m(V__AVERAGEs__equal__ms__DivisionFn(s__ListOrderFn(V__LIST2,V__LASTPLACE)
,V__LASTPLACE)))))))
)

People.kif 285-306 A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer
( ∀ [V__NUMBER1,V__NUMBER2]
   ((s__instance(V__NUMBER1,s__Quantity)s__and__ms__instance(V__NUMBER2,s__Quantity))
    s__=>(s__greaterThanOrEqualTo(V__NUMBER1,V__NUMBER2)
    s__<⇒
    ((V__NUMBER1s__equal__mV__NUMBER2)s__or__ms__greaterThan(V__NUMBER1,V__NUMBER2))))
)

Merge.kif 1953-1957 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__<⇒
    (s__greaterThan(V__NUMBER,0)
    s__and__ms__instance(V__NUMBER,s__RealNumber)))
)

Merge.kif 2009-2013 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__and__ms__instance(V__OBJ2,s__Object))
    s__=>(s__larger(V__OBJ1,V__OBJ2)
    s__<⇒
    (s__forall__m[V__QUANT1,V__QUANT2,V__UNIT]
       ((s__instance(V__QUANT1,s__RealNumber)s__and__ms__instance(V__QUANT2,s__RealNumber))
        s__=>((s__measure(V__OBJ1,s__MeasureFn(V__QUANT1,V__UNIT))
        s__and__ms__measure(V__OBJ2,s__MeasureFn(V__QUANT2,V__UNIT))
    s__and__ms__instance(V__UNIT,s__UnitOfLength))
  s__=>s__greaterThan(V__QUANT1,V__QUANT2))))))
)

Merge.kif 7963-7971 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__and__ms__instance(V__ZONE,s__LandArea)s__and__ms__instance(V__SLOPE,s__NonnegativeRealNumber))
    s__=>((s__attribute(V__AREA,s__FlatTerrain)s__and__ms__part(V__ZONE,V__AREA)
      s__and__ms__slopeGradient(V__ZONE,V__SLOPE))
  s__=>s__greaterThan(0.005,V__SLOPE)))
)

Geography.kif 1695-1700
( ∀ [V__AREA,V__ZONE,V__SLOPE]
   ((s__instance(V__AREA,s__Object)s__and__ms__instance(V__ZONE,s__LandArea)s__and__ms__instance(V__SLOPE,s__NonnegativeRealNumber))
    s__=>((s__attribute(V__AREA,s__LowTerrain)s__and__ms__part(V__ZONE,V__AREA)
      s__and__ms__slopeGradient(V__ZONE,V__SLOPE))
  s__=>s__greaterThan(0.03,V__SLOPE)))
)

Geography.kif 1707-1712
( ∀ [V__FOOD1,V__FOOD2,V__MEAS1,V__MEAS2,V__CLASS]
   ((s__instance(V__FOOD1,s__Object)s__and__ms__instance(V__FOOD2,s__Object)s__and__ms__instance(V__MEAS1,s__PhysicalQuantity)s__and__ms__instance(V__MEAS2,s__PhysicalQuantity)s__and__ms__instance(V__CLASS,s__SetOrClass))
    s__=>((s__attribute(V__FOOD1,s__FamilyStylePortion)s__and__ms__measure(V__FOOD1,V__MEAS1)
      s__and__m(s__not__ms__attribute(V__FOOD2,s__FamilyStylePortion))
    s__and__ms__measure(V__FOOD2,V__MEAS2)
  s__and__ms__instance(V__FOOD1,V__CLASS)
s__and__ms__instance(V__FOOD2,V__CLASS))
s__=>s__greaterThan(V__MEAS1,V__MEAS2)))
)

Dining.kif 1119-1127
No TPTP formula. May not be expressible in strict first order. ArabicCulture.kif 193-210
( ∀ [V__ROOM,V__HOTELUNIT]
   ((s__instance(V__ROOM,s__Object)s__and__ms__instance(V__HOTELUNIT,s__SetOrClass))
    s__=>((s__attribute(V__ROOM,s__Oversized)s__and__ms__immediateInstance(V__ROOM,V__HOTELUNIT)
      s__and__ms__subclass(V__HOTELUNIT,s__HotelUnit))
    s__=>(s__exists__m[V__NORMAL,V__AREA1,V__AREA2]
       (s__instance(V__NORMAL,s__Object)s__and__m(s__immediateInstance(V__NORMAL,V__HOTELUNIT)
      s__and__ms__measure(V__NORMAL,V__AREA1)
    s__and__ms__measure(V__ROOM,V__AREA2)
  s__and__ms__instance(V__AREA1,s__AreaMeasure)s__and__ms__instance(V__AREA2,s__AreaMeasure)s__and__ms__greaterThan(V__AREA2,V__AREA1))))))
)

Hotel.kif 1136-1148
( ∀ [V__CAPAMOUNT,V__AREA,V__PERIOD,V__TOTALAMOUNT]
   ((s__instance(V__CAPAMOUNT,s__CurrencyMeasure)s__and__ms__instance(V__AREA,s__GeopoliticalArea)s__and__ms__subclass(V__PERIOD,s__TimeInterval)s__and__ms__instance(V__TOTALAMOUNT,s__CurrencyMeasure))
    s__=>((s__capitalExpendituresOfAreaInPeriod(V__AREA,V__CAPAMOUNT,V__PERIOD)
      s__and__ms__annualExpendituresOfAreaInPeriod(V__AREA,V__TOTALAMOUNT,V__PERIOD))
  s__=>s__greaterThan(V__TOTALAMOUNT,V__CAPAMOUNT)))
)

Economy.kif 1544-1548
No TPTP formula. May not be expressible in strict first order. Cars.kif 802-815
No TPTP formula. May not be expressible in strict first order. Merge.kif 18835-18840
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11131-11140
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11141-11152
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11086-11094
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11160-11169
No TPTP formula. May not be expressible in strict first order. Merge.kif 18820-18825
( ∀ [V__AGENT,V__NUMBER1,V__NUMBER2]
   ((s__subclass(V__AGENT,s__BiochemicalAgent)s__and__ms__instance(V__NUMBER1,s__FunctionQuantity)s__and__ms__instance(V__NUMBER2,s__FunctionQuantity))
    s__=>((s__effectiveDose(V__AGENT,V__NUMBER1)
      s__and__ms__lethalDose(V__AGENT,V__NUMBER2))
  s__=>s__greaterThan(V__NUMBER2,V__NUMBER1)))
)

WMD.kif 812-816
No TPTP formula. May not be expressible in strict first order. Cars.kif 2571-2584
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3600-3608
No TPTP formula. May not be expressible in strict first order. Cars.kif 2865-2879
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28798-28819
No TPTP formula. May not be expressible in strict first order. Economy.kif 1562-1566
( ∀ [V__NORMAL,V__BIG,V__CLASS]
   ((s__instance(V__NORMAL,s__Object)s__and__ms__instance(V__BIG,s__Object))
    s__=>((s__immediateInstance(V__BIG,V__CLASS)
      s__and__ms__immediateInstance(V__NORMAL,V__CLASS)
    s__and__ms__attribute(V__BIG,s__Oversized))
  s__=>(s__exists__m[V__BIGSIZE,V__NORMALSIZE]
     (s__instance(V__BIGSIZE,s__PhysicalQuantity)s__and__ms__instance(V__NORMALSIZE,s__PhysicalQuantity)s__and__m(s__measure(V__BIG,V__BIGSIZE)
    s__and__ms__measure(V__NORMAL,V__NORMALSIZE)
  s__and__ms__greaterThan(V__BIGSIZE,V__NORMALSIZE))))))
)

Hotel.kif 1125-1134

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


Show simplified definition (without tree view)
Show simplified definition (with tree view)

Show without tree


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