Automated deduction: Achievements and future directions

Abstract

Automated deduction (AD) is one of the most advanced and technically deep of the many technologies that constitute computer science. AD software performs tasks ranging from the fast simple deductions of a type checker and the efficient exploration of models, to fully automated deduction and complex deductive interactions in high-level languages. The field lies at an interface with mathematics, logic, and computing theory, as well as with practice. It has contributed fundamental ideas to these fields as well as drawing heavily from them. AD has spawned useful tools and systems, and offers great promise for making substantial progress on some of the most challenging problems in computer science and engineering—-such as how to improve the reliability of systems, how to build secure software, and how to increase productivity in software production. In the mathematics world some previously unsolved problems have been solved by or with the assistance of an AD system. We use the term AD for automated theorem provers, counterexample (model) generation , and consequence generators, in both fully automated and interactive systems. We note that AD systems may establish truth of a statement by means other than a formal proof (a listing of steps that are given or follow from previous steps), for example by a decision procedure such as computing and comparing terms in an equation. Likewise, disproofs are frequently counter examples.