ADEPT: A Heuristic Program for Proving Theorems of Group Theory

A computer program, named ADEPT (A Distinctly Empirical Prover of Theorems), has been written which proves theorems taken from the abstract theory of groups. Its operation is basically heuristic, incorporating many of the techniques of the human mathematician in a "natural" way. This program has proved almost 100 theorems, as well as serving as a vehicle for testing and evaluating special-purpose heuristics. A detailed description of the program is supplemented by accounts of its performance on a number of theorems, thus providing many insights into the particular problems inherent in the design of a procedure capable of proving a variety of theorems from this domain. Suggestions have been formulated for further efforts along these lines, and comparisons with related work previously reported in the literature have been made.

Lean Transition of Emerging Industrial Capability

This volume of the final report documents the technical work performed from December 1998 through December 2002 under Cooperative Agreement F33615-97-2-5153 executed between the U.S. Air Force, Air Force Research Laboratory, Materials and Manufacturing Directorate, Manufacturing Technology Division (AFRL/MLM) and the McDonnell Douglas Corporation, a wholly-owned subsidiary of The Boeing Company. The work was accomplished by The Boeing Company, Phantom Works, Huntington Beach, St. Louis, and Seattle; Ford Motor Company; Integral Inc.; Sloan School of Management in the Massachusetts Institute of Technology; Pratt & Whitney; and Central State University in Xenia, Ohio and in association with Raytheon Corporation. The LeanTEC program manager for AFRL is John Crabill of AFRL / MLMP and The Boeing Company program manager is Ed Shroyer of Boeing Phantom Works in Huntington Beach, CA. Financial performance under this contract is documented in the Financial Volume of the final report.