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

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - greaterThanOrEqualTo
greaterThanOrEqualTo

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


s__documentation(s__greaterThanOrEqualTo__m,s__ChineseLanguage,'"(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2) 是真的以防 ?NUMBER1 的 Quantity 多于或者等于 ?NUMBER2 的 Quantity。"')

chinese_format.kif 1735-1736
s__documentation(s__greaterThanOrEqualTo__m,s__EnglishLanguage,'"(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2) is true just in case the Quantity ?NUMBER1 is greater than or equal to the Quantity ?NUMBER2."')

Merge.kif 1828-1830
s__domain(s__greaterThanOrEqualTo__m,n__1,s__Quantity)

Merge.kif 1824-1824 The number 1 argument of greater than or equal to is an instance of quantity
s__domain(s__greaterThanOrEqualTo__m,n__2,s__Quantity)

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

s__instance(s__greaterThanOrEqualTo__m,s__BinaryPredicate)

Merge.kif 1820-1820 greater than or equal to is an instance of binary predicate
s__instance(s__greaterThanOrEqualTo__m,s__PartialOrderingRelation)

s__instance(s__PartialOrderingRelation,s__Class)

Merge.kif 1821-1821 greater than or equal to is an instance of partial ordering relation
s__instance(s__RelationExtendedToQuantities,s__Class)

s__instance(s__greaterThanOrEqualTo__m,s__RelationExtendedToQuantities)

Merge.kif 1822-1822 greater than or equal to is an instance of relation extended to quantities
s__inverse(s__greaterThanOrEqualTo__m,s__lessThanOrEqualTo__m)

Merge.kif 1826-1826 greater than or equal to is an inverse of less than or equal to
s__trichotomizingOn(s__greaterThanOrEqualTo__m,s__RealNumber)

Merge.kif 1823-1823 greater than or equal to is trichotomizing on real number

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


s__format(s__ChineseLanguage,s__greaterThanOrEqualTo__m,'"%1 %n 是 greaterThanOrEqualTo %2"')

chinese_format.kif 113-113
s__format(s__EnglishLanguage,s__greaterThanOrEqualTo__m,'"%1 is %n greater than or equal to %2"')

english_format.kif 113-113
s__termFormat(s__ChineseLanguage,s__greaterThanOrEqualTo__m,'"大于或等于"')

chinese_format.kif 114-114
s__termFormat(s__ChineseTraditionalLanguage,s__greaterThanOrEqualTo__m,'"大於或等於"')

domainEnglishFormat.kif 26528-26528
s__termFormat(s__EnglishLanguage,s__greaterThanOrEqualTo__m,'"greater than or equal to"')

domainEnglishFormat.kif 26527-26527

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


( ! [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__greaterThanOrEqualTo(V__S,n__2_5))
       =>
       ( ? [V__PM25] :
         ((s__instance(V__PM25,s__FineParticulateMatter) &
             s__part(V__PM25,V__PM)))))
   &
   (( ? [V__PM25] :
       ((s__instance(V__PM25,s__FineParticulateMatter) &
           s__part(V__PM25,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__greaterThanOrEqualTo(V__S,n__2_5))))))
)
)

Geography.kif 7027-7037 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 the real number is greater than or equal to 2.5 if and only if there exists the object25 such that the object25 is an instance of PM2.5 and the object25 is a part of the object
( ! [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__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__arableLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfArea) &
     (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
    ,V__UNIT)))
=>
(s__arableLandArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 2061-2068
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__arableLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfArea))
   =>
   (( ? [V__ARABLE] :
       ((s__instance(V__ARABLE,s__ArableLand) &
           s__geographicSubregion(V__ARABLE,V__REGION)
         &
         s__measure(V__ARABLE,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
      ,V__UNIT)))))))))
)
)

Geography.kif 2070-2080
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__arableLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,V__TOTAL)
       &
       s__instance(V__TOTAL,s__AreaMeasure) &
       (V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))
   =>
   (s__arableLandArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 2052-2059
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 2002-2023
No TPTP formula. May not be expressible in strict first order. Merge.kif 13210-13223
( ! [V__AREA] :
   (((s__instance(V__AREA,s__TropicalClimateZone) &
         ( ! [V__MO, V__AMOUNT] :
           (((s__instance(V__MO,s__Month) &
                 s__instance(V__AMOUNT,s__RealNumber))
               =>
               ((s__averageRainfallForPeriod(V__AREA,V__MO,s__MeasureFn(V__AMOUNT,s__MilliFn(s__Meter)))
               =>
               (s__greaterThanOrEqualTo(V__AMOUNT,n__60))))))))
=>
(s__instance(V__AREA,s__WetTropicalClimateZone)))
)
)

Geography.kif 1306-1314
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 208-214
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__otherLandUseArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfArea) &
     (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
    ,V__UNIT)))
=>
(s__otherLandUseArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 2151-2158
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__otherLandUseArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfArea))
   =>
   (( ? [V__OTHER] :
       ((s__instance(V__OTHER,s__LandArea) &
           ~(s__instance(V__OTHER,s__ArableLand))
           &
           ~(s__instance(V__OTHER,s__PermanentCropLand))
           &
           s__geographicSubregion(V__OTHER,V__REGION)
         &
         s__measure(V__OTHER,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
      ,V__UNIT)))))))))
)
)

Geography.kif 2160-2172
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__otherLandUseArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,V__TOTAL)
       &
       s__instance(V__TOTAL,s__AreaMeasure) &
       (V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))
   =>
   (s__otherLandUseArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 2142-2149
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__permanentCropLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfArea) &
     (V__AMOUNT = s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
    ,V__UNIT)))
=>
(s__permanentCropLandArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 2109-2116
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__TOTAL,s__RealNumber) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__permanentCropLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
     &
     s__instance(V__UNIT,s__UnitOfArea))
   =>
   (( ? [V__PERMCROP] :
       ((s__instance(V__PERMCROP,s__PermanentCropLand) &
           s__geographicSubregion(V__PERMCROP,V__REGION)
         &
         s__measure(V__PERMCROP,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
      ,V__UNIT)))))))))
)
)

Geography.kif 2118-2128
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION] :
   (((s__instance(V__REGION,s__GeographicArea) &
         s__instance(V__AMOUNT,s__Number) &
         s__instance(V__AMOUNT,s__ConstantQuantity) &
         s__instance(V__FRACTION,s__Number) &
         s__instance(V__FRACTION,s__ConstantQuantity))
       =>
       (((s__permanentCropLandArea(V__REGION,V__FRACTION)
           &
           s__greaterThanOrEqualTo(V__FRACTION,n__0)
         &
         s__totalArea(V__REGION,V__TOTAL)
       &
       s__instance(V__TOTAL,s__AreaMeasure) &
       (V__AMOUNT = s__MultiplicationFn(V__FRACTION,V__TOTAL)))
   =>
   (s__permanentCropLandArea(V__REGION,V__AMOUNT)))))
)
)

Geography.kif 2100-2107
( ! [V__AGENT,V__POLITY,V__AGE,V__VOTINGAGE,V__ELECTION] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__POLITY,s__Nation) &
         s__instance(V__AGE,s__RealNumber) &
         s__instance(V__VOTINGAGE,s__RealNumber) &
         s__instance(V__ELECTION,s__Election))
       =>
       (((s__subProposition(s__CompulsorySuffrageLaw,s__RegionalLawFn(V__POLITY))
         &
         s__citizen(V__AGENT,V__POLITY)
       &
       s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration))
     &
     s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration))
   &
   s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
&
s__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
=>
(( ? [V__VOTING] :
((s__instance(V__VOTING,s__Process) &
   (s__instance(V__VOTING,s__VotingFn(V__ELECTION))
&
s__agent(V__VOTING,V__AGENT)))))))))
)
)

Government.kif 1162-1175
( ! [V__AGENT,V__POLITY,V__AGE,V__VOTINGAGE,V__ELECTION] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__POLITY,s__Nation) &
         s__instance(V__AGE,s__RealNumber) &
         s__instance(V__VOTINGAGE,s__RealNumber) &
         s__instance(V__ELECTION,s__Election))
       =>
       (((s__subProposition(s__UniversalSuffrageLaw,s__RegionalLawFn(V__POLITY))
         &
         s__citizen(V__AGENT,V__POLITY)
       &
       s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration))
     &
     s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration))
   &
   s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
&
s__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
=>
(s__capability(s__VotingFn(V__ELECTION)
,s__agent__m,V__AGENT)))))
)
)

Government.kif 1106-1116

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


( ! [V__NUMBER] :
   (((s__instance(V__NUMBER,s__NonnegativeRealNumber) =>
         (s__greaterThanOrEqualTo(V__NUMBER,n__0)
         &
         s__instance(V__NUMBER,s__RealNumber)))
     &
     ((s__greaterThanOrEqualTo(V__NUMBER,n__0)
       &
       s__instance(V__NUMBER,s__RealNumber))
     =>
     s__instance(V__NUMBER,s__NonnegativeRealNumber)))
)
)

Merge.kif 1873-1877 A quantity is an instance of nonnegative real number if and only if the quantity is greater than or equal to 0 and the quantity is an instance of real number
( ! [V__FROM,V__TO,V__QUANTITY] :
   (((s__instance(V__FROM,s__ConstantQuantity) &
         s__instance(V__TO,s__ConstantQuantity) &
         s__instance(V__QUANTITY,s__Quantity))
       =>
       (((s__instance(V__QUANTITY,s__IntervalFn(V__FROM,V__TO))
         =>
         (s__greaterThanOrEqualTo(V__QUANTITY,V__FROM)
         &
         s__lessThanOrEqualTo(V__QUANTITY,V__TO)))
   &
   ((s__greaterThanOrEqualTo(V__QUANTITY,V__FROM)
     &
     s__lessThanOrEqualTo(V__QUANTITY,V__TO))
=>
s__instance(V__QUANTITY,s__IntervalFn(V__FROM,V__TO))))))
)
)

Merge.kif 6375-6379 A quantity is an instance of the interval from a constant quantity to another constant quantity if and only if the quantity is greater than or equal to the constant quantity and the quantity is less than or equal to the other constant quantity
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17776-17786
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17792-17802
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 17808-17818
No TPTP formula. May not be expressible in strict first order. Government.kif 1118-1138
( ! [V__NODE2,V__NODE1,V__NUMBER1,V__NUMBER2,V__PATH] :
   (((s__instance(V__NODE2,s__GraphNode) &
         s__instance(V__NODE1,s__GraphNode) &
         s__instance(V__NUMBER1,s__Number) &
         s__instance(V__NUMBER2,s__Number) &
         s__instance(V__PATH,s__GraphPath))
       =>
       ((((s__MinimalWeightedPathFn(V__NODE1,V__NODE2)
             = V__PATH)
           &
           (s__PathWeightFn(V__PATH)
           = V__NUMBER1))
       =>
       (( ! [V__PATH2] :
           ((s__instance(V__PATH2,s__GraphPath) =>
               (((s__instance(V__PATH2,s__GraphPathFn(V__NODE1,V__NODE2))
                 &
                 (s__PathWeightFn(V__PATH2)
                 = V__NUMBER2))
             =>
             (s__greaterThanOrEqualTo(V__NUMBER2,V__NUMBER1)))))))))))
)
)

Merge.kif 5789-5798
( ! [V__AIRPORT] :
   (((s__instance(V__AIRPORT,s__Airport) &
         s__attribute(V__AIRPORT,s__LongRunwayAirport))
       =>
       (( ? [V__RUNWAY, V__LENGTH] :
           ((s__instance(V__LENGTH,s__RealNumber) &
               (s__instance(V__RUNWAY,s__Runway) &
                 s__part(V__RUNWAY,V__AIRPORT)
               &
               s__length(V__RUNWAY,s__MeasureFn(V__LENGTH,s__Meter))
             &
             (s__greaterThanOrEqualTo(V__LENGTH,n__2438)
             |
             s__lessThanOrEqualTo(V__LENGTH,n__3047))))))))
)
)

Transportation.kif 1445-1457
( ! [V__AIRPORT] :
   (((s__instance(V__AIRPORT,s__Airport) &
         s__attribute(V__AIRPORT,s__MediumLengthRunwayAirport))
       =>
       (( ? [V__RUNWAY, V__LENGTH] :
           ((s__instance(V__LENGTH,s__RealNumber) &
               (s__instance(V__RUNWAY,s__Runway) &
                 s__part(V__RUNWAY,V__AIRPORT)
               &
               s__length(V__RUNWAY,s__MeasureFn(V__LENGTH,s__Meter))
             &
             (s__greaterThanOrEqualTo(V__LENGTH,n__1524)
             |
             s__lessThanOrEqualTo(V__LENGTH,n__2437))))))))
)
)

Transportation.kif 1426-1438
( ! [V__AIRPORT] :
   (((s__instance(V__AIRPORT,s__Airport) &
         s__attribute(V__AIRPORT,s__ShortRunwayAirport))
       =>
       (( ? [V__RUNWAY, V__LENGTH] :
           ((s__instance(V__LENGTH,s__RealNumber) &
               (s__instance(V__RUNWAY,s__Runway) &
                 s__part(V__RUNWAY,V__AIRPORT)
               &
               s__length(V__RUNWAY,s__MeasureFn(V__LENGTH,s__Meter))
             &
             (s__greaterThanOrEqualTo(V__LENGTH,n__914)
             |
             s__lessThanOrEqualTo(V__LENGTH,n__1523))))))))
)
)

Transportation.kif 1407-1419
( ! [V__WEATHER,V__FRACTION,V__AREA] :
   ((s__instance(V__FRACTION,s__NonnegativeRealNumber) =>
       (((s__instance(V__AREA,s__GeographicArea) &
             s__instance(V__WEATHER,s__PartlyCloudyWeather) &
             s__eventLocated(V__WEATHER,V__AREA)
           &
           s__cloudCoverFraction(V__AREA,V__FRACTION))
       =>
       ((s__greaterThanOrEqualTo(V__FRACTION,n__0_3)
         &
         s__lessThanOrEqualTo(V__FRACTION,n__0_7))))))
)
)

Weather.kif 917-925
( ! [V__WEATHER,V__AREA] :
   (((s__instance(V__AREA,s__GeographicArea) &
         s__instance(V__WEATHER,s__PartlyCloudyWeather) &
         s__eventLocated(V__WEATHER,V__AREA))
     =>
     (( ? [V__FRACTION] :
         ((s__instance(V__FRACTION,s__NonnegativeRealNumber) &
             (s__cloudCoverFraction(V__AREA,V__FRACTION)
             &
             s__greaterThanOrEqualTo(V__FRACTION,n__0_3)
           &
           s__lessThanOrEqualTo(V__FRACTION,n__0_7)))))))
)
)

Weather.kif 906-915
( ! [V__CITIZENRY,V__POPULATION,V__AREA] :
   (((s__instance(V__CITIZENRY,s__Integer) &
         s__instance(V__POPULATION,s__Integer))
       =>
       (((s__instance(V__AREA,s__GeopoliticalArea) &
             (V__CITIZENRY = s__CardinalityFn(s__CitizenryFn(V__AREA)))
         &
         (V__POPULATION = s__CardinalityFn(s__ResidentFn(V__AREA))))
   =>
   (s__greaterThanOrEqualTo(V__POPULATION,V__CITIZENRY)))))
)
)

Mid-level-ontology.kif 7690-7697
( ! [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__TemperateClimateZone) &
             s__subclass(V__MO,s__Month) &
             s__averageTemperatureForPeriod(V__AREA,V__MO,s__MeasureFn(V__TEMP,s__CelsiusDegree)))
         =>
         (s__greaterThanOrEqualTo(V__TEMP,n___3)))))
)
)

Geography.kif 1404-1410
( ! [V__Amount,V__Date,V__Balance,V__U,V__Account] :
   (((s__instance(V__Amount,s__RealNumber) &
         s__instance(V__Date,s__TimePoint) &
         s__instance(V__Date,s__Day) &
         s__instance(V__Balance,s__RealNumber))
       =>
       (((s__instance(V__Account,s__FinancialAccount) &
             s__minimumBalance(V__Account,s__OpeningAnAccount,s__MeasureFn(V__Balance,V__U))
         &
         s__instance(V__U,s__UnitOfCurrency))
       =>
       (( ? [V__Payment] :
           ((s__instance(V__Payment,s__FinancialTransaction) &
               (s__destination(V__Payment,s__CurrencyFn(V__Account))
             &
             s__transactionAmount(V__Payment,s__MeasureFn(V__Amount,V__U))
         &
         s__greaterThanOrEqualTo(V__Amount,V__Balance)
       &
       s__agreementEffectiveDate(V__Account,V__Date)
     &
     s__date(V__Payment,V__Date)))))))))
)
)

FinancialOntology.kif 646-659
No TPTP formula. May not be expressible in strict first order. Merge.kif 13200-13208
( ! [V__MBR,V__C,V__S,V__X,V__Sub] :
   (((s__instance(V__MBR,s__Object) &
         s__instance(V__X,s__Integer))
       =>
       (((s__instance(V__C,s__Crystal) &
             s__attribute(V__C,s__MonoCrystalline) &
             s__instance(V__Sub,s__Substance) &
             s__attribute(V__Sub,s__Solid) &
             s__attribute(V__Sub,s__PolyCrystalline) &
             s__instance(V__S,s__Substance) &
             s__surface(V__S,V__Sub)
           &
           ~(s__part(V__C,V__S)))
       =>
       (( ? [V__CLNT] :
           ((s__instance(V__CLNT,s__Collection) &
               s__memberCount(V__CLNT,V__X)
             &
             s__greaterThanOrEqualTo(V__X,n__4)
           &
           (s__member(V__MBR,V__CLNT)
           =>
           ((s__part(V__MBR,V__Sub)
             &
             s__meetsSpatially(V__C,V__MBR)))))))))))
)
)

Geography.kif 6672-6692
No TPTP formula. May not be expressible in strict first order. Cars.kif 2811-2830
( ! [V__AGENT,V__POLITY,V__AGE,V__ACT,V__ELECTION,V__VOTINGAGE] :
   (((s__instance(V__AGENT,s__Agent) &
         s__instance(V__POLITY,s__Agent) &
         s__instance(V__AGE,s__RealNumber) &
         s__instance(V__ACT,s__Process) &
         s__instance(V__ELECTION,s__Election) &
         s__instance(V__VOTINGAGE,s__RealNumber))
       =>
       (((s__instance(V__ELECTION,s__ElectionFn(V__POLITY))
         &
         s__instance(V__ACT,s__VotingFn(V__ELECTION))
     &
     s__agent(V__ACT,V__AGENT)
   &
   s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration))
&
s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration)))
=>
(s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)))))
)
)

Government.kif 989-998
( ! [V__AGENT,V__POLITY,V__ACT,V__ELECTION,V__VOTINGAGE] :
   (((s__instance(V__AGENT,s__Agent) &
         s__instance(V__POLITY,s__Agent) &
         s__instance(V__ACT,s__Process) &
         s__instance(V__ELECTION,s__Election) &
         s__instance(V__VOTINGAGE,s__RealNumber))
       =>
       (((s__instance(V__ELECTION,s__ElectionFn(V__POLITY))
         &
         s__instance(V__ACT,s__VotingFn(V__ELECTION))
     &
     s__agent(V__ACT,V__AGENT)
   &
   s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration)))
=>
(( ? [V__AGE] :
   ((s__instance(V__AGE,s__RealNumber) &
       (s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration))
       &
       s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)))))))))
)
)

Government.kif 976-987
( ! [V__NUMBER1,V__POSITION,V__PERSON1,V__ELECTION] :
   (((s__instance(V__NUMBER1,s__RealNumber) &
         s__instance(V__POSITION,s__SocialRole) &
         s__instance(V__PERSON1,s__Agent))
       =>
       (((s__instance(V__ELECTION,s__PopularElection) &
             s__electionWinner(V__ELECTION,V__POSITION,V__PERSON1)
           &
           s__voteFractionReceived(V__ELECTION,V__POSITION,V__PERSON1,V__NUMBER1))
       =>
       (~(( ? [V__PERSON2, V__NUMBER2] :
             ((s__instance(V__PERSON2,s__Agent) &
                 s__instance(V__NUMBER2,s__RealNumber) &
                 (s__voteFractionReceived(V__ELECTION,V__POSITION,V__PERSON2,V__NUMBER2)
                 &
                 ~((V__PERSON1 = V__PERSON2))
                 &
                 s__greaterThanOrEqualTo(V__NUMBER2,V__NUMBER1))))))))))
)
)

Government.kif 1868-1878
No TPTP formula. May not be expressible in strict first order. Weather.kif 2358-2377
( ! [V__Period,V__Loan,V__Duration] :
   (((s__instance(V__Period,s__TimeInterval) &
         s__instance(V__Duration,s__RealNumber))
       =>
       (((s__instance(V__Loan,s__BankTermLoan) &
             s__agreementPeriod(V__Loan,V__Period)
           &
           s__duration(V__Period,s__MeasureFn(V__Duration,s__YearDuration)))
       =>
       (s__greaterThanOrEqualTo(V__Duration,n__1)))))
)
)

FinancialOntology.kif 1451-1456
( ! [V__WIDTH,V__RR] :
   ((s__instance(V__WIDTH,s__RealNumber) =>
       (((s__instance(V__RR,s__Railway) &
             s__property(V__RR,s__StandardGauge) &
             s__trackWidth(V__RR,s__MeasureFn(V__WIDTH,s__Meter)))
         =>
         (s__greaterThanOrEqualTo(V__WIDTH,n__1_435)))))
)
)

Transportation.kif 427-433
( ! [V__SHIP,V__GRT] :
   ((s__instance(V__GRT,s__RealNumber) =>
       (((s__instance(V__SHIP,s__MerchantMarineShip) &
             s__measure(V__SHIP,s__MeasureFn(V__GRT,s__RegistryTon)))
         =>
         (s__greaterThanOrEqualTo(V__GRT,n__1000)))))
)
)

Transportation.kif 1029-1033

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


No TPTP formula. May not be expressible in strict first order. Government.kif 1078-1089 For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information universal suffrage law
No TPTP formula. May not be expressible in strict first order. Government.kif 1146-1160 For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE contains information compulsory suffrage law
No TPTP formula. May not be expressible in strict first order. Military.kif 867-876 The available for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string
No TPTP formula. May not be expressible in strict first order. Military.kif 890-901 The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string

appearance as argument number 0
-------------------------


s__greaterThanOrEqualTo(s__CardinalityFn(s__TwelveApostles),n__11)

Media.kif 1967-1967 The number of instances in TwelveApostles is greater than or equal to 11
( ! [V__NUMBER] :
   ((s__instance(V__NUMBER,s__RealNumber) =>
       (s__greaterThanOrEqualTo(s__MeasureFn(V__NUMBER,s__MonthDuration),s__MeasureFn(s__MultiplicationFn(V__NUMBER,n__28)
      ,s__DayDuration))))
)
)

Merge.kif 6912-6914 A real number month duration(s) is greater than or equal to the real number and 28 day duration(s)


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