Latex will be input by the user for the PDG; the user will not need to supply the AST as input. To validate a step, the AST is needed. This presents a few challenges:
- Is the input valid tex?
- Is the valid tex a mathematical expression?
- Is the valid mathematical expression consistent with the step?
A step in a derivation is defined as the application of a single inference rule with one or more expressions as input, feed, or output.
There are a few options for parsing mathematical tex:
- write a custom parser
- use an existing parser, e.g. MathJax
No comments:
Post a Comment