( ! [V__AMOUNT,V__UNIT] :
(((s__instance(V__AMOUNT,s__Number) &
s__instance(V__AMOUNT,s__PhysicalQuantity))
=>
((((s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))
=>
(V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT))))
&
((V__AMOUNT = s__MultiplicationFn(s__MeasureFn(n__1,V__UNIT)
,s__MeasureFn(n__1,V__UNIT)))
=>
(s__instance(V__UNIT,s__UnitOfMeasure) &
(V__AMOUNT = s__MeasureFn(n__1,s__SquareUnitFn(V__UNIT))))))))
)
)
|
Geography.kif 3804-3808 |
An unit of measure is an instance of unit of measure and a number is equal to 1 the square unit of the unit of measure(s) if and only if the number is equal to 1 the unit of measure(s) and 1 the unit of measure(s) |
( ! [V__NUMBER1,V__NUMBER2,V__NUMBER] :
(((s__instance(V__NUMBER1,s__Integer) &
s__instance(V__NUMBER2,s__Integer) &
s__instance(V__NUMBER,s__Integer))
=>
((((s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)
=>
(s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1))
&
((s__AdditionFn(s__MultiplicationFn(s__FloorFn(s__DivisionFn(V__NUMBER1,V__NUMBER2))
,V__NUMBER2)
,V__NUMBER)
= V__NUMBER1)
=>
(s__RemainderFn(V__NUMBER1,V__NUMBER2)
= V__NUMBER)))))
)
)
|
Merge.kif 4941-4943 |
An integer mod another integer is equal to a third integer if and only if (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer |
( ! [V__O,V__A] :
(((s__instance(V__O,s__Physical) &
s__instance(V__A,s__RealNumber))
=>
(((s__measure(V__O,s__MeasureFn(V__A,s__MetricTon))
=>
s__measure(V__O,s__MeasureFn(s__MultiplicationFn(V__A,n__2205)
,s__PoundMass)))
&
(s__measure(V__O,s__MeasureFn(s__MultiplicationFn(V__A,n__2205)
,s__PoundMass))
=>
s__measure(V__O,s__MeasureFn(V__A,s__MetricTon))))))
)
)
|
Mid-level-ontology.kif 12807-12813 |
The measure of a physical is a real number metric ton(s) if and only if the measure of the physical is the real number and 2205 pound mass(s) |
( ! [V__OBJ,V__DEG] :
(((s__instance(V__OBJ,s__Physical) &
s__instance(V__DEG,s__RealNumber))
=>
(((s__measure(V__OBJ,s__MeasureFn(V__DEG,s__AngularDegree))
=>
s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
,s__ArcMinute)))
&
(s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
,s__ArcMinute))
=>
s__measure(V__OBJ,s__MeasureFn(V__DEG,s__AngularDegree))))))
)
)
|
Geography.kif 378-380 |
The measure of a physical is a real number angular degree(s) if and only if the measure of the physical is 60 and the real number arc minute(s) |
( ! [V__OBJ,V__DEG] :
(((s__instance(V__OBJ,s__Physical) &
s__instance(V__DEG,s__RealNumber))
=>
(((s__measure(V__OBJ,s__MeasureFn(V__DEG,s__ArcMinute))
=>
s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
,s__ArcSecond)))
&
(s__measure(V__OBJ,s__MeasureFn(s__MultiplicationFn(n__60,V__DEG)
,s__ArcSecond))
=>
s__measure(V__OBJ,s__MeasureFn(V__DEG,s__ArcMinute))))))
)
)
|
Geography.kif 397-399 |
The measure of a physical is a real number arc minute(s) if and only if the measure of the physical is 60 and the real number arc second(s) |
( ! [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 |
|
| No TPTP formula. May not be expressible in strict first order. |
ArabicCulture.kif 193-212 |
|
| No TPTP formula. May not be expressible in strict first order. |
Geography.kif 658-668 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 12768-12777 |
|
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 12779-12788 |
|
( ! [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))
&
(n__1 = s__ListLengthFn(V__L)))
=>
((V__VA = s__MultiplicationFn(s__SubtractionFn(V__M,s__ListOrderFn(V__L,n__1))
,s__SubtractionFn(V__M,s__ListOrderFn(V__L,n__1))))))))
)
)
|
Weather.kif 1485-1496 |
|
( ! [V__NUMBER] :
(((s__instance(V__NUMBER,s__Integer) &
~((V__NUMBER = n__0)))
=>
((n__1 = s__MultiplicationFn(V__NUMBER,s__ReciprocalFn(V__NUMBER)))))
)
)
|
Merge.kif 4923-4928 |
|
| No TPTP formula. May not be expressible in strict first order. |
Cars.kif 3095-3109 |
|
( ! [V__WH,V__SWH,V__WW] :
(((s__instance(V__WH,s__LengthMeasure) &
s__instance(V__SWH,s__RealNumber))
=>
(((s__instance(V__WW,s__WaterWave) &
s__waveHeight(V__WW,V__WH))
=>
(( ? [V__LIST, V__WA, V__U] :
((s__instance(V__LIST,s__List) &
(s__inList(V__WH,V__LIST)
&
s__instance(V__WA,s__WaterArea) &
s__eventLocated(V__WW,V__WA)
&
s__instance(V__U,s__LengthMeasure) &
s__significantWaveHeight(V__WA,s__WhenFn(V__WW)
,s__MeasureFn(V__SWH,V__U))
&
(V__SWH = s__MultiplicationFn(n__4,s__StandardDeviationFn(V__LIST)))))))))))
)
)
|
Weather.kif 1531-1546 |
|
( ! [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__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 |
|
| No TPTP formula. May not be expressible in strict first order. |
FinancialOntology.kif 2200-2210 |
|
( ! [V__N1,V__Time,V__N2,V__N3,V__TimeOfSplit,V__NewNumber,V__Stocks,V__TimeAfterSplit,V__Number] :
(((s__instance(V__N1,s__Integer) &
s__instance(V__Time,s__Agent) &
s__instance(V__Time,s__TimeInterval) &
s__instance(V__N2,s__Integer) &
s__instance(V__N3,s__Number) &
s__instance(V__TimeOfSplit,s__TimeInterval) &
s__instance(V__NewNumber,s__RealNumber) &
s__instance(V__Stocks,s__Physical) &
s__instance(V__TimeAfterSplit,s__Agent) &
s__instance(V__TimeAfterSplit,s__TimeInterval) &
s__instance(V__Number,s__RealNumber))
=>
(((s__price(V__Stocks,s__MeasureFn(V__Number,s__UnitedStatesDollar),V__Time)
&
( ? [V__Event] :
((s__instance(V__Event,s__StockSplit) &
(s__splitFor(V__Event,V__N1,V__N2)
&
(s__WhenFn(V__Event)
= V__TimeOfSplit))))))
=>
(((V__N3 = s__MultiplicationFn(V__Number,V__N1))
&
(V__NewNumber = s__DivisionFn(V__N3,V__N2))
&
s__price(V__Stocks,s__MeasureFn(V__NewNumber,s__UnitedStatesDollar),V__TimeAfterSplit)
&
s__meetsTemporally(V__Time,V__TimeOfSplit)
&
s__meetsTemporally(V__TimeOfSplit,V__TimeAfterSplit))))))
)
)
|
FinancialOntology.kif 2212-2224 |
|
( ! [V__Amount,V__Period,V__Rate,V__Balance,V__Account,V__Rate_Decimal] :
(((s__instance(V__Amount,s__Interest) &
s__instance(V__Amount,s__Number) &
s__instance(V__Period,s__TimeInterval) &
s__instance(V__Rate,s__Number) &
s__instance(V__Rate,s__PhysicalQuantity) &
s__instance(V__Balance,s__Number) &
s__instance(V__Balance,s__CurrencyMeasure) &
s__instance(V__Account,s__FinancialAccount) &
s__instance(V__Rate_Decimal,s__Number))
=>
(((s__principalAmount(V__Account,V__Balance)
&
s__fixedInterestRate(V__Account,V__Rate)
&
s__simpleInterest(V__Account,V__Amount,V__Period)
&
(V__Rate_Decimal = s__DivisionFn(s__MagnitudeFn(V__Rate)
,n__100)))
=>
((V__Amount = s__MultiplicationFn(s__MultiplicationFn(s__MagnitudeFn(V__Period)
,V__Balance)
,V__Rate_Decimal))))))
)
)
|
FinancialOntology.kif 514-520 |
|
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17186-17212 |
|
( ! [V__U,V__F,V__H1,V__H2,V__S1,V__HF,V__S2] :
(((s__instance(V__U,s__UnitOfMeasure) &
s__instance(V__F,s__SelfConnectedObject) &
s__instance(V__H1,s__RealNumber) &
s__instance(V__H2,s__RealNumber) &
s__instance(V__S1,s__SelfConnectedObject) &
s__instance(V__HF,s__RealNumber) &
s__instance(V__S2,s__SelfConnectedObject))
=>
((s__attribute(V__F,s__Flat) =>
((s__side(V__S1,V__F)
&
s__side(V__S2,V__F)
&
s__meetsSpatially(V__S1,V__S2)
&
~((V__S1 = V__S2))
&
s__height(V__F,s__MeasureFn(V__HF,V__U))
&
s__height(V__S1,s__MeasureFn(V__H1,V__U))
&
s__height(V__S2,s__MeasureFn(V__H2,V__U))
&
s__greaterThan(V__H1,s__MultiplicationFn(n__2,V__HF))
&
s__greaterThan(V__H2,s__MultiplicationFn(n__2,V__HF)))))))
)
)
|
Mid-level-ontology.kif 2720-2731 |
|
( ! [V__U,V__F,V__H1,V__H2,V__S1,V__HF,V__S2] :
(((s__instance(V__U,s__UnitOfMeasure) &
s__instance(V__F,s__SelfConnectedObject) &
s__instance(V__H1,s__RealNumber) &
s__instance(V__H2,s__RealNumber) &
s__instance(V__S1,s__SelfConnectedObject) &
s__instance(V__HF,s__RealNumber) &
s__instance(V__S2,s__SelfConnectedObject))
=>
((s__attribute(V__F,s__LongAndThin) =>
((s__side(V__S1,V__F)
&
s__side(V__S2,V__F)
&
s__meetsSpatially(V__S1,V__S2)
&
~((V__S1 = V__S2))
&
s__length(V__F,s__MeasureFn(V__HF,V__U))
&
s__length(V__S1,s__MeasureFn(V__H1,V__U))
&
s__length(V__S2,s__MeasureFn(V__H2,V__U))
&
s__lessThan(V__H1,s__MultiplicationFn(n__3,V__HF))
&
s__lessThan(V__H2,s__MultiplicationFn(n__3,V__HF)))))))
)
)
|
Mid-level-ontology.kif 2739-2750 |
|
( ! [V__CIRCLE,V__LENGTH] :
(((s__instance(V__CIRCLE,s__Circle) &
s__instance(V__LENGTH,s__LengthMeasure))
=>
((s__circumfrence(V__CIRCLE,V__LENGTH)
=>
(( ? [V__D, V__UNIT] :
((s__instance(V__D,s__RealNumber) &
s__instance(V__UNIT,s__UnitOfMeasure) &
(s__diameter(V__CIRCLE,s__MeasureFn(V__D,V__UNIT))
&
(s__MeasureFn(s__MultiplicationFn(V__D,n__3_14)
,V__UNIT)
= V__LENGTH)))))))))
)
)
|
Mid-level-ontology.kif 30183-30191 |
|
( ! [V__CIRCLE,V__LENGTH] :
(((s__instance(V__CIRCLE,s__Circle) &
s__instance(V__LENGTH,s__LengthMeasure))
=>
((s__diameter(V__CIRCLE,V__LENGTH)
=>
(( ? [V__NHALF, V__UHALF] :
((s__instance(V__NHALF,s__RealNumber) &
s__instance(V__UHALF,s__UnitOfMeasure) &
(s__radius(V__CIRCLE,s__MeasureFn(V__NHALF,V__UHALF))
&
(s__MeasureFn(s__MultiplicationFn(V__NHALF,n__2)
,V__UHALF)
= V__LENGTH)))))))))
)
)
|
Merge.kif 7447-7452 |
|
( ! [V__C,V__U,V__L] :
(((s__instance(V__C,s__Circle) &
s__instance(V__U,s__UnitOfMeasure) &
s__instance(V__L,s__RealNumber))
=>
(((s__DiameterFn(V__C)
= s__MeasureFn(V__L,V__U))
=>
(( ? [V__R] :
((s__instance(V__R,s__RealNumber) &
((s__RadiusFn(V__C)
= s__MeasureFn(V__R,V__U))
&
(s__MultiplicationFn(V__R,n__2)
= V__L)))))))))
)
)
|
Mid-level-ontology.kif 4651-4656 |
|
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
