 |
Goal: Write down all known mathematical physics in a way that can be both read by humans and checked by a computer algebra system.
To enact that, the Physics Derivation Graph provides a schema and software infrastructure for the systemization of documenting mathematical physics. By semantically enriching mathematical expressions, connections between topics is observable.
For the impatient, see the Physics Derivation Graph navigation.
Example: A simple example is the relation between period, \(T\), and linear frequency, \(f\). The mathematical expression of the relation is \(T=1/f\). To express frequency as a function of period, multiply both sides of the expression by \(f\) to get a new expression, \(T\ f=1\). Finally, divide both sides of the second expression by \(T\) to yield the third expression, \(f=1/T\).
|
In this example, there are three expressions: \(T=1/f\), \(T\ f=1\), and \(f=1/T\). Each expression is defined by a left-hand side, a relation operator (here "="), and a right-hand side. Two instances of the Equivalence relation relate the three expressions. These relations between expressions are called inference rules. The generic form of the first inference rule used in the example is "multiply both sides of an expression by a quantity to yield a new expression." Similarly, the second inference rule is generically, "divide both sides of an expression by a quantity to yield a new expression."
The database for documenting relations in derivations of Physics is a JSON file. This can be transformed into other formats; see the PDG navigation page.
Motivation: Mathematical Physics uses the tools of math applied to measurements of our environment. Physics is a unique field in that all existing knowledge can be recorded. Another aspect that is unique is that the result can be checked for correctness by a computer algebra system. A third unique facet to Physics is that claims can be tested by experiment.
A derivation is a sequence of steps. Each step in a derivation involves an "inference rule." An inference rule relates one or more math expressions. An inference rule may require one or more "feed" values. An expression is, by default, composed of (LHS, relation operator, RHS). Expressions include both equations (the relation operator is equality) and inequalities (the relation operator is an inequality).
"Inference rules", "expressions", and "feeds" are words specific to the Physics Derivation Graph.
Represented graphically, their relation is
Read this directed graph as, "The inference rule acts on the input expression and, combined with the feed, produces the output expression." Inference rules can be considered as functions; the above picture would be
def inference_rule(input_expression, feed):
return output_expression
Use the Physics Derivation Graph navigation, or read the FAQ, or review the documentation.
See also other related or similar projects, literature review, and experiments in annotation.