(=>
(and
(equal ?A
(AverageFn ?L))
(greaterThan
(ListLengthFn ?L) 0))
(equal ?A
(DivisionFn
(ListSumFn ?L)
(ListLengthFn ?L)))) |
Merge.kif 3388-3395 |
If equal X and the average of the numbers in Y and length of Y is greater than 0, then equal X, the sum of Y, and length of Y |
(=>
(and
(equal
(RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
(not
(equal ?NUMBER2 0)))
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5216-5227 |
If equal X mod Y and Z and equal Y and 0, then equal (the largest integer less than or equal to X and Y and Y and Z) and X |
(=>
(instance ?DEGREE RealNumber)
(equal
(TangentFn ?DEGREE)
(DivisionFn
(SineFn ?DEGREE)
(CosineFn ?DEGREE)))) |
Merge.kif 5362-5368 |
If X is an instance of real number, then equal the tangent of X, the sine of X, and the cosine of X |
(=>
(and
(relativeAngle ?O1 ?O2 ?N)
(physicalEnd ?E1 ?O1)
(physicalEnd ?E2 ?O1)
(not
(equal ?E1 ?E2))
(length ?O1
(MeasureFn ?N1 ?U))
(length ?O2
(MeasureFn ?N2 ?U))
(distance ?E1 ?E3
(MeasureFn ?N3 ?U))
(physicalEnd ?E3 ?O2)
(physicalEnd ?E4 ?O2)
(not
(equal ?E3 ?E4))
(not
(meetsSpatially ?E1 ?E3)))
(equal ?N
(ArcCosineFn
(DivisionFn
(SubtractionFn
(SubtractionFn
(MultiplicationFn ?N3 ?N3)
(MultiplicationFn ?N1 ?N1))
(MultiplicationFn ?N2 ?N2))
(MultiplicationFn 2.0
(MultiplicationFn ?N1 ?N2)))))) |
Merge.kif 18247-18272 |
If All of the following hold: (1) the relative angle between X and Y is Z (2) one end of X is W (3) one end of X is V (4) equal W and V (5) the length of X is U T(s) (6) the length of Y is S T(s) (7) the distance between W and R is Q T(s) (8) one end of Y is R (9) one end of Y is P (10) equal R and P (11) W doesn't meet R, then equal Z and the arccosine of ((Q and Q and U and U) and S and S) and 2.0 and U and S |
(=>
(equal
(PerCapitaFn
(MeasureFn ?QUANTITY1 ?U) ?AREA)
(MeasureFn ?QUANTITY2 ?U))
(exists (?POPULATION)
(and
(equal ?POPULATION
(CardinalityFn
(ResidentFn ?AREA)))
(equal ?QUANTITY2
(DivisionFn ?QUANTITY1 ?POPULATION))))) |
Mid-level-ontology.kif 9383-9396 |
If equal the per capita 1 of %2 and X Y(s), then there exists Z such that equal Z, the number of instances in the resident of W, equal X, V, and Z |
(<=>
(measure ?OBJECT
(MeasureFn ?NUMBER OunceMass))
(measure ?OBJECT
(MeasureFn
(DivisionFn ?NUMBER 16.0) PoundMass))) |
Mid-level-ontology.kif 14890-14895 |
The measure of X is Y Ounce(s) if and only if the measure of X is Y and 16.0 pound mass(s) |
(=>
(and
(resourceConsumption ?PROC ?QUANT)
(instance ?QUANT FunctionQuantity)
(resource ?PROC ?RES)
(equal ?QUANT
(PerFn
(MeasureFn ?Q ?U)
(MeasureFn ?DC ?DU)))
(duration
(WhenFn ?PROC)
(MeasureFn ?T ?DU))
(holdsDuring
(BeginFn
(WhenFn ?PROC))
(measure ?RES
(MeasureFn ?X ?U)))
(holdsDuring
(EndFn
(WhenFn ?PROC))
(measure ?RES
(MeasureFn ?Y ?U))))
(equal ?Y
(MeasureFn
(SubtractionFn ?X
(MultiplicationFn ?T
(DivisionFn ?Q ?DC))) ?U))) |
Mid-level-ontology.kif 18957-18983 |
If All of the following hold: (1) X amount as resource for the Process Y (2) X is an instance of function quantity (3) Z is a resource for Y (4) equal X and the per of W V(s) and U T(s) (5) duration of the time of existence of Y is S T(s) (6) the measure of Z is R V(s) holds during the beginning of the time of existence of Y (7) the measure of Z is Q V(s) holds during the end of the time of existence of Y, then equal Q and (R and S and W and U) V(s) |
(=>
(property ?PROCESS ChemicalEquilibrium)
(exists (?RATIO ?TIME ?RESOURCE ?RESULT)
(=>
(and
(holdsDuring ?TIME
(resource ?PROCESS ?RESOURCE))
(holdsDuring ?TIME
(result ?PROCESS ?RESULT)))
(equal ?RATIO
(DivisionFn ?RESOURCE ?RESULT))))) |
Mid-level-ontology.kif 21535-21542 |
If X the attribute chemical equilibrium, then there exist Y, Z,, , W, V such that W is a resource for X holds during Z, V is a result of X holds during Zequal Y, W, and V |
(=>
(and
(instance ?A AstronomicalBody)
(approximateDiameter ?A
(MeasureFn ?D ?U))
(instance ?U UnitOfLength)
(instance ?P PointInSpace)
(part ?P ?A))
(exists (?C)
(and
(equal ?C
(CenterOfPlanetFn ?A))
(distance ?C ?P
(MeasureFn
(DivisionFn ?D 2.0) ?U))))) |
Mid-level-ontology.kif 28094-28108 |
If X is an instance of astronomical body, the approximate diameter of X is Y Z(s), Z is an instance of unit of length, W is an instance of point in space, and W is a part of X, then there exists V such that equal V and the centre of AstronomicalBody X is and the distance between V and W is Y and 2.0 Z(s) |
(=>
(approximateValue ?N1 ?N2)
(modalAttribute
(greaterThan 0.9
(DivisionFn ?N1 ?N2)) Unlikely)) |
Mid-level-ontology.kif 32446-32452 |
If the approximate value of X is Y, then the statement 0.9 is greater than X and Y has the modal force of unlikely |
(=>
(approximateValue ?N1 ?N2)
(modalAttribute
(greaterThan 0.9
(DivisionFn ?N2 ?N1)) Unlikely)) |
Mid-level-ontology.kif 32454-32460 |
If the approximate value of X is Y, then the statement 0.9 is greater than Y and X has the modal force of unlikely |
(=>
(equal
(MeasureFn ?H HourDuration)
(MTBFInstanceFn ?D))
(equal ?H
(DivisionFn
(AdditionFn
(ListSumFn
(PhysicalQuantityToNumberFn
(DeviceUpTimeDurationListFn ?D)))
(ListSumFn
(PhysicalQuantityToNumberFn
(DevicePlannedDownTimeDurationListFn ?D))))
(ListLengthFn
(DeviceFailTimeDurationListFn ?D))))) |
Mid-level-ontology.kif 34359-34373 |
If equal X hour duration(s) and The MTBF of Y is HourDuration, then equal X and (the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The List of deviceUpTime duration for Y is and the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The List of deviceUpTime duration for Y is) and length of The List of deviceFailTime duration for Y is |
(=>
(equal
(MeasureFn ?X HourDuration)
(MTTRepairInstanceFn ?D))
(equal ?X
(DivisionFn
(ListSumFn
(PhysicalQuantityToNumberFn
(DeviceFailTimeDurationListFn ?D)))
(ListLengthFn
(DeviceFailTimeDurationListFn ?D))))) |
Mid-level-ontology.kif 34644-34654 |
If equal X hour duration(s) and The time to repair of Y is HourDuration, then equal X, the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The List of deviceFailTime duration for Y is, and length of The List of deviceFailTime duration for Y is |
(=>
(equal
(MeasureFn ?X HourDuration)
(MTTRecoveryInstanceFn ?D))
(equal ?X
(DivisionFn
(ListSumFn
(PhysicalQuantityToNumberFn
(TimeToRecoveryDurationListFn ?D)))
(ListLengthFn
(TimeToRecoveryDurationListFn ?D))))) |
Mid-level-ontology.kif 34737-34747 |
If equal X hour duration(s) and The time to repair of Y is HourDuration, then equal X, the sum of PhysicalQuantityToNumberFn returns the numberic values of a list of The list of time to recovery duration for Y is, and length of The list of time to recovery duration for Y is |
(=>
(and
(instance ?EC EngineChoke)
(holdsDuring ?FSC1
(attribute ?EC DeviceOn))
(holdsDuring ?FSC2
(attribute ?EC DeviceOff))
(instance ?C EngineCylinder)
(capacity ?C ?M)
(instance ?FSC1 FourStrokeCompression)
(instance ?FSC2 FourStrokeCompression)
(eventLocated ?FSC1 ?C)
(eventLocated ?FSC2 ?C)
(instance ?A1 Air)
(instance ?F1 Fuel)
(part ?A1 ?MIX1)
(part ?F1 ?MIX1)
(measure ?MIX1 ?M)
(instance ?A2 Air)
(instance ?F2 Fuel)
(part ?A2 ?MIX2)
(part ?F2 ?MIX2)
(measure ?MIX2 ?M)
(instance ?U UnitOfMeasure)
(measure ?A1
(MeasureFn ?A1M ?U))
(measure ?A2
(MeasureFn ?A2M ?U))
(measure ?F1
(MeasureFn ?F1M ?U))
(measure ?F2
(MeasureFn ?F2M ?U)))
(greaterThan
(DivisionFn ?A2M ?F2M)
(DivisionFn ?A1M ?F1M))) |
Cars.kif 1253-1287 |
If All of the following hold: (1) X is an instance of engine choke (2) device on is an attribute of X holds during Y (3) device off is an attribute of X holds during Z (4) W is an instance of engine cylinder (5) V is a capacity of W (6) Y is an instance of four stroke compression (7) Z is an instance of four stroke compression (8) Y is located at W (9) Z is located at W (10) U is an instance of air (11) T is an instance of fuel (12) U is a part of S (13) T is a part of S (14) the measure of S is V (15) R is an instance of air (16) Q is an instance of fuel (17) R is a part of P (18) Q is a part of P (19) the measure of P is V (20) O is an instance of unit of measure (21) the measure of U is N O(s) (22) the measure of R is M O(s) (23) the measure of T is L O(s) (24) the measure of Q is K O(s), then M, K is greater than N, and L |
(<=>
(compressionRatio ?E ?R)
(and
(minCylinderVolume ?E
(MeasureFn ?MIN ?M))
(maxCylinderVolume ?E
(MeasureFn ?MAX ?M))
(equal ?R
(DivisionFn ?MIN ?MAX)))) |
Cars.kif 1792-1797 |
The compression ratio of X is Y if and only if the minimum volume of the cylinders in the engine X is Z W(s) and the maximum volume of the cylinders in the engine X is V W(s) and equal Y and Z and V |
(=>
(and
(instance ?T ElectricalTransformer)
(instance ?WC1 WireCoil)
(instance ?WC2 WireCoil)
(coilCount ?WC1 ?N1)
(coilCount ?WC2 ?N2)
(holdsDuring ?T
(measure ?WC1
(MeasureFn Volt ?V1))))
(and
(holdsDuring ?T
(measure ?WC2
(MeasureFn Volt ?V2)))
(equal ?V2
(MultiplicationFn ?V1
(DivisionFn ?N2 ?N1))))) |
Cars.kif 2984-2998 |
If All of the following hold: (1) X is an instance of electrical transformer (2) Y is an instance of wire coil (3) Z is an instance of wire coil (4) the number of coils in Y is W (5) the number of coils in Z is V (6) the measure of Y is volt U(s) holds during X, then the measure of Z is volt T(s) holds during X and equal T, U, V, and W |
(=>
(and
(instance ?BTS BimetalTemperatureSensor)
(instance ?M1 Metal)
(instance ?M2 Metal)
(not
(equal ?M1 ?M2))
(part ?M1 ?BTS)
(part ?M2 ?BTS)
(instance ?T1 TemperatureMeasure)
(instance ?T2 TemperatureMeasure)
(instance ?L1 LengthMeasure)
(instance ?L2 LengthMeasure)
(instance ?L3 LengthMeasure)
(instance ?L4 LengthMeasure)
(not
(equal ?T1 ?T2))
(not
(equal ?TM1 ?TM2))
(holdsDuring ?TM1
(and
(measure ?BTS ?T1)
(measure ?M1 ?L1)
(measure ?M2 ?L2)))
(holdsDuring ?TM2
(and
(measure ?BTS ?T2)
(measure ?M1 ?L3)
(measure ?M2 ?L4))))
(not
(equal
(DivisionFn ?L1 ?L2)
(DivisionFn ?L3 ?L4)))) |
Cars.kif 3951-3983 |
If All of the following hold: (1) X is an instance of bi_metal temperature sensor (2) Y is an instance of metal (3) Z is an instance of metal (4) equal Y and Z (5) Y is a part of X (6) Z is a part of X (7) W is an instance of temperature measure (8) V is an instance of temperature measure (9) U is an instance of length measure (10) T is an instance of length measure (11) S is an instance of length measure (12) R is an instance of length measure (13) equal W and V (14) equal Q and P (15) the measure of X is W, the measure of Y is U, and the measure of Z is T holds during Q (16) the measure of X is V, the measure of Y is S, and the measure of Z is R holds during P, then equal U, T, S, and R |
(=>
(and
(instance ?R RadiatingElectromagnetic)
(carrierFrequency ?R
(MeasureFn ?HZ Hertz))
(wavelength ?R
(MeasureFn ?L Meter)))
(equal
(MeasureFn ?L Meter)
(MeasureFn
(DivisionFn 299792458 ?HZ) Meter))) |
ComputingBrands.kif 1570-1577 |
If X is an instance of radiating electromagnetic, the frequency of the carrier of X is Y hertz(s), and the wavelength of X is Z meter(s), then equal Z meter(s) and 299792458 and Y meter(s) |
(=>
(and
(measure ?P1
(MeasureFn ?N1 Lumen))
(measure ?P2
(MeasureFn ?N2 Lumen))
(part ?P1 ?O)
(part ?P2 ?O)
(not
(equal ?P1 ?P2))
(greaterThan ?N1 ?N2)
(equal
(DivisionFn ?N1 ?N2) ?R)
(contrastRatio ?O ?R))
(not
(exists (?P3 ?P4 ?N3 ?N4)
(and
(measure ?P3
(MeasureFn ?N3 Lumen))
(measure ?P4
(MeasureFn ?N4 Lumen))
(part ?P3 ?O)
(part ?P4 ?O)
(not
(equal ?P3 ?P4))
(greaterThan ?N3 ?N4)
(greaterThan
(DivisionFn ?N3 ?N4) ?R))))) |
ComputingBrands.kif 3641-3662 |
If All of the following hold: (1) the measure of X is Y lumen(s) (2) the measure of Z is W lumen(s) (3) X is a part of V (4) Z is a part of V (5) equal X and Z (6) Y is greater than W (7) equal Y, W, and U (8) the contrast ratio of V is U, then there don't exist T, S,, , R and Q such that the measure of T is R lumen(s) and the measure of S is Q lumen(s) and T is a part of V and S is a part of V and equal T and S and R is greater than Q and R and Q is greater than U |
(=>
(and
(possesses ?Agent ?Stocks)
(measure ?Stocks
(MeasureFn ?Number ShareUnit))
(splitFor ?Event ?N1 ?N2))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?Event))
(and
(equal ?N3
(MultiplicationFn ?Number ?N2))
(equal ?NewNumber
(DivisionFn ?N3 ?N1))
(measure ?Stocks
(MeasureFn ?NewNumber ShareUnit))))) |
FinancialOntology.kif 2270-2280 |
If X possesses Y, the measure of Y is Z share unit(s), and W is split for V for U, then equal T and Z and U and equal S and T and V and the measure of Y is S share unit(s) holds during immediately after the time of existence of W |
(=>
(equal ?SPEED
(SpeedFn
(MeasureFn ?DISTANCE NauticalMile)
(MeasureFn ?TIME HourDuration)))
(equal ?SPEED
(MeasureFn
(DivisionFn ?DISTANCE ?TIME) KnotUnitOfSpeed))) |
Geography.kif 5464-5472 |
If equal X and Y nautical mile(s) per Z hour duration(s), then equal X and Y and Z knot unit of speed(s) |
(=>
(and
(subclass ?X ClothesWashingMachine)
(laundryApplianceMaximumClothesVolume ?X
(MeasureFn ?VOL Liter))
(waterConsumptionPerWashingCycle ?X
(MeasureFn ?WATER UnitedStatesGallon)))
(clothesWasherWaterFactor ?X
(DivisionFn ?WATER
(MultiplicationFn ?VOL 28.316846592)))) |
HouseholdAppliances.kif 1519-1528 |
If X is a subclass of clothes washing machine, maximum clothes volume X and Y liter(s), and water use per one clothes washing cycle X and Z united states gallon(s), then clothes washer water factor X, Z, Y, and 28.316846592 |
(=>
(and
(instance ?H HumanAdult)
(measure ?H
(MeasureFn ?N PoundMass)))
(and
(bloodVolume ?H
(MeasureFn ?N2 Liter))
(equal ?N2
(DivisionFn
(MultiplicationFn ?N 0.07) 2.33)))) |
Medicine.kif 5945-5954 |
If X is an instance of human adult and the measure of X is Y pound mass(s), then X has Z liter(s) of blood and equal Z, Y, 0.07, and 2.33 |
(<=>
(and
(instance ?YEAR
(YearFn ?Y))
(equal
(PopulationGrowthFn ?AREA ?YEAR) ?ADJUSTEDPERCENT))
(and
(equal
(SubtractionFn ?Y ?YP) 1)
(instance ?PREVIOUSYEAR
(YearFn ?YP))
(holdsDuring ?YEAR
(equal
(PopulationFn ?AREA) ?POPULATION))
(holdsDuring ?PREVIOUSYEAR
(equal
(PopulationFn ?AREA) ?PREVIOUSPOPULATION))
(equal
(DivisionFn ?POPULATION ?PREVIOUSPOPULATION) ?PERCENT)
(equal
(SubtractionFn ?PERCENT 1) ?ADJUSTEDPERCENT))) |
People.kif 52-64 |
X is an instance of the year Y and equal the population growth of Z and X and W if and only if equal (Y and V) and 1 and U is an instance of the year V and equal the population of Z and T holds during X and equal the population of Z and S holds during U and equal T and S and R and equal (R and 1) and W |
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
DivisionFn