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。')

Merge.kif 1950-1951
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 1947-1949
s__domain(s__greaterThanOrEqualTo__m,1,s__Quantity)

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

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

s__instance(s__greaterThanOrEqualTo__m,s__BinaryPredicate)

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

s__instance(s__PartialOrderingRelation,s__SetOrClass)

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

s__instance(s__greaterThanOrEqualTo__m,s__RelationExtendedToQuantities)

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

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

Merge.kif 1943-1943 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 83-83
s__termFormat(s__ChineseLanguage,s__greaterThanOrEqualTo__m,'大于或等于')

chinese_format.kif 114-114 "大于或等于" is the printable form of greater than or equal to in ChineseLanguage
s__termFormat(s__EnglishLanguage,s__greaterThanOrEqualTo__m,'greater than or equal to')

domainEnglishFormat.kif 4844-4844 "greater than or equal to" is the printable form of greater than or equal to in english language

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


( ! [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__greaterThanOrEqualTo(V__S,2.5))
s__<=>
(s__exists__m[V__PM25] :
   (s__instance(V__PM25,s__FineParticulateMatter)s__and__ms__part(V__PM25,V__PM)))))
)

Geography.kif 6819-6829 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__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__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__AMOUNT,s__ConstantQuantity)s__and__ms__instance(V__TOTAL,s__RealNumber)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__arableLandArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfArea)s__and__m(V__AMOUNTs__equal__ms__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))
s__=>s__arableLandArea(V__REGION,V__AMOUNT)))
)

Geography.kif 2028-2035
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__TOTAL,s__RealNumber)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__arableLandArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfArea))
s__=>(s__exists__m[V__ARABLE] :
(s__instance(V__ARABLE,s__ArableLand)s__and__ms__geographicSubregion(V__ARABLE,V__REGION)
s__and__ms__measure(V__ARABLE,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT))))))
)

Geography.kif 2037-2047
( ! [V__REGION,V__AMOUNT,V__FRACTION,V__TOTAL] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__AMOUNT,s__ConstantQuantity)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__arableLandArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,V__TOTAL)
  s__and__ms__instance(V__TOTAL,s__AreaMeasure)s__and__m(V__AMOUNTs__equal__ms__MultiplicationFn(V__FRACTION,V__TOTAL)))
s__=>s__arableLandArea(V__REGION,V__AMOUNT)))
)

Geography.kif 2019-2026
No TPTP formula. May not be expressible in strict first order. Merge.kif 13830-13843
( ! [V__AREA] :
   ((s__instance(V__AREA,s__TropicalClimateZone)s__and__m(s__forall__m[V__MO,V__AMOUNT] :
       ((s__instance(V__MO,s__Month)s__and__ms__instance(V__AMOUNT,s__LengthMeasure))
        s__=>(s__averageRainfallForPeriod(V__AREA,V__MO,V__AMOUNT)
        s__=>s__greaterThanOrEqualTo(V__AMOUNT,s__MeasureFn(60,s__MilliFn(s__Meter)))))))
s__=>s__instance(V__AREA,s__WetTropicalClimateZone))
)

Geography.kif 1288-1295
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 358-364
No TPTP formula. May not be expressible in strict first order. FinancialOntology.kif 1966-1984
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__AMOUNT,s__ConstantQuantity)s__and__ms__instance(V__TOTAL,s__RealNumber)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__otherLandUseArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfArea)s__and__m(V__AMOUNTs__equal__ms__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))
s__=>s__otherLandUseArea(V__REGION,V__AMOUNT)))
)

Geography.kif 2118-2125
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__TOTAL,s__RealNumber)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__otherLandUseArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfArea))
s__=>(s__exists__m[V__OTHER] :
(s__instance(V__OTHER,s__LandArea)s__and__m(s__not__ms__instance(V__OTHER,s__ArableLand))
s__and__m(s__not__ms__instance(V__OTHER,s__PermanentCropLand))
s__and__ms__geographicSubregion(V__OTHER,V__REGION)
s__and__ms__measure(V__OTHER,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT))))))
)

Geography.kif 2127-2139
( ! [V__REGION,V__AMOUNT,V__FRACTION,V__TOTAL] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__AMOUNT,s__ConstantQuantity)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__otherLandUseArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,V__TOTAL)
  s__and__ms__instance(V__TOTAL,s__AreaMeasure)s__and__m(V__AMOUNTs__equal__ms__MultiplicationFn(V__FRACTION,V__TOTAL)))
s__=>s__otherLandUseArea(V__REGION,V__AMOUNT)))
)

Geography.kif 2109-2116
( ! [V__REGION,V__AMOUNT,V__TOTAL,V__FRACTION,V__UNIT] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__AMOUNT,s__ConstantQuantity)s__and__ms__instance(V__TOTAL,s__RealNumber)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__permanentCropLandArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfArea)s__and__m(V__AMOUNTs__equal__ms__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT)))
s__=>s__permanentCropLandArea(V__REGION,V__AMOUNT)))
)

Geography.kif 2076-2083
( ! [V__REGION,V__TOTAL,V__FRACTION,V__UNIT] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__TOTAL,s__RealNumber)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__permanentCropLandArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,s__MeasureFn(V__TOTAL,V__UNIT))
s__and__ms__instance(V__UNIT,s__UnitOfArea))
s__=>(s__exists__m[V__PERMCROP] :
(s__instance(V__PERMCROP,s__PermanentCropLand)s__and__ms__geographicSubregion(V__PERMCROP,V__REGION)
s__and__ms__measure(V__PERMCROP,s__MeasureFn(s__MultiplicationFn(V__FRACTION,V__TOTAL)
,V__UNIT))))))
)

Geography.kif 2085-2095
( ! [V__REGION,V__AMOUNT,V__FRACTION,V__TOTAL] :
   ((s__instance(V__REGION,s__GeographicArea)s__and__ms__instance(V__AMOUNT,s__ConstantQuantity)s__and__ms__instance(V__FRACTION,s__ConstantQuantity))
    s__=>((s__permanentCropLandArea(V__REGION,V__FRACTION)
      s__and__ms__greaterThanOrEqualTo(V__FRACTION,0)
    s__and__ms__totalArea(V__REGION,V__TOTAL)
  s__and__ms__instance(V__TOTAL,s__AreaMeasure)s__and__m(V__AMOUNTs__equal__ms__MultiplicationFn(V__FRACTION,V__TOTAL)))
s__=>s__permanentCropLandArea(V__REGION,V__AMOUNT)))
)

Geography.kif 2067-2074
( ! [V__AGENT,V__POLITY,V__AGE,V__VOTINGAGE,V__ELECTION] :
   ((s__instance(V__AGENT,s__Human)s__and__ms__instance(V__POLITY,s__Nation)s__and__ms__instance(V__AGE,s__TimeDuration)s__and__ms__instance(V__VOTINGAGE,s__TimeDuration)s__and__ms__instance(V__ELECTION,s__Election))
    s__=>((s__subProposition(s__CompulsorySuffrageLaw,s__RegionalLawFn(V__POLITY))
    s__and__ms__citizen(V__AGENT,V__POLITY)
  s__and__ms__suffrageAgeMinimum(V__POLITY,V__VOTINGAGE)
s__and__ms__age(V__AGENT,V__AGE)
s__and__ms__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
s__and__ms__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
s__=>(s__exists__m[V__VOTING] :
(s__instance(V__VOTING,s__Process)s__and__m(s__instance(V__VOTING,s__VotingFn(V__ELECTION))
s__and__ms__agent(V__VOTING,V__AGENT))))))
)

Government.kif 1143-1154
( ! [V__AGENT,V__POLITY,V__AGE,V__VOTINGAGE,V__ELECTION] :
   ((s__instance(V__AGENT,s__Human)s__and__ms__instance(V__POLITY,s__Nation)s__and__ms__instance(V__AGE,s__TimeDuration)s__and__ms__instance(V__VOTINGAGE,s__TimeDuration)s__and__ms__instance(V__ELECTION,s__Election))
    s__=>((s__subProposition(s__UniversalSuffrageLaw,s__RegionalLawFn(V__POLITY))
    s__and__ms__citizen(V__AGENT,V__POLITY)
  s__and__ms__suffrageAgeMinimum(V__POLITY,V__VOTINGAGE)
s__and__ms__age(V__AGENT,V__AGE)
s__and__ms__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
s__and__ms__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
s__=>s__capability(s__VotingFn(V__ELECTION)
,s__agent__m,V__AGENT)))
)

Government.kif 1093-1101

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


( ! [V__NUMBER] :
   (s__instance(V__NUMBER,s__NonnegativeRealNumber)s__<=>
    (s__greaterThanOrEqualTo(V__NUMBER,0)
    s__and__ms__instance(V__NUMBER,s__RealNumber)))
)

Merge.kif 1998-2002 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__and__ms__instance(V__TO,s__ConstantQuantity)s__and__ms__instance(V__QUANTITY,s__Quantity))
    s__=>(s__instance(V__QUANTITY,s__IntervalFn(V__FROM,V__TO))
  s__<=>
  (s__greaterThanOrEqualTo(V__QUANTITY,V__FROM)
  s__and__ms__lessThanOrEqualTo(V__QUANTITY,V__TO))))
)

Merge.kif 6782-6786 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 16325-16336
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16342-16353
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 16359-16370
No TPTP formula. May not be expressible in strict first order. Government.kif 1103-1121
( ! [V__NODE2,V__NODE1,V__NUMBER1,V__NUMBER2,V__PATH] :
   ((s__instance(V__NODE2,s__GraphNode)s__and__ms__instance(V__NODE1,s__GraphNode)s__and__ms__instance(V__NUMBER1,s__Quantity)s__and__ms__instance(V__NUMBER2,s__Quantity)s__and__ms__instance(V__PATH,s__GraphPath))
    s__=>(((s__MinimalWeightedPathFn(V__NODE1,V__NODE2)
        s__equal__mV__PATH)s__and__m(s__PathWeightFn(V__PATH)
      s__equal__mV__NUMBER1))
    s__=>(s__forall__m[V__PATH2] :
       (s__instance(V__PATH2,s__GraphPath)s__=>((s__instance(V__PATH2,s__GraphPathFn(V__NODE1,V__NODE2))
        s__and__m(s__PathWeightFn(V__PATH2)
      s__equal__mV__NUMBER2))
    s__=>s__greaterThanOrEqualTo(V__NUMBER2,V__NUMBER1))))))
)

Merge.kif 6143-6152
( ! [V__AIRPORT] :
   ((s__instance(V__AIRPORT,s__Airport)s__and__ms__attribute(V__AIRPORT,s__LongRunwayAirport))
    s__=>(s__exists__m[V__RUNWAY,V__LENGTH] :
       (s__instance(V__LENGTH,s__Quantity)s__and__m(s__instance(V__RUNWAY,s__Runway)s__and__ms__part(V__RUNWAY,V__AIRPORT)
      s__and__ms__length(V__RUNWAY,V__LENGTH)
    s__and__m(s__greaterThanOrEqualTo(V__LENGTH,s__MeasureFn(2438,s__Meter))
  s__or__ms__lessThanOrEqualTo(V__LENGTH,s__MeasureFn(3047,s__Meter)))))))
)

Transportation.kif 1417-1428
( ! [V__AIRPORT] :
   ((s__instance(V__AIRPORT,s__Airport)s__and__ms__attribute(V__AIRPORT,s__MediumLengthRunwayAirport))
    s__=>(s__exists__m[V__RUNWAY,V__LENGTH] :
       (s__instance(V__LENGTH,s__Quantity)s__and__m(s__instance(V__RUNWAY,s__Runway)s__and__ms__part(V__RUNWAY,V__AIRPORT)
      s__and__ms__length(V__RUNWAY,V__LENGTH)
    s__and__m(s__greaterThanOrEqualTo(V__LENGTH,s__MeasureFn(1524,s__Meter))
  s__or__ms__lessThanOrEqualTo(V__LENGTH,s__MeasureFn(2437,s__Meter)))))))
)

Transportation.kif 1399-1410
( ! [V__AIRPORT] :
   ((s__instance(V__AIRPORT,s__Airport)s__and__ms__attribute(V__AIRPORT,s__ShortRunwayAirport))
    s__=>(s__exists__m[V__RUNWAY,V__LENGTH] :
       (s__instance(V__LENGTH,s__Quantity)s__and__m(s__instance(V__RUNWAY,s__Runway)s__and__ms__part(V__RUNWAY,V__AIRPORT)
      s__and__ms__length(V__RUNWAY,V__LENGTH)
    s__and__m(s__greaterThanOrEqualTo(V__LENGTH,s__MeasureFn(914,s__Meter))
  s__or__ms__lessThanOrEqualTo(V__LENGTH,s__MeasureFn(1523,s__Meter)))))))
)

Transportation.kif 1381-1392
( ! [V__FRACTION,V__AREA,V__WEATHER] :
   (s__instance(V__FRACTION,s__NonnegativeRealNumber)s__=>((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__WEATHER,s__PartlyCloudyWeather)s__and__ms__eventLocated(V__WEATHER,V__AREA)
      s__and__ms__cloudCoverFraction(V__AREA,V__FRACTION))
  s__=>(s__greaterThanOrEqualTo(V__FRACTION,0.3)
  s__and__ms__lessThanOrEqualTo(V__FRACTION,0.7))))
)

Weather.kif 529-537
( ! [V__AREA,V__WEATHER] :
   ((s__instance(V__AREA,s__GeographicArea)s__and__ms__instance(V__WEATHER,s__PartlyCloudyWeather)s__and__ms__eventLocated(V__WEATHER,V__AREA))
  s__=>(s__exists__m[V__FRACTION] :
     (s__instance(V__FRACTION,s__NonnegativeRealNumber)s__and__m(s__cloudCoverFraction(V__AREA,V__FRACTION)
    s__and__ms__greaterThanOrEqualTo(V__FRACTION,0.3)
  s__and__ms__lessThanOrEqualTo(V__FRACTION,0.7)))))
)

Weather.kif 518-527
( ! [V__CITIZENRY,V__POPULATION,V__AREA] :
   ((s__instance(V__CITIZENRY,s__GroupOfPeople)s__and__ms__instance(V__CITIZENRY,s__Quantity)s__and__ms__instance(V__POPULATION,s__GroupOfPeople)s__and__ms__instance(V__POPULATION,s__Quantity))
    s__=>((s__instance(V__AREA,s__GeopoliticalArea)s__and__m(V__CITIZENRYs__equal__ms__CitizenryFn(V__AREA))
    s__and__m(V__POPULATIONs__equal__ms__ResidentFn(V__AREA)))
s__=>s__greaterThanOrEqualTo(V__POPULATION,V__CITIZENRY)))
)

Mid-level-ontology.kif 7786-7791
( ! [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__TemperateClimateZone)s__and__ms__subclass(V__MO,s__Month)s__and__ms__averageTemperatureForPeriod(V__AREA,V__MO,V__TEMP))
    s__=>s__greaterThanOrEqualTo(V__TEMP,s__MeasureFn(-3,s__CelsiusDegree))))
)

Geography.kif 1381-1386
( ! [V__Amount,V__Date,V__Balance,V__Account,V__FinancialAccount] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Date,s__TimePoint)s__and__ms__instance(V__Date,s__Day)s__and__ms__instance(V__Balance,s__CurrencyMeasure)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__FinancialAccount,s__SetOrClass))
    s__=>((s__instance(V__Account,V__FinancialAccount)
      s__and__ms__minimumBalance(V__Account,s__OpeningAnAccount,V__Balance))
  s__=>(s__exists__m[V__Payment] :
     (s__instance(V__Payment,s__FinancialTransaction)s__and__m(s__destination(V__Payment,s__CurrencyFn(V__Account))
  s__and__ms__transactionAmount(V__Payment,V__Amount)
s__and__ms__greaterThanOrEqualTo(V__Amount,V__Balance)
s__and__ms__agreementEffectiveDate(V__Account,V__Date)
s__and__ms__date(V__Payment,V__Date))))))
)

FinancialOntology.kif 646-656
No TPTP formula. May not be expressible in strict first order. Merge.kif 13820-13828
( ! [V__MBR,V__X,V__C,V__Sub,V__S] :
   ((s__instance(V__MBR,s__Object)s__and__ms__instance(V__X,s__Integer))
    s__=>((s__instance(V__C,s__Crystal)s__and__ms__attribute(V__C,s__MonoCrystalline)s__and__ms__instance(V__Sub,s__Substance)s__and__ms__attribute(V__Sub,s__Solid)s__and__ms__attribute(V__Sub,s__PolyCrystalline)s__and__ms__instance(V__S,s__Substance)s__and__ms__surface(V__S,V__Sub)
      s__and__m(s__not__ms__part(V__C,V__S)))
s__=>(s__exists__m[V__CLNT] :
   (s__instance(V__CLNT,s__Collection)s__and__ms__memberCount(V__CLNT,V__X)
  s__and__ms__greaterThanOrEqualTo(V__X,4)
s__and__m(s__member(V__MBR,V__CLNT)
s__=>(s__part(V__MBR,V__Sub)
s__and__ms__meetsSpatially(V__C,V__MBR)))))))
)

Geography.kif 6464-6484
No TPTP formula. May not be expressible in strict first order. Cars.kif 2792-2811
( ! [V__AGENT,V__POLITY,V__AGE,V__ACT,V__ELECTION,V__VOTINGAGE] :
   ((s__instance(V__AGENT,s__Agent)s__and__ms__instance(V__POLITY,s__Agent)s__and__ms__instance(V__AGE,s__TimeDuration)s__and__ms__instance(V__ACT,s__Process)s__and__ms__instance(V__ELECTION,s__Election)s__and__ms__instance(V__VOTINGAGE,s__TimeDuration))
    s__=>((s__instance(V__ELECTION,s__ElectionFn(V__POLITY))
    s__and__ms__instance(V__ACT,s__VotingFn(V__ELECTION))
s__and__ms__agent(V__ACT,V__AGENT)
s__and__ms__suffrageAgeMinimum(V__POLITY,V__VOTINGAGE)
s__and__ms__age(V__AGENT,V__AGE))
s__=>s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)))
)

Government.kif 990-997
( ! [V__AGENT,V__POLITY,V__ACT,V__ELECTION,V__VOTINGAGE] :
   ((s__instance(V__AGENT,s__Agent)s__and__ms__instance(V__POLITY,s__Agent)s__and__ms__instance(V__ACT,s__Process)s__and__ms__instance(V__ELECTION,s__Election)s__and__ms__instance(V__VOTINGAGE,s__TimeDuration))
    s__=>((s__instance(V__ELECTION,s__ElectionFn(V__POLITY))
    s__and__ms__instance(V__ACT,s__VotingFn(V__ELECTION))
s__and__ms__agent(V__ACT,V__AGENT)
s__and__ms__suffrageAgeMinimum(V__POLITY,V__VOTINGAGE))
s__=>(s__exists__m[V__AGE] :
(s__instance(V__AGE,s__TimeDuration)s__and__m(s__age(V__AGENT,V__AGE)
s__and__ms__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE))))))
)

Government.kif 979-988
( ! [V__NUMBER1,V__POSITION,V__PERSON1,V__ELECTION] :
   ((s__instance(V__NUMBER1,s__RealNumber)s__and__ms__instance(V__POSITION,s__SocialRole)s__and__ms__instance(V__PERSON1,s__Agent))
    s__=>((s__instance(V__ELECTION,s__PopularElection)s__and__ms__electionWinner(V__ELECTION,V__POSITION,V__PERSON1)
      s__and__ms__voteFractionReceived(V__ELECTION,V__POSITION,V__PERSON1,V__NUMBER1))
  s__=>(s__not__m(s__exists__m[V__PERSON2,V__NUMBER2] :
     (s__instance(V__PERSON2,s__Agent)s__and__ms__instance(V__NUMBER2,s__RealNumber)s__and__m(s__voteFractionReceived(V__ELECTION,V__POSITION,V__PERSON2,V__NUMBER2)
    s__and__m(s__not__m(V__PERSON1s__equal__mV__PERSON2))
  s__and__ms__greaterThanOrEqualTo(V__NUMBER2,V__NUMBER1)))))))
)

Government.kif 1842-1852
( ! [V__Period,V__Duration,V__Loan] :
   ((s__instance(V__Period,s__TimeInterval)s__and__ms__instance(V__Duration,s__RealNumber))
    s__=>((s__instance(V__Loan,s__BankTermLoan)s__and__ms__agreementPeriod(V__Loan,V__Period)
      s__and__ms__duration(V__Period,s__MeasureFn(V__Duration,s__YearDuration)))
  s__=>s__greaterThanOrEqualTo(V__Duration,1)))
)

FinancialOntology.kif 1440-1445
( ! [V__WIDTH,V__RR] :
   (s__instance(V__WIDTH,s__LengthMeasure)s__=>((s__instance(V__RR,s__Railway)s__and__ms__property(V__RR,s__StandardGauge)s__and__ms__trackWidth(V__RR,V__WIDTH))
    s__=>s__greaterThanOrEqualTo(V__WIDTH,s__MeasureFn(1.435,s__Meter))))
)

Transportation.kif 423-428
( ! [V__GRT,V__SHIP] :
   (s__instance(V__GRT,s__RealNumber)s__=>((s__instance(V__SHIP,s__MerchantMarineShip)s__and__ms__measure(V__SHIP,s__MeasureFn(V__GRT,s__RegistryTon)))
    s__=>s__greaterThanOrEqualTo(V__GRT,1000)))
)

Transportation.kif 1003-1007
( ! [V__Amount,V__Day,V__Account,V__Amount1,V__Transaction,V__Cash] :
   ((s__instance(V__Amount,s__CurrencyMeasure)s__and__ms__instance(V__Day,s__Day)s__and__ms__instance(V__Account,s__FinancialAccount)s__and__ms__instance(V__Amount1,s__Quantity))
    s__=>((s__instance(V__Transaction,s__FinancialTransaction)s__and__ms__origin(V__Transaction,s__CurrencyFn(V__Account))
    s__and__ms__transactionAmount(V__Transaction,V__Amount)
  s__and__ms__instance(V__Cash,s__Currency)s__and__ms__patient(V__Transaction,V__Cash)
s__and__ms__date(V__Transaction,V__Day))
s__=>(s__exists__m[V__Amount2] :
(s__instance(V__Amount2,s__CurrencyMeasure)s__and__m(s__availableCash(V__Account,V__Day,V__Amount2)
s__and__ms__greaterThanOrEqualTo(V__Amount1,V__Amount2))))))
)

FinancialOntology.kif 3675-3686

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 1069-1078 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 1129-1141 For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
  • if ?VOTER is a citizen of ?POLITY and ?VOTINGAGE is a suffrage age minimum of ?POLITY and the age of ?VOTER is ?AGE and ?AGE is greater than or equal to ?VOTINGAGE and ?ELECTION is an instance of the election of ?POLITY,
  • then there exists ?VOTING such that ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING
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),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__=>s__greaterThanOrEqualTo(s__MeasureFn(V__NUMBER,s__MonthDuration),s__MeasureFn(s__MultiplicationFn(V__NUMBER,28)
  ,s__DayDuration)))
)

Merge.kif 7392-7394 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 2.99c (>= 2017/11/20) is open source software produced by Articulate Software and its partners