(=>
(and
(instance ?O Odometer)
(instance ?V Vehicle)
(part ?O ?V)
(instance ?T Translocation)
(instrument ?T ?V)
(path ?T ?P)
(distanceOnPath
(MeasureFn ?D ?U) ?P)
(instance ?U LengthMeasure))
(hasPurpose ?O
(exists (?M ?L ?DIST)
(and
(instance ?M Measuring)
(instrument ?M ?O)
(measurementReading ?O ?DIST)
(inList ?D ?L)
(holdsDuring
(WhenFn
(EndFn ?M))
(and
(equal ?DIST
(MeasureFn
(ListSumFn ?L) ?U))
(not
(attribute ?O ResetMeasuringDevice)))))))) |
Cars.kif 2824-2850 |
If All of the following hold: (1) X is an instance of odometer (2) Y is an instance of vehicle (3) X is a part of Y (4) Z is an instance of translocation (5) Y is an instrument for Z (6) W is path along which Z occurs (7) the distance of W is V U(s) (8) U is an instance of length measure, then X has the purpose there exist T, S and R such that T is an instance of measuring and X is an instrument for T and R is a measurement reading of X and V is a member of S and equal R and the sum of S U(s) and reset measuring device is not an attribute of X holds during the time of existence of the end of T |
(=>
(and
(instance ?M Marathon)
(agent ?M ?H)
(path ?M ?P)
(distanceOnPath
(MeasureFn ?N Mile) ?P))
(equal ?N 26.2)) |
Sports.kif 293-300 |
If X is an instance of marathon, Y is an agent of X, Z is path along which X occurs, and the distance of Z is W mile(s), then equal W and 26.2 |
(=>
(and
(instance ?M HalfMarathon)
(agent ?M ?H)
(path ?M ?P)
(distanceOnPath
(MeasureFn ?N Mile) ?P))
(equal ?N 13.1)) |
Sports.kif 307-314 |
If X is an instance of half_marathon, Y is an agent of X, Z is path along which X occurs, and the distance of Z is W mile(s), then equal W and 13.1 |
(=>
(distanceOnPath ?DIST ?PATH)
(exists (?GP)
(and
(instance ?GP GraphPath)
(abstractCounterpart ?GP ?PATH)))) |
Transportation.kif 3940-3945 |
If the distance of X is Y, then there exists Z such that Z is an instance of graph path and the abstract counterpart of X is Z |
(=>
(and
(distanceOnPath ?DIST ?PATH)
(pathInSystem ?PATH ?SYS)
(routeStart ?START ?PATH)
(routeEnd ?END ?PATH)
(abstractCounterpart ?GRAPH ?SYS))
(exists (?S ?BN ?EN)
(and
(subGraph ?S ?GRAPH)
(equal ?BN
(BeginNodeFn ?GRAPH))
(equal ?EN
(EndNodeFn ?GRAPH))
(abstractCounterpart ?BN ?START)
(abstractCounterpart ?EN ?END)))) |
Transportation.kif 3947-3960 |
If the distance of X is Y, Z is a path in system of X, W is the start of X, V is the end of X, and the abstract counterpart of Z is U, then All of the following hold: (1) there exist T, S (2) R such that T is a subgraph of U (3) equal S (4) the beginning of U (5) equal R (6) the end of U (7) the abstract counterpart of W is S (8) the abstract counterpart of V is R |
(=>
(and
(instance ?S RadiatingSound)
(path ?S ?R)
(distanceOnPath ?L ?R)
(duration
(WhenFn ?S) ?D)
(speedOfSound ?Q ?R
(WhenFn ?S)))
(equal ?Q
(SpeedFn ?L ?D))) |
Transportation.kif 5116-5126 |
If X is an instance of radiating sound, Y is path along which X occurs, the distance of Y is Z, duration of the time of existence of X is W, and the speedOfSound for V at Y is V, then equal V and Z per W |
(=>
(and
(instance ?F Flying)
(patient ?F ?A)
(instance ?A Aircraft)
(path ?F ?R)
(distanceOnPath ?L ?R)
(duration
(WhenFn ?F) ?D)
(speedOfSound ?Q ?R
(WhenFn ?F))
(holdsDuring
(WhenFn ?F)
(measure ?A
(MeasureFn ?M MachNumber))))
(equal ?M
(DivisionFn
(SpeedFn ?L ?D) ?Q))) |
Transportation.kif 5225-5237 |
If All of the following hold: (1) X is an instance of flying (2) Y is a patient of X (3) Y is an instance of aircraft (4) Z is path along which X occurs (5) the distance of Z is W (6) duration of the time of existence of X is V (7) the speedOfSound for U at Z is U (8) the measure of Y is T Mach number(s) holds during the time of existence of X, then equal T, W per V, and U |
