This paper describes a tutorial program that serves a double role as an educational tool and a research environment. First, it introduces students to fundamental concepts of propositional logic and gives them practice with theore m proving. Secondly, the program provides an environment in which we can track student learning, explore cognitive issues of human problem solving, and investigate the possibilities of interactive human/machine learning. We have tested the tutorial program on two groups of Discrete Mathematics students and report the results of our assessment. We also discuss the contributions and future directions of our research in interactive human/machine learning. 1 Background Propositional logic is a staple of introductory computer science courses, often taught in CS I, Discrete Mathematics, or both. Mastery of the concepts of formal logic, so basic to the problem-solving inherent in computer science, requires practice, particularly in the deductive methods of formal th...