We now consider the longer-range opportunities and research directions of various areas of automated deduction. We begin with the verification area because of its application importance, the emergence of real application successes, and the number of projects in the research community for which verification is a major application.