CADE-15 workshop

Using AI methods in Deduction

Lindau, Germany
July 5-10, 1998


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 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:

Accepted Papers:


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!


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