greaterThanOrEqualTo


Sigma KEE  greaterThanOrEqualTo
appearance as argument number 1


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

Merge.kif 19501951 

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 19471949 

s__domain(s__greaterThanOrEqualTo__m,1,s__Quantity)

Merge.kif 19441944 
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 19451945 
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 19401940 
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 19411941 
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 19421942 
greater than or equal to is an instance of relation extended to quantities 
s__inverse(s__greaterThanOrEqualTo__m,s__lessThanOrEqualTo__m)

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

Merge.kif 19431943 
greater than or equal to is trichotomizing on real number 
appearance as argument number 2


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 68196829 
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 19531957 
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 20282035 

( ∀ [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 20372047 

( ∀ [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 20192026 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1383013843 

( ∀ [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 12881295 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 358364 

No TPTP formula. May not be expressible in strict first order. 
FinancialOntology.kif 19661984 

( ∀ [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 21182125 

( ∀ [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 21272139 

( ∀ [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 21092116 

( ∀ [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 20762083 

( ∀ [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 20852095 

( ∀ [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 20672074 

( ∀ [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 11431154 

( ∀ [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 10931101 

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 19982002 
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 67826786 
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. 
Midlevelontology.kif 1632516336 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1634216353 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1635916370 

No TPTP formula. May not be expressible in strict first order. 
Government.kif 11031121 

( ∀ [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 61436152 

( ∀ [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 14171428 

( ∀ [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 13991410 

( ∀ [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 13811392 

( ∀ [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 529537 

( ∀ [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 518527 

( ∀ [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)))
)

Midlevelontology.kif 77867791 

( ∀ [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 13811386 

( ∀ [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 646656 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1382013828 

( ∀ [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 64646484 

No TPTP formula. May not be expressible in strict first order. 
Cars.kif 27922811 

( ∀ [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 990997 

( ∀ [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 979988 

( ∀ [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 18421852 

( ∀ [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 14401445 

( ∀ [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 423428 

( ∀ [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 10031007 

( ∀ [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 36753686 

 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 10691078 
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 11291141 
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 867876 
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 890901 
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 
