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