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
- Recent work on
obtained with our programs.
a program that searches for proofs.
a program that searches for equational proofs.
a program that searches for Models And Counter-Examples.
- You can try Otter and MACE right now with
Son of BirdBrain.
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
Recent visitors and collaborators include
Johan G. F. Belinfante,
Maria Paola Bonacina,
For further information, contact
Larry Wos (firstname.lastname@example.org).
Some Related Links
These activities are projects of the
Mathematics and Computer Science Division
Argonne National Laboratory.