In this thesis we study the domains of standard equivalences and
normal forms, Hilbert-style axiomatic proofs, and structural induction. The main questions we address are:
How can we describe the expert knowledge of these topics in a domain reasoner?How can we generate feedback and feed forward?
What is the effect of the use of the designed tools in logic education?