The aim of this project was to evaluate and refine a visualisation tool (Jape) intended to support the formal reasoning of computer science students; and in so doing to increase understanding of the effectiveness of such tools in supporting training in the software development process, and in particular the cognitive processes and factors which affect visualisation software's ease of use.

The particular tool under investigation allows users to manipulate proofs on screen, using a mouse. An educator can control which logic Jape uses, how proofs are presented, and what actions the user can take. The implementation studied here - ItL Jape - is pre-loaded with propositional and predicate logic, with Natural Deduction rules and with Fitch boxes. When users apply a rule to a line of the proof, the software shows the effect on the proof.

Three empirical studies were carried out. In the first study, four subjects were videotaped as they used the tool Jape to assist them in constructing proofs as part of their course in formal logic. In the second study, usage data was collected from a year's cohort of computer science undergraduates. In the third study, ten subjects were videotaped using the program in task-based interviews.

A quantitative analysis of tests, surveys and logfiles suggests that subjects' backgrounds appeared to have little effect either on how much the program was used, or on how much progress was made with the conjectures in the program. However, on average, the more a subject used Jape the higher his or her score in course outcome measures. Moreover, progress in Jape was a significant factor in course performance, even when significant background variables such as gender, degree course, and prior programming experience are taken into account. This suggests that visualisation tools can be appropriate for different user groups.

Evidence from observation and interviews suggests that the main advantages of ItL Jape for many users are that it allowed them to consider many more examples than would be possible on paper, it encouraged experimentation with different routes to a proof, and it challenged inaccurate and forward-fixated reasoning.

In order to explore the role of visualisation in this process, a model of users' knowledge in terms of conjectured proof strategies was developed. Rule-specific strategies that enable users to decide what rule should be applied in given situations are distinguished from global strategies that help users to make and debug plans. Users are categorised by their prior knowledge of the rules. This model provides insights into the reasons for success and failure in learning from Jape, explains the differences in users' proving behaviour on paper and using the visualisation tool ItL Jape, and enables predictions about interface refinements that would enhance learning.