Kinematics

Up: Corpus of Examples
Previous: Holes
Next: Dynamics

Definition KIN.D1

A situation is feasible if no two objects overlap.

feasible(S : situation) -- Predicate.

Formalism:
feasible(S) < = >
forall (O1,O2 in objects(S) O1 != O2 => holds(S1,rcc_DS*(O1,O2))]

Definition KIN.D2

A history is kinematic iff (a) no two objects overlap in any situation in the history; (b) all objects move continuously; (c) fixed objects have a constant position.

Declaration: kinematic(H : history) -- Predicate.

Formalism:
kinematic(H) < = >
[forall(S in situations(H)) feasible(S)] ^
[forall(O in objects(H)) continuous(motion(O,H)) ^ [fixed(O,H) => motionless(O,H)]].

Fact KIN.F1

Being kinematic is a "liquid" property of a history (Shoham).

Formalism:
kinematic(H1) ^ subhistory(H2,H1) => kinematic(H2).
kinematic(H1) ^ kinematic(H2) ^ start(H1)=end(H2) => kinematic(splice(H1,H2)).

Fact KIN.F2

If H is kinematic then the history that results when some objects are removed from H is still kinematic.

Formalism:
[kinematic(H) ^ forall(O in objects(H1)) O in objects(H) ^ motion(O,H1) = motion(O,H)] =>
kinematic(H1).

Fact KIN.F3

Kinematics is invariant under time reversal.

Formalism: kinematic(H) => kinematic(reverse(H)).

Definition KIN.D3

Objects O1 and O2 are kinematically separable in S if they can be taken arbitrarily far apart.

Declaration: k_separable(O1,O2 : object; S : situation)

Formalism: k_separable(O1,O2,S) < = >
forall (D : distance) exists(H : history) kinematic(H) ^ start(H) = S ^ value(end(H),distance(O1,O2)) > D.

Fact KIN.F5

If O1 and O2 are separated by a plane in S, then they are kinematically separable in S.

Formalism: holds(S,plane_separates(P,O1 : object, O2 : object)) => k_separable(O1,O2,S).