I believe that CADE has been successful, and will continue to be so. There are many conferences that emphasize formalism and theory, but CADE is one place where results leading to better implementations of theorem provers are of central importance, regardless of their formal content.
Here are some of the directions I would like to see CADE moving in:
I want to strengthen the relationship of theorem proving to other research communities, such as logic, mathematics, artificial intelligence, algorithms, and theory. What reputation does theorem proving research have in these communities, and how are we viewed? What can be done to further our relationships with these communities? Theorem proving already has had some notable successes. The solution of the Robbins problem is one example. Verifying a microprocessor, and other substantial verifications, are other such achievements. One can also mention stimulating the development of Prolog and constraint logic programming. What additional achievements would give theorem proving added recognition in other areas of computer science? Perhaps we should formulate some goals for the field using input from other areas.
Another area of great practical importance is hardware verification, and perhaps there is more that we can do to contribute to it. Just facilitating interaction between the CADE community and the hardware verification community is worthwhile, as CADE has done in the past to some extent.
I think we need to do more thinking about which approaches to theorem proving are going to solve the basic problems of the field. We all do this individually, but perhaps more discussion of such issues would be beneficial.
We also need to address the level of funding of theorem proving research, and think about whether it is adequate, and what can be done to improve it if necessary. The recent report by Don Loveland is a good step in this direction.
We need to address the issue of multiple conferences devoted fully or partially to theorem proving research. I don't think this is necessarily a bad thing, and it may even be a good thing for the field. It might also be good to promote joint meetings of various theorem-proving related conferences.
I would like to discuss the possibility of permitting authors of papers submitted to CADE, to respond to referee reports before a final decision is made.
I am also interested in making CADE more democratic. The current system probably would not have come into existence at all had it not been for my efforts and the support of many other people. However, this system is a compromise. One possibility worth considering is to increase the number of trustees from six to nine. This makes it easier to be elected, encouraging people to run for office, and makes the trustees more representative by having more people. I am also interested in promoting openness and verifiability of CADE elections.
I would like to find out how CADE and the trustees are viewed by the members of the AAR, and what suggestions they have for modifying and improving CADE. Dealing with perceived grievances can help to strengthen CADE.
One procedure that might be useful is to post the agendas of the CADE business meeting on the web beforehand, so that CADE attendees can better prepare for them. Another possibility would be to post minutes of past business meetings on the web, for reference.
It would be good to promote communication between those working in the field of automated deduction. Perhaps a theorem proving "chat room" would help in this direction.
Another possibility is to post lecture notes and transparencies for theorem-proving related courses in a web depository to make the teaching of these courses easier.
It sometimes seems that many fields begin to emphasize formalism and lose their purpose. To help guard against this in theorem proving, it may be good to initiate a journal of empirical theorem proving, in which the only papers would be those that discuss implemented systems and ways to measure or improve their performance.
I believe that theorem proving should be regarded as of fundamental importance, as it deals with deduction, which is central to many areas of endeavor. I think that this field has a tremendous future, and will make significant contributions to computer science and other areas. Let's work together to make this area, and CADE, a continuing success.