[om-a] 2nd CFP: The Role of Automated Deductionin Mathematics

[Simon Colton]

--------------------------------------------------------------------------

                     Second Call for Contributions

                             Workshop on

            The Role of Automated Deduction in Mathematics

                     (in conjunction with CADE-17)

                     CMU Pittsburgh, Pennsylvania, 
                         June 16 or 21, 2000

         http://www.dai.ed.ac.uk/~simonco/conferences/CADE00

[Apologies if you receive this more than once via different mailing lists]
--------------------------------------------------------------------------

Scope
-----
The   purpose of this  workshop is  to   discuss the role of automated
deduction in all  areas of mathematics. This  will  include looking at
the    interaction between  automated   deduction  programs  and other
computational systems  which have been  developed over recent years to
automate different  areas   of mathematical   activity. Such   systems
include computer   algebra    packages,  tutoring    programs, systems
developed  to help explore  a mathematical theory, and those developed
to help  present and archive  mathematical theories. The workshop will
also include discussions  of the use of  automated theorem  proving in
the wider  mathematical   community.  Presentations which detail   the
employment   of   automated deduction  techniques    in   any area  of
mathematical research are encouraged.

We are interested in the interaction of automated theorem proving
programs with:
(i)   computer algebra (CA) packages 
(ii)  constraint solvers 
(iii) model generators 
(iv)  tutoring systems 
(v)   interactive textbooks 
(vi)  theory formation programs and 
(vi)  mathematical databases. 

In all  these  fields automated deduction is   either already  used or
could be fruitfully employed  to enhance the  power and reliability of
existing  systems.  Particular  ongoing projects   include the use  of
deduction to certify CA systems, and also to enhance CA systems. Other
projects  include the  incorporation  of  deduction into  mathematical
tutoring systems and interactive mathematical textbooks and the use of
theory formation to help in automated theorem proving. The interaction
between  these programs   could  be in  terms of   improving automated
deduction  or in  terms of  using automated deduction  to improve  the
techniques employed by the other system.

The workshop  is intended to  inspire  the use of  automated deduction
within   other fields of mathematics  as  well as the incorporation of
techniques from other  fields  into automated deduction. The  workshop
will provide a forum for discussion  between researchers interested in
various aspects and  application areas of mathematics, with particular
emphasis on the role of automated deduction.


Submissions
-----------
Original workshop papers of up to 10 pages are solicited which discuss
the  interaction  of  automated    deduction and   other  mathematical
techniques, including, but not restricted to:

 -- computer algebra 
 -- constraint solvers 
 -- model generators 
 -- theory formation programs 
 -- mathematical tutoring systems 
 -- mathematical textbook systems 
 -- mathematical databases 

We hope to  attract papers discussing  the  theoretical frameworks for
such   integration  as      well   as papers  detailing     particular
implementations. Demonstrations of systems combining deduction systems
with other mathematical software will be particularly encouraged.

We also  hope  to attract  papers   discussing  the use  of  automated
deduction for mathematical research, including, but not restricted to:

 -- The use of automated theorem proving on particular problems from
    mathematics.

 -- The use of semi-automated deduction techniques in mathematics.

 -- Novel frameworks for the use of automated deduction within
    mathematics.

Submissions should be sent by email in Postscript format to

simonco at dai.ed.ac.uk 

Submissions should not exceed 10 pages. The deadline for submission is
April  1,  2000.  Authors of  accepted papers  are expected  to give a
presentation during the workshop.

Publication
-----------
Accepted submissions will  be collected in a  volume to be distributed
at the workshop. Additionally, the submissions  will be made available
on the web after the workshop.


Workshop Venue
--------------
The workshop will be held as  part of CADE  17 (The 17th International
Conference  on Automated Deduction),   June  17-20, 2000,  Pittsburgh,
Pennsylvania, USA.

See http://www.research.att.com/conf/cade/ for more information on
CADE 17.

Organizers
----------

      Simon Colton
            University of Edinburgh, Scotland
            simonco at dai.ed.ac.uk
            http://www.dai.ed.ac.uk/~simonco/
                  
      Ursula Martin
            University of St. Andrews, Scotland
            ursula at csl.sri.com
            http://www-theory.dcs.st-and.ac.uk/~um/
            
      Volker Sorge 
            University Saarbruecken, Germany
            sorge at ags.uni-sb.de
            http://www.ags.uni-sb.de/~sorge/

Important Dates
---------------

Deadline for submission:      1 April 2000
Notification of acceptance:   1 May 2000
Final version due:            20 May 2000
Workshop date:                16 or 21 June 2000

Further information
-------------------
Web sites:

Workshop Home Page     http://www.dai.ed.ac.uk/~simonco/conferences/CADE00
CADE 17 Workshops      http://www.ags.uni-sb.de/~kohlhase/event/cadews.html
CADE 17                http://www.research.att.com/conf/cade/

For further information on the workshop, please contact one of the
organizers.  

-----------------------------------------------------------------------------

--
om-announce at openmath.org  -  public announcements concerning OpenMath
Post discussion to om at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-announce-owner at openmath.org for assistance with any problems