Explanation: Here the focus is on a single inference rule and verifying the inference rule with respect to a logical basis like Zermelo–Fraenkel set theory in a formal proof assistent like Coq or Lean. This validation per inference rule would need to be applied to each inference rule used in the derivation. Who does this work: human content creator Motive for doing this work: |
Navigation:
|
The expression \begin{equation} \frac{1}{2} m_1 v^2 = \frac{G m_1 m_2}{r} \label{eq:initial} \end{equation} reduces to \begin{equation} v^2 = \frac{2Gm_2}{r} \end{equation} when both sides of Eq.~\ref{eq:initial} are multiplied by $$2/m_2$$
(Insert proof of "multiply both sides by" here)