FLAIRS-97

Track: Using AI methods to control automated deduction

Daytona Beach, FL, USA
May 10-14, 1997

Note: Information on submission of final papers

The information that you need to prepare the final version of your paper can be found using the URL http://www.cis.ufl.edu/~ddd/FLAIRS/authors.html

Conference registration and airfare discount information may be found at the URL http://erau.db.erau.edu/~towhid/atlas.html

The camara ready copy or your paper is due by **March 17th**, to:

Douglas D Dankel II (ddd@cis.ufl.edu)
Program Chair, FLAIRS 97
Box 116120,
E301 CSE, C.I.S.E,
University of Florida
Gainesville, FL 32611-6120

Here is the list of papers accepted in this track:

Automatic Selection of Search-guiding Heuristics
Matthias Fuchs, U. Kaiserslautern
Case-based Reasoning for Automated Deduction
Marc Fuchs, TU Munich,
Matthias Fuchs, U. Kaiserslautern
A Translation of Model Elimination Proofs into a Structured Natural Deduction
Andreas Wolf, TU Munich
Incremental Proof Planning by Meta-Rules
Stefan Gerberding, TH Darmstadt,
Axel Noltemeier, Debis Systemhaus GEI, Darmstadt
Self-Modifying Theorem Provers
Dirk Fuchs, U. Kaiserslautern,
Marc Fuchs, TU Munich
Hierarchical Proof Planning Using Abstractions
Dieter Hutter, DFKI Saarbrücken
Analogy as a Control Strategy in Theorem Proving
Erica Melis, U. Saarbrücken,
Jon Whittle, U. Edinburgh
Proving Ground Completeness of Resolution by Proof Planning
Manfred Kerber, U. Birmingham,
Arthur Christian Sehn, U. Saarbrücken
Some Experiments on the Applicability of Folding Architecture Networks to Guide Theorem Proving
Stephan Schulz, TU Munich,
Christoph Goller, TU Munich,
Andreas Küchler, U. Ulm

Call For Papers in the Track:
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 from 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.

Critical Dates

Papers Due (electronic submission): October 9, 1996
Papers Due: October 9, 1996
Author Notificaton: December 1996
Camera Ready Copy Due: March 17, 1997
Conference Dates: May 10-14, 1997

Authors are encouraged to submit electronically by mailing an encoded compressed PostScript file to bspencer@unb.ca (instructions below). Submissions may also be physically mailed by sending four (4) copies to either of the Program Committee Co-Chairs (addresses below). In the case of physical submission, please send an e-mail message to bspencer@unb.ca containing the title, author name(s) and abstract. In the case of electronic submission, if there are any difficulties printing, the authors will be notified and should be prepared to resubmit via courier. Other submissions received after October 9 will not be considered.

All accepted papers will be published with the FLAIRS-97 proceedings. The submitted paper should not exceed 10 (ten) pages, double spaced. The final accepted version of the paper will be limited to five galley pages. Please include with your submission a separate page identifying where correspondence should be sent.

The Program Committee's decisions will be mailed in early December 1996. Authors of accepted papers will be expected to submit the final camera-ready copy of their full papers to the publisher by February 17, 1997.

Program Committee Co-Chairs

Bruce Spencer
Faculty of Computer Science
University of New Brunswick
P.O. Box 4400
Fredericton, New Brunswick
CANADA E3B 5A3
FAX: 506-453-3566
Phone: 506-453-4566
Email: bspencer@unb.ca
http://www.cs.unb.ca/profs/bspencer/home.html

Jörg Denzinger
Computer Science Department
University of Kaiserslautern
Postfach 3049
67653 Kaiserslautern
Germany
FAX: +49-631-205-3558
Phone: +49-631-205-2181
Email: denzinge@informatik.uni-kl.de
http://www-avenhaus.informatik.uni-kl.de/mitarbeiter/denzinger/

Program Committee

P. Baumgartner, U. Koblenz-Landau
W. Bibel, TH Darmstadt
M. Fuchs, U. Kaiserslautern
U. Furbach, U. Koblenz-Landau
R. Goebel, U. Alberta
C. Goller, TU Munich
J. Horton, U. New Brunswick
W. McCune, Argonne Nat. Lab.
D. Plaisted, U. North Carolina
J. Pelletier, U. Alberta
S. Schulz, TU Munich
M. Stickel, SRI
G. Sutcliffe, James Cook U.
C. Suttner, TU Munich