
Abstract 1. Introduction Propositional logic is a fundamental topic in computer science and mathematics (Merceron 2001). When studying formal logic, students learn how conclusions can be validly derived from a set of premises using logical rules. The concept of formal proof is not easy for students to understand, and the best way to grasp it is through exercises. However exercises are beneficial only with feedback. Students have to know whether they are right or wrong, and, when they are wrong, they have to know what is wrong and be given a chance to try again. But the increasing number of students in computer science makes it difficult to provide enough human tutors to assist students in this part of their learning. Computers themselves can help with this problem. Formal proofs, by their very nature of being formal, can be automated. This means also that computer programs can check formal proofs given by students. Thus, formal logic is an excellent topic to be presented by means of computerbased tutorials. Existing tools for practicing logic have not matched our expectations, mainly because their GUIs were not attractive enough and they had high barriers to initial use. This led us to design our own tool. The Logic Tutor presents exercises of formal proofs in propositional logic, checks students' answers, and provides feedback. It has been developed with an emphasis on educational value. Educational value in the Logic Tutor is achieved by five means. First the Logic Tutor provides step by step feedback. Each time a student enters a line of the proof, the line is checked for correctness. In case of a mistake, extensive explanation is provided by the use of a 'cascading mistakes' principle (See the multimedia presentation in section 2.1). Second, several levels of help are provided, ranging from a quick start button, to a handy reference to rules of inference, to a tutorial on proof strategies. Third, the "history" feature provides students not only with the exercises they have done or attempted, but also with statistics on their mistakes. Fourth, files of exercises may be easily created with a possibility of comments, hints, and partial or even complete solutions. And lastly, the Logic Tutor has a simple and attractive graphical interface. This simplicity helps to eliminate the barriers to student learning. 


Figure 1. Snapshot of the screen when a new question to solve is currently loaded. 
2.1 Handling
of Mistakes When students make mistakes, they have quite often made more than one error. This leads to the principle of cascading mistakes. First it is checked that all the fields in the answer are filled with the right type of data. Then the formula is checked for its syntax. In case of a mistake, the parser provides good error messages. Then the real cascade in the derivation begins. The lower level represents general mistakes like incorrect line number and invalid application of the rule. The next level is when the expert module detects that the rule specified by the user can be applied, using lines other than those provided by the user. Then the next level is for cases where the rule specified by the user cannot be applied but where another one can be applied with the same lines provided by the user. The higher level of mistakes deals with more specific mistakes, like the use of Simplification without Commutation to deduce the right hand side of a conjunct. A clear illustration of the principle of cascading mistake can be found here. All mistakes are context sensitive, which means that explanations are adjusted to the current exercise.A careful analysis of mistakes made by the students led to the organisation of the database mistakes according to patterns. Currently the database has 50 patterns. Two patterns are given as examples below. Incorrect Justification Pattern: The mistakeanalyzer looks at the deduction and can determine that the user meant to use, say, Commutation, but confused the name with Association. Incorrect Line of Reference Pattern: The mistake analyzer picks up typing errors when the user enters the line number references. It will inform them of the correct line numbers by printing "Try using (1, 3) instead", for example. 
A Powerpoint file (~120 KB) or a ppz file (~83 KB) available for download. 
3. Preliminary
Evaluation 

Figure 2. Evaluation results for usability and looks 

Figure 3. Evaluation results for Course involvement 
The evaluation survey also questioned the users about shortcomings of the system. Some minor problems such as the display of the conclusion while doing an exercise and the ability of opening several windows were mentioned. The most obvious suggestions were added to the system accordingly. 
4. Conclusion Immediate future work includes modifying the present tool according to the results of the preliminary evaluation to increase users' comfort. We are also working on a Teacher Assistant System (Yacef 2000), which will embed:
This will improve even more the educational value of the tool, both for the student and for the lecturer. Finally, our aim is to increase the multimedia aspect of this course to encourage flexible and independent learning. Our logic course has been redesigned this year to include this tool at the teaching, training and assessment levels. It includes more media, like a set of commented solutions accessible from the web. Tutors have written commented solutions after watching mistakes made and difficulties encountered by students while solving exercises. Comments include traps to avoid and hints to find solutions. The course evaluation last year has shown that students find them very valuable. 
5. Acknowledgements

6. References Du Boulay, B. (2000). Can we learn from ITSs ?, Invited talk at the 5th International Conference on Intelligent Tutoring Systems, Montreal, June 2000. Dugdale, S. (1992) The design of computerbased mathematics education. In ComputerAssisted Instruction and Intelligent Tutoring Systems: shared goals and complementary approaches. J.H Larkinand R.W Chabay, eds. Lawrence Erlbaum, pp. 1145. Greer J. & McCalla, G. (1994). Student Modelling, the key to individualised knowledgebased instruction. Berlin, SpringerVerlag. Gugerty, L. & Hicks, K. (1993), Nondiagnostic intelligent tutoring systems, Proceedings of the 15th interservice/industry training systems and education conference. Orlando, Florida, pp. 450459. Kay, J.(1997). Learner know thyself : student models to give learner control and responsibility. Keynote address at ICCE'97, Kuching. Merceron, A. (2001). Languages and Logic. Pearson Education Australia. Yacef, K. (1999) Towards an intelligent instructorassistant system for training operators of complex and dynamic skills. Ph.D. Dissertation. University of Paris 5 and INRIA. Yacef, K. (2000). Providing an intelligent tutoring aid to assist undergraduate teaching. SESQUI Internal proposal report, University of Sydney, Sydney, Australia. 
**********
End of Document **********
