**Automated Theorem Proving** (ATP) deals with the development of computer
programs that show that some statement (the *conjecture*) is a
*logical consequence* of a set of statements (the *axioms*
and *hypotheses*).
ATP systems are used in a wide variety of domains. For examples, a mathematician
might prove the conjecture that groups of order two are commutative, from
the axioms of group theory; a management consultant might formulate axioms
that describe how organizations grow and interact, and from those axioms
prove that organizational death rates decrease with age; a hardware developer
might validate the design of a circuit by proving a conjecture that describes
a circuit's performance, given axioms that describe the circuit itself;
or a frustrated teenager might formulate the jumbled faces of a Rubik's
cube as a conjecture and prove, from axioms that describe legal changes
to the cube's configuration, that the cube can be rearranged to the solution
state. All of these are tasks that can be performed by an ATP system, given
an appropriate formulation of the problem as axioms, hypotheses, and a
conjecture.

The **language** in which the conjecture, hypotheses, and axioms
(generically known as *formulae*) are written is a logic, often
classical 1st order logic, but possibly a non-classical logic and possibly
a higher order logic.
These languages allow a precise formal statement of the necessary
information, which can then be manipulated by an ATP system.
This formality is the underlying strength of ATP: there is no ambiguity
in the statement of the problem, as is often the case when using a natural
language such as English. Users have to describe the problem at hand precisely
and accurately, and this process in itself can lead to a clearer understanding
of the problem domain. This in turn allows the user to formulate their
problem appropriately for submission to an ATP system.

The **proofs** produced by ATP systems describe how and
why the conjecture follows from the axioms and hypotheses, in a manner
that can be understood and agreed upon by everyone, even other computer
programs. The proof output may not only be a convincing argument that the
conjecture is a logical consequence of the axioms and hypotheses, it often
also describes a process that may be implemented to solve some problem.
For example, in the Rubik's cube example mentioned above, the proof would
describe the sequence of moves that need to be made in order to solve the
puzzle.

**ATP systems** are enormously powerful computer programs, capable
of solving immensely difficult problems. Because of this extreme capability,
their application and operation sometimes needs to be guided by an expert
in the domain of application, in order to solve problems in a reasonable
amount of time. Thus ATP systems, despite the name, are often used by domain
experts in an interactive way. The interaction may be at a very detailed
level, where the user guides the inferences made by the system, or at a
much higher level where the user determines intermediate lemmas to be proved
on the way to the proof of a conjecture.
There is often a synergetic relationship between ATP system users and the
systems themselves:

- The system needs a precise description of the problem written in some logical form,
- the user is forced to think carefully about the problem in order to produce an appropriate formulation and hence acquires a deeper understanding of the problem,
- the system attempts to solve the problem,
- if successful the proof is a useful output,
- if unsuccessful the user can provide guidance, or try to prove some intermediate result, or examine the formulae to ensure that the problem is correctly described,
- and so the process iterates.

**Fields** where ATP has been successfully used include logic, mathematics,
computer science, engineering, and social science; some outstanding successes
are described below. There are potentially many more fields where ATP could
be used, including biological sciences, medicine, commerce, etc.
The technology is waiting for users from such fields.

The most exciting recent success in **mathematics** has been the
settling of the Robbins problem by the ATP system
EQP.
In 1933 Herbert Robbins conjectured that a particular group of axioms form
a basis for Boolean algebra, but neither he nor anyone else (until the
solution by EQP) could prove this. The proof that confirms that Robbins'
axioms are a basis for Boolean algebra was found October 10, 1996, after
about 8 days of search by EQP, on an RS/6000 processor. This result was
reported in the
New York Times.

In the mathematical domain of quasi-groups there have been several successes using ATP systems. Otter has been used by the mathematician Ken Kunen to prove several results in quasi-groups. Fujita, Slaney, and Bennett (the first two being ATP researchers, the last a mathematician) decided many quasi-group problems using a system built at ICOT in Japan. William McCune and colleagues have used Otter to find minimal axiom sets, find new single axioms, and solve other interesting problems, in a range of algebraic structures. The ATP system Waldmeister has been embedded into Mathmatica, extending Mathematica's already uniquely powerful algebraic theorem-proving capabilities. ATP has been used at Charles University to cross-verify the Mizar Mathematical Library. In the higher order setting NUPRL helped to confirm Higman's lemma and Gerard's paradox, both of which were under active investigation by humans at the time. The specialist geometry prover Geometry Expert, of Chou, Gao, and Zhang, has been used to obtain new results in Euclidean geometry.

**Software creation** is an economically important real world application
of ATP.
Although the use of ATP in software creation is in its infancy, there have
already been some interesting results.
The KIDS
system developed at Kestrel Institute has been used to derive scheduling
algorithms that have outperformed currently used algorithms.
KIDS provides intuitive, high level operations for transformational
development of programs from specifications.
The Amphion
project, sponsored by NASA, is used to determine appropriate subroutines
to be combined to produce programs for satellite guidance.
By encapsulating usable functionality in software components (e.g.,
subroutines, object classes), and then reusing those components, Amphion can
develop software of greater functionality in less time than human programmers,
with some assurance that the overall system is correct because it is built up
from trusted components
The
Certifiable Synthesis project at NASA goes even further, generating
code with annotations that can be used to extract ATP problems whose solution
ensures various safety properties of the code.

**Software verification** is an obvious and attractive goal, which
is slowly being realized using ATP technology.
Three examples are given here, while many more are indexed at the
Formal
Methods page.
The Karlsruhe
Interactive Verifier (KIV) was designed as an experimental platform
for interactive program verification at the University of Karlsruhe, and
has since been used to successfully verify a range of software applications.
These include some case studies of academic software, e.g., implementation
od set functions, tree and graph representation and manipulation, and
verification of a Prolog to WAM compiler.
The KeY Project in Europe
integrates formal software specification and verification into the industrial
software engineering processes.
The starting point is a commercial CASE tool, which is augmented by
capabilities for formal specification and verification.
The ultimate goal is to make the verification process transparent for the
user with respect to the informal object-oriented model.
PVS is a verification
system that has been used in various applications, including
diagnosis and scheduling algorithms for fault tolerant architectures, and
requirements specification for portions of the space shuttle flight control
system.
Escher Techologies is a company
that researches, develops and delivers tools for the efficient construction
of provably correct software for mission-critical, business-critical or
safety-critical systems.

**Hardware verification** is the largest industrial application of
ATP. IBM, Intel, and Motorola are among the companies that employ ATP technology
for verification.
A few good examples of the use of ATP systems for hardware
verification are listed here, while many more are indexed at the
Formal
Methods page.
The ACL2
system has been used to obtain a proof of the correctness of the floating
point divide code for AMD's PENTIUM-like AMD5K86 microprocessor, while
ANALYTICA has been used to verify a division circuit that implements the
floating point standard of IEEE.
PVS (mentioned above in the context
of software verification) has been used to verify a microprocessor for
aircraft flight control.
The RRL system has verified commercial size adder and multiplier circuits.
The HOL
system has been used at Bell Laboratories for hardware verification.
Nqthm
has been used to produce a mechanical proof of correctness of the FM9001
microprocessor.
Jasper Design Automation, Inc is a
company with a mission of making full formal IC verification a competitive
advantage for its customers.
The company’s flagship product, JasperGold Verification System, is the first
verification product to deliver systematic complete verification, and
accomplishes this task within predictable, finite schedule constraints.