This paper describes a new method for helping students improve their ability to develop proofs, a skill necessary for comprehending and appreciating the foundational topics of computer science. Our method transforms ordinary pen-and-paper homework problems into a puzzle-like game, where students connect dots to justify assertions, in a quest to reach a desired goal. We have implemented a software tutoring system using this method, for students to use at home as an optional study aid. Potentially, our system could one day become a full replacement for traditional hand-written homework, which has the additional benefit for course instructors of automating the grading of student work. Our system is also easy to adapt to any class that requires students to write proofs, and it is easy for instructors to create new problems to use with this system. This stands in contrast to many other educational tools for teaching proofs, which are limited to specific topic domains. We have demonstrated the versatility of our system by testing it in two computer science classes at a large public university. One was a Sophomore-level discrete mathematics course where the students were learning first-order prepositional logic, and the other was a Junior-level algorithms course where students were being first exposed to the concept of NP-completeness. Students from our experiments reported that they would like our system to be used in more of their classes.

This lightning talk describes the development of Complexity Tutor, an interactive tutoring system to assist students in understanding theoretical models of computation and computational complexity. Many computer science students, especially ones lacking a strong background in mathematics, struggle to learn these subjects with the traditional regimen of lectures and written homework assignments. When they are in the process of developing proofs for these homework assignments, they receive no immediate feedback that would illuminate their errors. We intend to remedy this. The main components of our system will entail a novel framework for constructing proofs, as well as a framework for producing algorithmic reductions. The first framework provides continuous feedback to the student on their approach and progress toward the needed proof. The second framework involves analyzing code the student writes in a pseudocode-like language, such as Python. Currently, we have prototypes, which show how to use our frameworks to construct NP-completeness reduction proofs. We are planning to test the efficacy of this system in theoretical computer science courses at the University of Massachusetts Amherst.