George Walford: Precision In Thought

This is from Philosophical Facts No.3, Summer 1985, issued by Philosophy Documentation Center:

LOGICIAN is a text processor for logicians and logic teachers. The program provides an efficient means of quickly producing error-free natural deduction proofs for use as examples and exercises for students. LOGICIAN differs from ordinary text editors in that it understands and can apply 25 common inference rules including six rules of quantification and identity. Proofs are constructed by first typing in the premises and/or axioms. After that, the user simply tells the program which inference rules to apply to which steps of the proof. The program constructs and displays the actual steps of the proof.

(No, that reference to the limited understanding of text editors is not an author hitting back at the people who issue the rejection slips; a “text editor” is a type of computer programme).

A computer programme able to handle Aristotelian logic; clearly the inventors have got closer to artificial intelligence than most of us had realised. Or is it – could it possibly be – that Aristotelian logic does not after all require any very high mentality, that it is rather a matter of mechanical complications which a computer is well equipped to manage?

from Ideological Commentary 21, November 1985.