|
Automated Reasoning Systems
|
|
Automated reasoning is still in its infancy, but offers tremendous
promise for problem solving. Automated reasoning
assists with the deductive aspects of scientific problem solving. By spearheading the
development of such new technologies, MCS researchers have made Argonne world leaders in
both numerical and nonnumerical problem solving.
|
|
|
| AR Programs |
Our goal in automated reasoning is to develop techniques and to build
practical programs to help mathematicians, logicians, scientists, engineers, and others
with some of the deductive aspects of their work. Currently, we have three programs that
we use for different aspects of deductive reasoning.
- Otter, our most powerful
general-purpose automated deduction system, is designed to prove theorems stated in
first-order logic with equality. It can also be used as a symbolic calculator. Currently,
its main application is in abstract algebra and formal logic.
- EQP is an automated
theorem-proving program that searches for equational proofs. EQP performs especially well
on problems about lattice-like structures.
- MACE is a program that
searches for models and counterexamples.
|
|
|
| AR
Strategies and Inference Rules |
Key to sharply increasing the power of automated reasoning programs are
new strategies -- strategies to direct and strategies to restrict the reasoning. For over
three decades, MCS researchers have led the world in the formulation of new strategies
(such as the set of support strategy, weighting, and resonance). Equally important has
been the formulation of inference rules, with the objective of providing various types of
reasoning capability -- some focusing on but two hypotheses, for example, or focusing on
drawing conclusions free of logical "or". In all of our successful applications,
one or more strategies and inference rules have played a key role. |
|
|
| AR
Applications |
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. Most
recently, EQP was used to solve the Robbins problem -- a challenging
problem in Boolean algebra whose solution had eluded eminent mathematicians and logicians
for more than 60 years.Additionally, Otter
has been used to find new combinators in combinatory logic, single axioms for groups, new
axiomatizations for left and right calculi, and circles of pure proofs. |
