The intent of this set of pages is to illustrate the role of the Physics Derivation Graph in a formalization workflow. To summarize, there is a sequence of increasing nuance from text to Latex expressions to a Computer Algebra System to proofs. The four main aspects get broken into additional components, and there is tagging of words and sections.

Mathematical proofs (item 12) and semantic enrichment (items 4, 5, 6) both play a role in formalization of Physics. There is a third aspect addressed by the Physics Derivation Graph (items 7 through 11).

The examples provided are visual rather than implementations of specific methods.

1. lecture video: verbal overview with whiteboard
2. hand-written notes: contemporaneous with the lecture delivery
3. Latex document: after the lecture, convert hand-written notes to Latex
4. Content tags (as described by OMdoc)
   • section document structure
   • tagging words
   • expression semantics
5. tags for sections and words and expressions: combine all content tagging into a single document
6. concepts to variables: relation between keywords and symbols
7. all steps: all the implied steps documented
8. derivation graph: inference rules
9. replace symbols with numeric ID: globally consistent method for referriing to the same concept
10. validation of steps: use a Computer Algebra System to check each step in a derivation
11. validation of dimension: use a Computer Algebra System to check dimensional consistency of each expression
12. proof of inference rule: proofs that the inference rules are valid in a selected logical basis

The examples provided may have flaws and inconsistencies. Hopefully there is sufficient illustration to convey intent.

The Physics Derivation Graph does not depend on semantic tags. The PDG could be done after creating the Latex document.

There is a gap between sementically tagged and the Physics Derivation Graph. The relation is not clear.

The graph structure of a derivation does not fit into the hierarchical RDF data structure.

References

1. "Understanding Scientific Documents with Synthetic Analysis on Mathematical Expressions and Natural Language" by Takuto Asakura (2019) at CICM 2019
2. "Towards an Ontology of Physics" by J. B. Collins and D. Clark
3. "Metamath proof explorer: A Modern Principia Mathemtica" by D. A. Wheeler