CADE-15 workshop

Using AI methods in Deduction

Lindau, Germany
July 5-10, 1998

Aim:

Standard automated theorem proving techniques often fail, when applied to difficult problems. To achieve success, researchers have found it necessary to use specific knowledge from different sources: knowledge about the problem to solve and the domain it stems from, knowledge about the calculus and its weak spots, and knowledge about the behaviour of the particular prover used and its problems. In the last years many approaches have been developed to put this knowledge into provers. Naturally, concepts from other areas of artificial intelligence that deal with acquiring, handling and using of knowledge influenced the proposed approaches. Examples of such concepts that are currently under investigation are

generation and use of knowledge bases supporting deduction systems
data mining techniques for analyzing prover behaviour
classification techniques for proof tasks, proof problems, results and search states
techniques for adapting deduction systems to a given problem
learning from previous proof experiences
theorem proving by proof planning
distributed artificial intelligence methods for cooperation of deduction systems or search control mechanisms
natural language understanding and generation for communicating with the user

This workshop is intended for researchers and developers of deduction systems, both fully automated and interactive, that are interested in the use of AI methods in their systems. Of special interest are papers describing deduction systems employing a concept given above or techniques from some other fields of AI together with empirical results or case studies.

Important Dates:

Papers Due: April 30, 1998
Author Notification: May 18, 1998
Camera-ready Copy Due: June 3, 1998
Workshop: July 6, 1998

Accepted Papers:

L. Cheikhrouhou, J. Siekmann:
Planning Diagonalization Proofs
L. Cheikhrouhou, V. Sorge:
Planning Equivalence Proofs
M. Fisher, A. Ireland:
Towards a Science of Reasoning through Societies of Proof Planning Age nts
D. Fuchs:
Processing Top-Down generated Subgoal Clauses in a Bottom-Up Prover
E. Melis:
Proof Planning for Limit Theorems
S. Schulz:
Term Space Mapping for DISCOUNT
A. Wolf:
Pre-Run Prover Strategy Optimization

Proceedings:

The submissions will be reviewed by the organizers and accepted contributions will be included into the workshop notes that will be made available at the workshop. All participants of the workshop have to register for the main conference!

Organizers

Jörg Denzinger, Computer Science Department, University of Kaiserslautern

Michael Kohlhase, Computer Science Department, Universität des Saarlandes, Saarbrücken

Bruce Spencer, Faculty of Computer Science, Univers ity of New Brunswick

This page is maintained by Jörg Denzinger

Last Change: 10/08/98

Jörg Denzinger,	Computer Science Department,	University of Kaiserslautern
Michael Kohlhase,	Computer Science Department,	Universität des Saarlandes, Saarbrücken
Bruce Spencer,	Faculty of Computer Science,	Univers ity of New Brunswick