CADE-15 Workshop on

STRATEGIES IN AUTOMATED DEDUCTION


July 5, 1998
Lindau, Germany


BACKGROUND

Strategies are almost ubiquitous in automated deduction and reasoning 
systems.  They describe, guide, and combine computations and
deductions in theorem proving environments, including automated
theorem provers, proof checkers, and logical frameworks.  Strategies
are used for various purposes, such as

  - proof search and proof planning,
  - restriction of search spaces,
  - specification of control components,
  - combination of different proof techniques and computation paradigms, 
  - meta-level programming in reasoning systems.

Deterministic computations or deductions based on inference rules are 
often insufficient to capture every computation or proof
development. A mechanism is needed, for instance, to sequentialize the
search for different solutions, to check context conditions, to
request user input to instantiate variables, to process subgoals in a
particular order, etc.  Strategies may involve iteration, case
analysis, or various forms of deterministic and non-deterministic
choices.  One may want to program strategies, transform them, or prove
properties on the computations or the proofs that they describe.

The workshop intends to foster the active exchange of ideas among
researchers interested in strategy-related topics. It continues 
the work and discussion of last year's CADE workshop on the same 
theme which were quite fruitful and promising. We plan to 
have a mixture of contributed talks, 1-2 invited speakers, ample time
for discussion, and, possibly, system demonstrations.


TOPICS OF INTEREST

Topics of interest for the workshop include all aspects related to
strategies in automated deduction, in particular:

  - strategy concepts and features in first- and higher-order, deductive 
    and inductive theorem proving systems and logical frameworks,
  - proof planning,
  - integration of strategies in existing proof systems,
  - strategy languages,
  - strategy analysis and properties of strategies,
  - applications and case studies where strategies play a major role.


SUBMISSIONS

Authors interested in presenting their work related to strategies are
invited to submit an extended abstract of up to 10 pages.  Researchers
interested in attending the workshop without giving a talk may send a
position paper of 1-2 pages describing their interest in the mentioned
topics.  All submissions should be sent to the organizers
(strategies98@logic.at) in postscript by May 15, 1998. Accepted
contributions will be included in the informal workshop proceedings
which will be available at the workshop and also on the www.

In order to keep the workshop reasonable in size, attendance is by
invitation only, based on the received submissions. However, depending
on the number of expected active participants, we will also consider
late requests for participation.  All workshop attendees are expected
to register for the main CADE-15 conference.

Additional updated information about the workshop is available under
the workshop web site. 


IMPORTANT DATES 

Submission deadline             May  15, 1998
Notification of acceptance      May  29, 1998
Final versions for proceedings  June 12, 1998                   
Workshop date                   July  5, 1998
CADE-15                         July 5-10, 1998


WORKSHOP ORGANIZERS          

Bernhard Gramlich                       Frank Pfenning
Inst. f. Computersprachen, TU Wien      Department of Computer Science, CMU
Resselg. 3/I/3, A-1040 Wien, Austria    Pittsburgh, PA 15213-3891, U.S.A.
phone:  +43 1 58801 4101                phone: +1 412 268 6343
fax:    +43 1 5041 589                  fax:   +1 412 268 5576 
e-mail: gramlich@logic.at               e-mail: fp@cs.cmu.edu
http://www.logic.at/staff/gramlich      http://www.cs.cmu.edu/~fp/ 


WORKSHOP WEB SITE

http://www.logic.at/staff/gramlich/cade15-ws-strategies.html

**********************************************************************