Academic journal article Educational Technology & Society

Automatic Hint Generation for Logic Proof Tutoring Using Historical Data

Academic journal article Educational Technology & Society

Automatic Hint Generation for Logic Proof Tutoring Using Historical Data

Article excerpt


According to the Joint Task Force on Computing Curricula (2005), discrete mathematics is a core course in computer science, and an important topic in this course is solving formal logic proofs. However, this topic is of particular difficulty for students, who are unfamiliar with logic rules and manipulating symbols. To allow students extra practice and help in writing logic proofs, we are building an intelligent tutoring system on top of our existing proof-verifying program. Results from student surveys and our experience in teaching discrete math indicate that students particularly need hints when they get stuck.

The problem of offering individualized help is not unique to logic proofs. Through adaptation to individual learners, intelligent tutoring systems (ITS) can have significant effects on learning (Anderson & Gluck, 2001). However, building one hour of adaptive instruction takes between 100 and 1000 hours of work for subject experts, instructional designers, and programmers (Murray, 1999), and a large part of this time is used in developing production rules that model student behavior and progress. A variety of approaches have been used to reduce the development time for ITSs, including ITS authoring tools and constraint-based student models. ASSERT is an ITS authoring system that uses theory refinement to learn student models from an existing knowledge base and student data (Baffes & Mooney, 1996). Constraint-based tutors, which look for violations of problem constraints, require less time to construct and have been favorably compared to cognitive tutors, particularly for problems that may not be heavily procedural (Mitrovic, Keodinger, & Martin, 2003). However, constraint-based tutors can only provide condition-violation feedback, not goal-oriented feedback that has been shown to be more effective (Van Lehn, 2006).

Some systems use teacher-authored or demonstrated examples to develop ITS production rules. RIDES is a "Tutor in a Box" system used to build training systems for military equipment usage, while DIAG was built as an expert diagnostic system that generates context-specific feedback for students (Murray, 1999). These systems cannot be easily generalized, however, to learn from student data. In example-based authoring tools, teachers work problems in what they predict to be common correct and incorrect approaches, and then annotate the learned rules with appropriate hints and feedback. The Cognitive Tutors Authoring Tool (CTAT) has been used to develop example-based tutors for genetics, Java, and truth tables (Koedinger, Aleven, Heffernan, McLaren, & Hockenberry, 2004). This system has also been used with data to build initial models for an ITS, in an approach called Bootstrapping Novice Data (BND) (McLaren, Koedinger, Schneider, Harrer, & Bollen, 2004). However, in both of these approaches, considerable time must still be spent in identifying student approaches and creating appropriate hints.

Machine learning has also been used to improve tutoring systems. In the ADVISOR tutor, machine learning was used to build student models that could predict the time students took to solve arithmetic problems, and to adapt instruction to minimize this time while meeting teacher-set instructional goals (Beck, et al., 2000). In the Logic-ITA tutor, student data was mined to create hints that warned students when they were likely to make mistakes using their current approach (Merceron & Yacef, 2005). Another logic tutor called the Carnegie Proof Lab uses an automated proof generator to provide contextual hints (Sieg, 2007).

Similar to the goal of BND, we seek to use student data to directly create student models for an ITS. However, instead of feeding student behavior data into CTAT to build a production rule system, our method generates Markov decision processes (MDPs) that represent all student approaches to a particular problem, and uses these MDPs directly to generate hints. …

Search by... Author
Show... All Results Primary Sources Peer-reviewed


An unknown error has occurred. Please click the button below to reload the page. If the problem persists, please try again in a little while.