If one were to attempt a single image, phrase, or slogan for the focal point of future research in automated deduction, the best choice could be the word chosen by Larry Wos: strategies. We have already used this word to describe a range of technical innovations within deduction engineering, centered on the need to direct proof searches within highly restricted search spaces. One may also extend this notion to include better methods for induction hypotheses selection and to the construction of effective proof-planning paradigms, for example. We leave to the reader the review of the preceding sections to see the number of activities of importance that can be captured by a fluid notion of the concept strategies.
In this report we have listed some of the achievements of the automated deduction field and considered some future directions for the field. We have seen that practical applications are now appearing and that more are likely in the near future. The most grandiose applications, such as full program synthesis, the mechanized mathematician, or the general reasoning machine, are not yet within view, nor should we venture to state when they will arrive. However, such automated deduction applications clearly can and will be developed, and they will be enormously beneficial.