Another old publication of mine related to Harvey's program for computer verification of proofs is: ``Obvious Logical Inferences,'' Proceedings of the Seventh Joint International Congress on Artificial Intelligence, 1981, pp. 530-531. Martin