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 1766-1768
s__domain(s__greaterThan__m,n__1,s__Quantity)

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

Merge.kif 1763-1763 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 1756-1756 greater than is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__SetOrClass)

s__instance(s__greaterThan__m,s__IrreflexiveRelation)

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

s__instance(s__RelationExtendedToQuantities,s__SetOrClass)

Merge.kif 1760-1760 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 1757-1757 greater than is an instance of total valued relation
s__instance(s__TransitiveRelation,s__SetOrClass)

s__instance(s__greaterThan__m,s__TransitiveRelation)

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

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

Merge.kif 1761-1761 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 14744-14761
( ! [V__A,V__L] :
   (((s__instance(V__A,s__Number) &
         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 3168-3175
( ! [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__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 2898-2916
( ! [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 8332-8339
( ! [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 8341-8346
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 13199-13214
( ! [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 13134-13143
( ! [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 13145-13154
( ! [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 13156-13165
( ! [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 8300-8307
( ! [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 8309-8314

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 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__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 1799-1803 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 1851-1855 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 7503-7511 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 1151-1166
( ! [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 17589-17594
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11912-11921
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11923-11934
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11862-11872
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 11942-11951
No TPTP formula. May not be expressible in strict first order. Merge.kif 17573-17578
No TPTP formula. May not be expressible in strict first order. Cars.kif 2599-2617
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16515-16529
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 3649-3657
No TPTP formula. May not be expressible in strict first order. Cars.kif 2898-2916
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 22127-22144
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 5561-5568
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 28801-28822

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