Dynamics
Up: Corpus of Examples
Previous: Kinematics
Next: Boxes
Definition Dyn.D1
Up is a direction.
Declaration: up : direction --- Constant.
Definition Dyn.D2
A history is dynamic if it can physically occur. We
do not give necessary and sufficient conditions for dynamic histories;
rather, here and in the various pages describing particular systems,
are many necessary conditions and some small number of sufficient
conditions.
Declaration dynamic(H : history) --- Predicate.
Definition Dyn.D3
An object is motionless throughout history H if its position
does not change.
Declaration motionless(O : object; H : history) --- Predicate.
Formalism
motionless(O,H) < = >
forall(S1,S2 in H) value(S1,placement(O)) = value(S2,placement(O)).
Definition Dyn.D4
An object is fixed in history H if it is constrained to
be motionless in H.
Declaration fixed(O : object; H : history) --- Predicate.
Axiom:
fixed(O,H) => motionless(O,H).
Definition Dyn.D5
An object O is still in situation S if its linear and angular
velocities are zero.
Declaration still(O : object) : boolean fluent -- Function.
Definition Dyn.D6
An external force F is applied to object O in situation S.
Declaration applied(F : external_force; O : object;
S : situation)
Definition Dyn.D7
Let OS1 and OS2 be sets of objects.
Object OS1 are isolated from all influences OS2 throughout
history H if the objects in OS1 do not come into contact with any other
objects besides those of OS1 and OS2, and no external forces are applied
to them.
Declaration: isolated(OS1, OS2 : set[object]; H : history)
Formalism:
isolated(OS1,OS2,H) < = >
forall(S in H, O in OS1)
[forall(O : object) ~(O in OS1) ^ ~(O in OS2) => holds(S,rcc_DC(O,O1))] ^
~exists(F : external_force) applied(F,O,S).