Workshop on
Automation of Proofs by Mathematical Induction


Held in Connection with
The 17th International Conference on Automated Deduction
June 17-20, 2000
Pittsburgh, Pennsylvania, U.S.A.

  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 challenge" in the body (the header might stay empty) 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. All workshop attendees are expected to register for the CADE conference.

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

Carsten Schuermann
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

and the deadline for submitting experience reports is

June, 1st, 2000

Accepted contributions will be included in the workshop proceedings which will be available at the workshop and on the workshop web page.


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