automating entry of derivations into the Physics Derivation Graph website

Published 2023-06-10T21:03:00.002Z by Physics Derivation Graph

1. user provides initial expression in Latex to web UI.
2. computer parses symbols and operators from Latex
3. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
4. computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
5. computer parses expression to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
6. if yes, continue; if no, go back to step 1 or provide corrections to AST.
7. user provides next expression in Latex
8. computer parses symbols and operators from Latex
9. if symbols match symbols used in this derivation, then associate with those; otherwise 
10. computer searches Physics Derivation Graph database of symbols and operators to find candidate symbols
11. if computer had to search PDG database, then computer provides candidate symbols to user and prompts, "which of the following symbols were you referring to?"
12. computer parses expression from step 7 to SymPy, returns AST to user, and prompts, "is this the AST you meant?"
13. computer uses brute force to check every inference rule using a CAS against the provided expressions to "guess" the inference rule. 
14. if valid inference rule is found, continue to next expression; if no valid inference rule is found, prompt user to provide inference rule.
15. Given the inference rule and associated expressions, use the CAS to verify the step.