-----------------------------------------------------------------------

4th International Workshop on Strategies in Automated Deduction
                       (STRATEGIES 2001)

             held in conjunction with IJCAR 2001
             in Siena, Italy, June 18 / 19, 2001

-----------------------------------------------------------------------

                         INVITED TALK


                      Manual Strategies

                      by William McCune
            Mathematics and Computer Science Division
               Argonne National Laboratory, U.S.A.


                          Abstract

Argonne's various automated deduction programs are not interactive.
In some cases, the problem at hand is solved automatically in the
first attempt. More often, however, the user has to run a sequence of
searches, using data or insight from one search to adjust the strategy
for the next. We call these metastrategies "manual strategies", and we
are looking for methods to automate them.

The talk will consist primarily of examples of our manual strategies
with the goal of initiating discussions on frameworks for automation.
A simple example is to find a good limit on the size of clauses.  A
trivial solution is start with a small limit, and run a sequence of
searches with increasing limits.  A more interesting solution
(analogous to the manual strategy) is to start with a large limit and
dynamically adjust it during the search. 

One set of examples is on improving known proofs, in particular,
finding shorter proofs, proofs with shorter clauses, and proofs with
fewer variables.  Automating these strategies seems feasible, but we
don't yet have a good general view of the situation.

A second set of examples is on achieving well-behaved search.  The
manual strategies for these usually depend on intuition (e.g., "that's
silly, the program shouldn't be wasting time on that"), and automation
has been ad hoc. 

----------------------------------------------------------------------