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

Friday, June 16
Room: Wean Hall 4623

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.

8:30-10:00: Higher-Order Inductive Theorem Proving (Chair: Deepak Kapur)

Brigitte Pientka, Carnegie Mellon University, USA
Jeremie Wajs, Pennsylvania State University, USA

10:00-10:30: Coffee Break

10:30-12:00: Inductive Theorem Provers and Formal Methods (Chair: Christoph Kreitz)

Dieter Hutter, DFKI, Germany
Deepak Kapur, University of New Mexico, USA

12:00-1:30: Lunch

1:30-3:30: Proof Planning and Program Transformation (Chair: Dieter Hutter)

Juergen Giesl, University of New Mexico, USA
Toby Walsh, University of York, England
Louise Dennis, University of Edinburgh, Scotland

3:30-4:00: Coffee Break

4:00-5:30: Challenges

Jeremey Gow, University of Edinburgh, Scotland
Dieter Hutter, DFKI, Germany


Carsten Schürmann Carnegie Mellon University
Andrew Ireland Heriot-Watt University
Deepak Kapur University of New Mexico
Christoph Kreitz Cornell University
Toby Walsh University of Strathclyde