This is the final call for papers at a track of the FLAIRS-97
conference, to be held in Daytona Beach, Florida, May 10-14
1997. Please note the EXTENDED DEADLINE! This track follows the
successful track on controlling search in automated reasoning held at
FLAIRS-96. The subject of the 1997 track is, again, controlling
automated deduction systems, but this time with an emphasis on using
techniques from the AI literature to do so. We are particularly
interested in papers reporting empirical results using implemented
systems.  The papers are due on 9 October 1996, should be at most 10
double spaced pages.

All papers will be reviewed by at least three reviewers, from the
program committee, including W. Bibel, TH Darmstadt; P. Baumgartner,
U.  Koblenz-Landau; M. Fuchs, U.  Kaiserslautern; R. Goebel,
U. Alberta; C.  Goller, TU Munich; J. Horton, U. New Brunswick;
W. McCune, Argonne Nat.  Lab.; D. Plaisted, U. North Carolina;
S. Schulz, TU Munich; M.  Stickel, SRI; G. Sutcliffe, James Cook U.;
and C. Suttner, TU Munich.

All accepted papers will appear in the regular FLAIRS-97 proceedings. 

The Call for Papers appears below.  For full details, see the URL
        <A HREF="http://www.cs.unb.ca/profs/bspencer/flairs97-aim.html">http://www.cs.unb.ca/profs/bspencer/flairs97-aim.html</A> 
or in Europe
        <A HREF="http://www.uni-kl.de/AG-AvenhausMadlener/flairs97-aim.html">http://www.uni-kl.de/AG-AvenhausMadlener/flairs97-aim.html</A>

We hope you will consider participating in this year's track, especially
by submitting a paper.  

Sincerely,
        Bruce Spencer and Joerg Denzinger

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

        Using AI methods to control automated deduction

The success and usability of an automated theorem prover strongly
depends on its control of its inference rules. The gains one can
achieve by a better control of one's system can be even higher than
the gains provided by better implementation techniques or extensions
or restrictions of the underlying calculus. As in the case of human
beings, a good control requires the adequate use of various kinds of
knowledge. Consequently, automated theorem provers and their search
processes can highly profit =66rom methods and techniques for
knowledge-based systems developed in other areas of AI. Examples of
such methods that are currently under investigation are

- generation and use of knowledge bases supporting deduction systems
- classification techniques for proof tasks, proof problems, results and
  search states
- techniques for adapting deduction systems to a given problem
- learning from prior proof experiences
- planning of theorem proving attempts
- DAI methods for cooperation of deduction systems or search control
  mechanisms

This track shall provide a forum for researchers and developers of
deduction systems, both fully automated and interactive, that are
interested in concepts for better controlling the search of their
provers.  We especially encourage the submission of papers describing
deduction systems employing techniques from other fields of AI
together with empirical results or case studies.