CFP: CADE-17 WORKSHOP ON AUTOMATION OF PROOFS BY MATHEMATICAL INDUCTION

To: types@cis.upenn.edu
Subject: CFP: CADE-17 WORKSHOP ON AUTOMATION OF PROOFS BY MATHEMATICAL INDUCTION
From: Carsten Schuermann <carsten+@cs.cmu.edu>
Date: Fri, 10 Mar 2000 09:32:59 -0500
CC: carsten@cs.cmu.edu
Organization: School of Computer Science, Carnegie Mellon University
Sender: carsten@postoffice.srv.cs.cmu.edu

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.

Regards
-- Carsten





       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

    http://www.cs.cmu.edu/~carsten/induction00

Send mail to

    challenge-request@twelf.org

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

    Carsten Schuermann
    Department of Computer Science
    Carnegie Mellon University
    5000 Forbes Ave.
    Pittsburgh, PA 15213-3891
    U.S.A.
    carsten@cs.cmu.edu

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