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:
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.