CFP: CADE-17 WORKSHOP ON AUTOMATION OF PROOFS BY MATHEMATICAL INDUCTION
Type theories and logical frameworks have been shown to be appropriate
meta-languages for the representation of formal systems; therefore they
are of central importance for automated reasoning.
I am organizing a workshop on automation of proofs by mathematical
induction to be held in connection with CADE-17 in Pittsburgh, PA,
USA, where I plan an entire session on type theory and inductive
reasoning. Thus I would like to encourage members of the types
mailing list to contribute.
Here is the call for papers.
CADE-17 WORKSHOP ON
AUTOMATION OF PROOFS BY MATHEMATICAL INDUCTION
Pittsburgh, Pennsylvania, USA
16 or 21 June, 2000
SECOND CALL FOR PAPERS
Proof by Mathematical Induction presents the Automated Deduction
community with some very challenging research problems. The aim of
this one day workshop is to create an informal forum in which
hot-topics and emerging techniques can be presented and discussed.
The workshop will feature invited talks and contributed presentations
with ample time for discussion regarding topics like:
Inductive theorem proving and formal methods,
higher-order inductive theorem proving,
integrating inductive and high-performance theorem provers,
solutions to challenging problems.
Consistent with the workshop format, we expect and encourage
contributed talks to present work in progress, rather than polished
final results. In addition, we encourage system users to report on
their solutions to so called "challenges"; challenges are informal
problem descriptions which we distribute through a moderated mailing
list and the workshop web page
Send mail to
with "subscribe" in the header to subscribe to this mailing list.
Everybody is invited to submit challenges.
Attendance is by invitation only, based on the received submissions,
but we will consider late requests for participation.
Authors interested in presenting their work related to the workshop
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. Users interested in presenting their solution
to a challenge are invited to submit a 1 page experience report.
All submissions should be sent in postscript format to
Department of Computer Science
Carnegie Mellon University
5000 Forbes Ave.
Pittsburgh, PA 15213-3891
Electronic submissions are highly encouraged. The deadline for
submitting research and position papers is
April, 1st, 2000 (notification: May, 1st, 2000)
and the deadline for submitting experience reports is
June, 1st, 2000
Accepted contributions will be included in the workshop proceedings
will be available at the workshop and on the workshop web page.
ORGANIZING AND PROGRAMME COMMITTEE:
Carsten Schuermann Carnegie Mellon University
Andrew Ireland Heriot-Watt University
Deepak Kapur University of New Mexico
Christoph Kreitz Cornell University
Toby Walsh University of Strathclyde