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 firstorder 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.
 Recent work on
search strategies
and
inference rules.

New Results
obtained with our programs.
 Otter,
a program that searches for proofs.
 EQP,
a program that searches for equational proofs.
 MACE,
a program that searches for Models And CounterExamples.
 You can try Otter and MACE right now with
Son of BirdBrain.

Prototype software.

Automated Reasoning: Introduction and Applications,
a book by Wos, Overbeek, Lusk, and Boyle.

Automated Reasoning: 33 Basic Research Problems,
a book by Larry Wos.

The Automation of Reasoning: An Experimenter's Notebook with
OTTER Tutorial, a book by Larry Wos.

Automated Deduction in Equational Logic and Cubic Curves,
a monograph by W. McCune and R. Padmanabhan.

History of Automated Deduction at Argonne.
 A few
puzzles.
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
(mccune@mcs.anl.gov) or
Larry Wos (wos@mcs.anl.gov).
Some Related Links
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.