-----------------------------------------------------------------
                Call for Participation
        IJCAR Workshop on the Automation of Proof by
                Mathematical Induction
                  June 18/19, 2001
                    Siena, Italy
        http://www.dai.ed.ac.uk/~louised/inductionws/
------------------------------------------------------------------

Mathematical induction is required for reasoning about objects or
events containing repetition, e.g. computer programs with
recursion or iteration, electronic circuits with feedback loops or
parameterized components. It is thus a vital ingredient of formal
methods techniques for synthesizing, verifying and transforming
software and hardware. The automation of induction proof
improves the capability of mechanical assistants for software and
hardware designers. It reduces the need for such designers to
be skilled in mathematical proof techniques and improves
their productivity by automating tedious and error-prone aspects
to their task in a formal software development.

Format of Workshop
==================
This is a one day workshop aimed at bringing together researchers in the
field.  Most of the sessions will be themed panel discussions. The
precise topics of these sessions will be finalised nearer the time.
Areas we are considering include but are not limited to:

* The combination of inductive theorem provers with decision
procedures and other reasoning components
* Program synthesis and transformation
* The use of induction in logical frameworks.

Participants are welcome to suggest other sessions that would be of
interest to them.

We plan to hold a session devoted to system descriptions.  We would
prefer system descriptions to consider the workshop challenge problems
(available from workshop home page and by email from workshop chair)
but will accept descriptions that do not.  Researchers are encouraged
to contribute problems to the challenge corpus.

If there is a demand we will consider a session dedicated to the
presentation of papers.

Participation and Submission Details
====================================
All researchers with an interest in the automation of proofs by
mathematical induction are welcome to attend the workshop.  Please
note that all attendees must register to IJCAR.

Researchers interested in attending the workshop are asked to submit a
short abstract or a position paper describing their current research
in the area or a system description of some relevant implementation
work they have performed.  Final versions of the submissions will be
soft bound into a volume of working notes for circulation at the
workshop.  It will be acceptable for one paper to cover several
participants who work in close conjunction with each other.  It will
also be acceptable for one participant to submit both a position paper
and a system description.  The purpose of these submissions is to
provide attendees with some background on each others' interests.

Participants are asked to indicate if they wish to present their
position paper or system description at the workshop.

Position papers and system descriptions should be emailed in to the
workshop chair.  Submissions should include both latex source and one
of DVI, Postscript or PDF output.  We would prefer submissions to
follow the LNCS Guidelines.

Important Dates
===============
Submission deadline: 31st March
Notification date: 15th April
Camera-ready deadline: 31st April
Workshop Date: 18th or 19th July
IJCAR: 20-23rd July


Contact
=======

Workshop Chair
--------------
Louise Dennis
Division of Informatics
University of Edinburgh
80 South Bridge
Edinburgh
EH1 1HN
United Kingdom
email: [log in to unmask]

Organising Committee
--------------------
Louise Dennis, University of Edinburgh, [log in to unmask]
Carsten Schuermann,  Yale University, [log in to unmask]
Juergen Giesl, University of Technology, Aachen,
[log in to unmask]