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.
- 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 Counter-Examples.
- 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
- AAR,
the Association for Automated Reasoning
- CADE,
the Conference on Automated Deduction
- JAR,
the Journal of Automated Reasoning
-
The QED Project
-
Other theorem proving systems and groups
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.
gipoco.com
is neither affiliated with the authors of this page or responsible
for its contents. This is a safe-cache copy of the original web site.
gipoco.com
is neither affiliated with the authors of this page nor responsible
for its contents. This is a safe-cache copy of the original web site.