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.

  Home
  Call for papers
  Challenges
 
  

PRELIMINARY PROGRAMME
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

ORGANIZING AND PROGRAMME COMMITTEE:

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