Automated Deduction at Argonne

Our goal is to develop techniques and build practical programs to help mathematicians, logicians, scientists, engineers, and others with some of the deductive aspects of their work. Most of our work applies to problems that can be stated in the language of first-order logic with equality. Our programs have been applied to many real problems, mostly in abstract algebra and logic, and many new results have been obtained through their use. The members of the group are William McCune and Larry Wos.

Recent visitors and collaborators include Johan G. F. Belinfante, Maria Paola Bonacina, Zac Ernst, Branden Fitelson, Kenneth Harris, Ken Kunen, Bob Meyer, Olga Matlin, Dale Myers, R. Padmanabhan, Mike Rose, Bob Veroff, Hantao Zhang.

For further information, contact William McCune ( or Larry Wos (

Some Related Links

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.