Rod Burstall - A proof tool for teaching Natural Deduction and Induction

I have been teaching an operational semantics course and developed a tool to teach students about logic and the sort of induction you need for proofs about programs and languages. The main idea is that it should be easy to learn use and oriented to proof discovery, but giving you a readable proof at the end. Since our students know a lot about programming and not much about mathematics, I try to use programs as a paradigm for presenting proofs. I'll talk about how we use it and how we test students, and present my unfounded prejudices about the matter. I'll be interested to hear from other people about their experience.