"Grand Challenges for Automated Reasoning"
                Statement of Interest 
                   Stephan Schulz
          schulz@informatik.tu-muenchen.de

While there are many challenges and open questions in automated
reasoning, there are two I consider to be particularly interesting
(for me) and pressing (for the community).


Understanding the Search Space
------------------------------

Nearly 40 years have passed since Robinson's ground-breaking paper on
resolution and unification, and Otter, the earliest and probably still
most prominent of modern theorem provers, is about 15 years old. In
this time, hardware performance has increased by an incredible
factor. However, we are still performing proof search in essentially
the same way we did 15 or 20 years ago -- by locally evaluating simple
search alternatives. While refined calculi and better implementations
allow us to penetrate deeper, the basic problem of good search
strategies in an exponentially growing search space has not been
solved.

It is my belief that search strategies that offer more than a slow,
gradual improvement will need to be based on introspection, either via
the analysis of successful previous searches, or on the analysis of
certain global properties of the search state.


Breaking out of the Ghetto
--------------------------

Despite the many open research questions, automated reasoning systems
today are powerful enough for many interesting application. However,
there are two significant barriers for new users. First, users don't
know how to formalize their problems. Secondly, they don't know if the
effort of learning how to do it will pay off. Improving the power of
reasoning systems will increase the lure, but will still leave the
high initial outlay on the part of the user.

I believe another way of winning more application is the lowering of
the initial cost for potential users. There are large systems that
already are specified in a more or less formal way: Hare ware designs
in languages like Verilog and VHDL, and, of course, computer programs
in various programming languages. The AR community should work on
tools that allow us to automatically translate such specifications
into forms that make the application of automated reasoning tools to
prove relevant properties of designs and programs possible.