Joachim Breitner's Homepage

I’m currently on the way home, returning from a four-day workshop for high school students; ages 13 to 20, grade 9 to 13. My goal was to teach them something about proofs and logic, in a ambitiously formal and abstract way. For this workshop, I created a computer program called “The Incredible Proof Machine” that allows the kids to explore creating a proof, by placing blocks on a canvas and drawing connections between them (see my previous blog post for an introduction).

Subtracting time spent on on breaks, organizational stuff, the time the student needed to prepare a final presentation, I think we were working for a total of 14 hours, during which we covered propositional logic. I generally let the students explore and try to solve the tasks of one session mostly on their own, followed by a common discussion of what they have just done, what it means why it makes sense etc. The sessions were: assumptions and conclusions in general, with conjunction; implication; disjunction; falsum and tertium non datur. We also briefly discussed “paper proofs” with the student: how they look, and how they relate to the Proof Machine proofs. We had some lecture notes that we handed out pice-wise after each session.

The sections were mildly¹ password-protected to avoid that the quicker students would work ahead, thus keeping the group together. One or two of the 13 students were doing very well and eventually, I gave them the passwords to the predicate logic section and let them work them on them on their own. The quickest managed to solve almost all of these as well, but (as far I as I can tell) without a deeper understanding of the quantifiers, and more a mechanical intuition.

As expected, the students were able to solve most of the exercises, even when a proper understanding of the logical semantics was not yet fully developed. This was by design: I believe that this way it was more motivating and encouraging, as they could “make it work”, compared to a more traditional approach of first throwing a lot of theory at them and then expecting them to apply it. This was confirmed by their feedback after the workshop.

I was happy with my implementation. The students immediately could work with it with very few hick-ups, and only one minor bug occurred², which I could fix on the spot. Having everything run on in the browser was a big plus, given that we had no stable internet connection for everyone: Once the Incredible Proof Machine was loaded, the student could continue to work offline.

Personally, I find that the UI is occasionally too sluggish, especially on the weaker laptops, but it seems that the students did not seem to mind. Some students tried to connect outputs with outputs or inputs with inputs and the visualization did make it clearly visible that such a link is not actually connected to the block. The predicate logic part is a bit less convincing, with e.g. scoping of local constants not easily understood. I would say that this part would work better if some explanation is given before the students start working on the more involved rules.

Our room was equipped with a smartboard, and I was delighted when I found out, mostly by accident, that I could actually use my finger to drag the blocks of the proof and to draw connections. This not only gave me a “Minority Report”-like feeling, but also meant that it was much easier for the students to follow my explanations when they could just watch my hand, instead of trying to locate the mouse pointer on a regular projector. I’m generally doubtful whether such fancy technological toys are useful in the class room, but in this case at least I liked it. The ability to scribble anywhere on the screen was occasionally a plus as well.

All in all I believe the Proof Machine was a useful tool, and I am sure that without it, it would have been tricky to have students voluntarily spend 14 hours on such a relatively dry and abstract topic. Given the amount of work that went into the development, I hope that this will not be the last occasion where it is put to good use. So if you have to teach formal logic and natural deduction-style proofs, you are welcome to use the Incredible Proof Machine to get your students excited. It is purely static, i.e. needs no special server-side infrastructure, and you can define your own logic (i.e. proof rules), sessions and tasks.

Also, there are a few interesting way in which the Proof Machine could be extended. In particular, I’d like it to be able to generate a “normal”, natural-language proof from a given proof – even if it will sound a bit mechanical – and then use hover-highlight effects to relate the formulas and sentences in the text proof to the connections and blocks in the graphical proof. Contributions are welcome!