(=>
(and
(instance ?R Rotating)
(fulcrum ?R ?F)
(lever ?R ?L)
(rotationalAxis ?R ?X))
(holdsDuring
(WhenFn ?R)
(exists (?P)
(and
(instance ?P PointInSpace)
(part ?P ?X)
(meetsSpatially ?P ?F)
(meetsSpatially ?P ?L))))) |
Mid-level-ontology.kif 1582-1594 |
If X is an instance of rotating, Y is the lever of X, lever X and Z, and W is the axis of X, then there exists V such that V is an instance of point in space, V is a part of W, V meets Y, and V meets Z holds during the time of existence of X |
(=>
(and
(verticalAxis ?X PlanetEarth)
(instance ?R Rotating)
(rotationalAxis ?R ?X)
(betweenOnPath NorthPole ?C SouthPole ?X))
(centerOfMass ?C PlanetEarth)) |
Geography.kif 5276-5282 |
If X is the verticalAxis of planet earth, Y is an instance of rotating, X is the axis of Y, and Z is between North Pole and South Pole on path X, then Z is the centerOfMass of planet earth |
(=>
(and
(instance ?V Aircraft)
(instance ?R Rotating)
(patient ?R ?V)
(rotationalAxis ?R ?A)
(transverseAxis ?A ?V)
(holdsDuring
(BeginFn
(WhenFn ?R))
(pitch ?V ?X))
(holdsDuring
(EndFn
(WhenFn ?R))
(pitch ?V ?Y)))
(not
(equal ?X ?Y))) |
Transportation.kif 3226-3238 |
If All of the following hold: (1) X is an instance of aircraft (2) Y is an instance of rotating (3) X is a patient of Y (4) Z is the axis of Y (5) Z is the transverseAxis of X (6) X is heading at W degree from its level of plane axis. holds during the beginning of the time of existence of Y (7) X is heading at V degree from its level of plane axis. holds during the end of the time of existence of Y, then equal W and V |
(=>
(and
(instance ?V Aircraft)
(instance ?R Rotating)
(patient ?R ?V)
(rotationalAxis ?R ?A)
(verticalAxis ?A ?V)
(holdsDuring
(BeginFn
(WhenFn ?R))
(yaw ?V ?X))
(holdsDuring
(EndFn
(WhenFn ?R))
(yaw ?V ?Y)))
(not
(equal ?X ?Y))) |
Transportation.kif 3265-3277 |
If All of the following hold: (1) X is an instance of aircraft (2) Y is an instance of rotating (3) X is a patient of Y (4) Z is the axis of Y (5) Z is the verticalAxis of X (6) X is heading at W of its longitudinalAxis. holds during the beginning of the time of existence of Y (7) X is heading at V of its longitudinalAxis. holds during the end of the time of existence of Y, then equal W and V |
(=>
(and
(instance ?V Aircraft)
(instance ?R Rotating)
(patient ?R ?V)
(rotationalAxis ?R ?A)
(longitudinalAxis ?A ?V)
(holdsDuring
(BeginFn
(WhenFn ?R))
(roll ?V ?X))
(holdsDuring
(EndFn
(WhenFn ?R))
(roll ?V ?Y)))
(not
(equal ?X ?Y))) |
Transportation.kif 3306-3318 |
If All of the following hold: (1) X is an instance of aircraft (2) Y is an instance of rotating (3) X is a patient of Y (4) Z is the axis of Y (5) Z is the longitudinalAxis of X (6) X is rolling at W of its longitudinalAxis. holds during the beginning of the time of existence of Y (7) X is rolling at V of its longitudinalAxis. holds during the end of the time of existence of Y, then equal W and V |
