Computerised logic teaching was the thing, in the past decade. But ten years on, what has happened? Where have all the plans and hopes gone? Most of the brave new programs of the 1980s are gathering dust on the hard disc. Technology has not, it would appear, had quite the impact that its philosophical adherents would have liked.
I surveyed philosophy departments in the United Kingdom in 1990 as part of an Enterprise in Higher Education project, and found a number of them eagerly grasping the computerised nettle. There was Ulster's Coleraine campus, where programs written in-house, such as a version of that philosophical evergreen the Prisoner's Dilemma, and interactive philosophy texts using HyperCard were said to be successful and popular; and St Andrews, where MacLogic was developed for the Apple-dominated US education market. Glasgow, Leeds and Edinburgh had written their own proof checking programs, some in BASIC, some in Pascal and others in Prolog. Proof checking is well suited to computerisation, as it is dull and mechanical - the computer applies various rules to symbols in the manner of algebra.
When the survey was made, DOS still ruled. "Point and click" graphical user interfaces were largely confined to Mac users. Throughout the 1980s, academics laboured contentedly with their home-grown programs while in the background a tidal wave of sophisticated graphical programming was building up. The result has been that the logic programs were out of date and old fashioned almost before they were born. No one wants to type strings of funny symbols, to receive either "ok" or "parse error line 5".
Typically, the logic programs have been found not to fit in with either the pre-existing courses, or the teaching styles of the lecturers, and they have either been dropped or left as an option. Edinburgh students, for example, were in 1990 using "Lemmon Aid" (a pun on the logician), a gift from their computer enthusiast professor, John Slaney. Since then, programs teaching "how to construct natural deduction systems in sequential and predicate logic" have come and gone in bewildering succession.
Peter Milne, computing expert in Edinburgh's philosophy department explains that the problems have been twofold. One is that there are different logics and the computer's logic is not necessarily the department's. So it was with Bertie3, an import from the US, whose "honking and tooting" proved less useful when it emerged that its view of validity differed significantly from everyone else's.
Bertie is still on the the university system, but deleted from the philosophy department's itinerary. Not many people use its successor Twootie either, although Milne has tried to persuade students of "the benefits to be gained for the small amount of time and effort needed".
At Leeds, where staff spent much of the 1980s happily developing an ambitious and complex program looking at axioms rather than simply checking proofs, logic has taken something of a nose dive. The new language proved rather a flop although there are, as ever, plans to resurrect something from it. With the department's intake changing from specialists expecting to be given loads of logic to generalists looking for short tasty modules, the era of "mass logic courses" of up to 500 students has come to an end, and with it most of the usefulness of computerised logic teaching. What remains, according to Peter Millican, lecturer in philosophy and computing at Leeds, is the higher level logic courses requiring deeper skills and "meta-theory" rather than ways to repetitively take students through simple proofs. So what are the prospects for computerised logic? Not entirely bad, if Keith Stenning, director of the Human Communication Research Centre at Edinburgh, is to be believed. Professor Stenning says that the next generation of logic programs is about to arrive, promising "a way to develop general reasoning skills in students through diagrammatic representations".
Programs such as Tarski's World and Hyper Proof produce a kind of 3D checkerboard world of cuboids and spheres creating a kind of logical landscape representing rules and deductions. The computer, says Stenning, interacts actively with the student, generating designs and offering instant feedback. According to research by the Edinburgh centre and logicians at Stanford, California, there are two types of problem solvers - diagrammatic and non-diagrammatic. Stenning believes that students can use the graphical interface to improve their scores in intelligence tests, develop the ability to translate between formal and informal modes of thinking, and test and revise theories and cases. In fact he suggests the program could be divorced from formal logic and applied instead to ordinary language problems and scenarios. But not if, as one philosopher put it, students find it is bad enough learning logic, without having to learn computers as well.
Martin Cohen is editor of The Philosopher (philosopher@ilkfoe. demon.co.uk)