Corrections and Comments on
in the NY Times, Dec. 10, 1996
Tarski's name and university are incorrect.
It should have been written Alfred Tarski at UC Berkeley.
The article incorrectly states:
"Computers have found proofs of mathematical conjectures before, of
course, but those conjectures were easy to prove".
Many of those previous proofs were quite difficult. Look
for many examples.
There are a few theoretical applications of the Robbins Theorem
(on the size of axiom systems)
but no practical ones that we know of.
Wos is not McCune's supervisor :-) Both are staff members in the
Mathematics and Computer Science Division; their supervisor is
The correct name of our workplace is Argonne National Laboratory.
We frown upon the name Argonne Labs.
The automated deduction project is supported by the Mathematical, Information,
and Computational Sciences Division subprogram of the
Office of Computational and Technology Research,
U.S. Department of Energy, under Contract W-31-109-Eng-38.