Automated Deduction

In this article, the body of a report on automated deduction is presented that notes some significant achievements and takes a studied look at the future of the field. Mechanization of the deductive process includes not only proving new mathematical results by computer but also formally verifying the correctness of (certain properties of) computer chip designs and programs and even deducing the programs themselves from formal specifications of the task. A less obvious application is the use of automated inference tools within programming languages and within programs that produce scheduling algorithms and optimize other programs. Some of the early work in this field is already part of the fabric of the AI world. The machinery developed in this field is useful in inferring missing rules or facts in a problem specification (abduction) and generalizing from examples to full specifications (inductive inference, learning from examples), although I do not deal with these forms of reasoning in this article.