----------------------------------------------------------------
We apologize if you receive multiple copies of this message.
----------------------------------------------------------------

          Calculemus 2003

       11th Symposium on the Integration of
  Symbolic Computation and Mechanized Reasoning
       In conjunction with TPHOLs 2003 and TABLEAUX 2003

       Roma Italy -- September 10-12, 2003
         Version 1.1 of 2003, January 30

About this conference series

This is the eleventh symposium in a series which started with three meetings
in year 1996, two meetings in 1997 and then turned to a yearly event in
1998. It has become tradition to hold the meeting jointly with an event in
either symbolic computation or automated deduction. This year's symposium is
in conjunction with Theorem Proving and Higher Order Logics (TPHOL 2003) and
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX
2003).
The aim of the symposium is to bring together researchers interested in both
symbolic computation and mechanized reasoning.
It has been recognized that the integration of computing and deduction would
enhance the power of mathematical software systems. However it is not yet
clear which is the right way to achieve such an integration. The symposium
provides a forum for discussing and investigating the various approaches
possible including integration of reasoning into computer algebra systems,
integration of efficient computations in theorem provers, and frameworks,
languages, or protocols for integrating both symbolic computation and
mechanized reasoning.
Other topics of interest include the integration of constraint solving
techniques into both theorem provers and computer algebra systems,
environments for hybrid mathematical systems and systems for explorative
mathematics.


Indicative topics


   o Integration of Computer Algebra Systems (CAS) and Automated Theorem
     Provers (ATP)
   o Symbolic Computation Aspects in Mechanized Reasoning
   o Mechanized Reasoning Aspects of Symbolic Computation Systems
   o Combination of Logical and Formal Methods with Computer Algebra
   o Connections between formal and informal approaches to mathematics
   o Design Issues for Logic and Symbolic Computing Systems
   o Constraint Solving Aspects in ATP/CAS
   o Case studies and applications.

Other topics within the above manifesto are also welcomed.
This year's conference will emphasize on heuristics in computer algebra
algorithms. How to integrate them in the algorithm specification.


Submission Details

Authors are invited to submit papers in the following categories:

   o Full research papers up to 12 pages describing original theoretical or
     applied research that has not been published elsewhere.
   o Position Papers of up to 5 pages describing new systems, significant
     upgrades of existing ones or experiments made inside systems.

Submitted papers should be prepared following the LNCS guidelines and
submitted preferabily through the conference Web Page

http://www-calfor.lip6.fr/~rr/Calculemus03/

We strongly encourage the author(s) to use LaTeX. Authors of
accepted papers and system descriptions are expected to present their
contribution at the symposium. Authors of system descriptions are further
expected to demonstrate their systems.



Program Committee

                      
 Andrea Asperti  (Bologna, Italy)    
 Henk Barendregt  (Nijmegen, The Netherlands)     
 Chris Benzmuller  (Saarbruecken, Germany)    
 Olga Caprotti          
 James Davenport  (Bath, United Kingdom)    
 William M. Farmer     (McMaster, Canada)
 Hoon Hong             (North Carolina State, United States)
 Fairouz Kamareddine   (Heriot-Watt Edimburg, Scotland)
 Michael Kohlhase      (CMU, United States)
 Steve Linton          (St. Andrews, Scotland)
 Loic Pottier          (INRIA Nice, France)
 Roberto Sebastiani    (Trento, Italy)
 Volker Sorge          (Birmingham, United Kingdom)
 Thomas Sturm          (Passau, Germany)
 Stephen Watt          (ORCCA, Canada)
 Wolfgang Windsteiger  (RISC-Linz, Austria)
                      

Local Organizing Committee

                  Marta Cialdea Mayer                       
                  Dipartimento di Informatica e Automazione 
                  Via Vasca Navale, 79                      
                  00146 Roma (Italia)                       
                                                            
                  tel +39-06-55173232                       
                  fax +39-06-5573030                        


Deadlines


                                           
 Submission Deadline:        May 23, 2003  
 Notification if acceptance: June 16, 2003 
 Camera ready version:       July 8, 2003  
                                           
Proceedings

Papers submitted to the symposium undergo a standard review process. Accepted
research papers and system descriptions will be published in the Symposium's
informal proceedings and as a research report of Laboratoire D'Informatique de
Paris 6.
The full paper versions of the very best papers will be considered for
publication in the London Mathematical Society's Journal of Computation and
Mathematics. The Editor-in-Chief of the Journal has joined the Program
Committee to facilitate this process.

Addresses

e-mail: calculemus2003@calfor.lip6.fr

URL:  http://www-calfor.lip6.fr/~rr/Calculemus03/  

Surface mail:

     CALCULEMUS'2003
     Therese Hardin
     LIP6-UPMC
     8 rue du Capitaine Scott
     F-75015 Paris (France)

Phone number: +33-1-4427-7369
Fax number: +33-1-4427-8878

     CALCULEMUS'2003
     Renaud Rioboo
     LIP6-UPMC
     8 rue du Capitaine Scott
     F-75015 Paris (France)

Phone number: +33-1-4427-3341
Fax number: +33-1-4427-8878