Conclusions

MathCheck can be used for exercising various aspects of elementary university math

• also logic

Building the equation mode forced to formalize `rArr` and `hArr` in the presence of `_|_`

• 3-valued logic, `not`U yields U
• U is undefined (unknown is FUT)
• `rArr` and `hArr` are reasoning operators, not propositional operators
• only regular predicates can be written, which partly explains why it works

Thank You for Attention!

Questions?