A Review of Several Programs for the Teaching of Logic

Abstract
There has been an explosion of interest in the use of logic in computer science in recent years. This is in part due to theoretical developments within academic computer science and in part due to the recent popularity of Formal Methods amongst software engineers. There is now a widespread and growing popularity 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 practising computer scientist. This recognition that computer science has become a much more rigorous subject has lead a number of influential academics to call for changes to its curriculum that reflect this new rigour [8,12]. At the same time, it is a commonplace amongst computer science 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 necessary in order for logic to be used effectively. The purpose of this article 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 power of the encoded logic), their usability (the quality of the user interface) and their pedagogic value as teaching tools. We hope the review will act as a useful reference for the design and development of logic curricular within computer science.