A REVIEW OF SEVERAL PROGRAMS FOR THE TEACHING OF LOGIC

There has been an explosion of interest in the use of logic in compute r science in recent years. This is in part due to theoretical developm ents within academic computer science and in part due to the recent po pularity of Formal Methods amongst software engineers. There is now a widespread and growing recognition that formal techniques are central to the subject and that a good grasp of them is essential for a practi sing computer scientist. This recognition that computer science has be come a much more rigorous subject has lead a number of influential aca demics to call for changes to its curriculum that reflect this new rig our [8, 12]. At the same time, it is a commonplace amongst computer sc ience teachers that students find formal techniques difficult to learn . The growth of interest in logic has therefore been accompanied-by a further recognition that certain kinds of mechanical support are neces sary in order for logic to be used effectively. The purpose of this ar ticle is to describe a number of programs which have been developed to support the teaching of logic. Three broad criteria have been used in evaluating these systems. We consider their logical generality (the p ower of the encoded logic), their usability (the quality of the user i nterface) and their pedagogic value as teaching tools. We hope the rev iew will act as a useful reference for the design and development of l ogic curricula within computer science.