monitoring patterns of use One of the possibilities opened up by the Web access to Nuprl libraries is that we can use CoNote to monitor how students use the interactive course material. We can find out which definitions are referred to most often, which proofs are read to great depth, which expressions must be fully disambiguated, which lemmas are most often viewed. These measures will give us a map of the difficulty of the cognitive terrain.
Our plan for the courseware offers a technique for evaluating the formalism. Since we plan to create ordinary hypertext lessons with links into and out of the formal text, we can monitor the student traffic into the formal text for various assignments.
formative evaluations Professor Jere Confrey [18] of the Cornell Education Department has agreed to meet with us as we plan systematic formative evaluations and assess the results.
We will use the Spring '98 offering of the Cornell discrete mathematics course as a control group for measuring the effectiveness of our course material to address the problems of omission, ambiguity, location of information and motivation discussed in 2. We will also use results on similar homework assignments to evaluate understanding of induction and logic. In general we will be looking to see if students use the material as we anticipate. Do they follow definition chains? Do they consult the formal proof when encountering obstacles to understanding the ordinary text? Do they often execute the algorithms associated with computational theorems in order to produce more examples of a result? Do they experiment by applying induction tactics to a variety of formulas to learn the structure of subgoals?
Integration of our courseware with the Cornell CoNote system [27] will enable students to ask questions about the course material interactively. We can reply interactively and add new formal or informal material as required.