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.5 of 2003, september 27

Topics

Call for Papers

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

Integration of Computer Algebra Systems (CAS) and Automated Theorem Provers (ATP)
Symbolic Computation Aspects in Mechanized Reasoning
Mechanized Reasoning Aspects of Symbolic Computation Systems
Combination of Logical and Formal Methods with Computer Algebra
Connections between formal and informal approaches to mathematics
Design Issues for Logic and Symbolic Computing Systems
Constraint Solving Aspects in ATP/CAS
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:

Full research papers up to 12 pages describing original theoretical or applied research that has not been published elsewhere.
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. 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.

Call for Papers

The preliminary, first and second calls for papers.

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. After refereeing it was decided not to publish the special issue but informal proceedings are available.

Deadlines

Abstract Submission:	May 23, 2003
Submission Deadline:	May 30, 2003
Notification if acceptance:	June 26, 2003
Camera ready version:	July 15, 2003

Invited speakers

Thierry Coquand

James Davenport

Program Chairs

Program Committee

Andrea Asperti	Bologna, Italy
Henk Barendregt	Nijmegen, The Netherlands
Chris Benzmuller	Saarbruecken, Germany
Olga Caprotti	Risc Linz
James Davenport	Bath, United Kingdom
William 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