Fwd: First call for papers CICM 2012 - Conference on Intelligent Computer Mathematics

Mathematical Knowledge Management and Digital Mathematical Library tracks
may be relevant. -Jodi

---------- Forwarded message ----------
From: Johan Jeuring <J.T.Jeuring@uu.nl>
Date: Tue, Nov 15, 2011 at 11:24 AM
Subject: First call for papers CICM 2012 - Conference on Intelligent
Computer Mathematics
To: J.T.Jeuring@uu.nl


        CICM 2012 - Conference on Intelligent Computer Mathematics
          July 9-13, 2012 at Jacobs University, Bremen, Germany

             http://www.informatik.uni-bremen.de/cicm2012/

                            Call for Papers
----------------------------------------------------------------

As computers and communications technology advance, greater
opportunities arise for intelligent mathematical computation. While
computer algebra, automated deduction, mathematical publishing and
novel user interfaces individually have long and successful histories,
we are now seeing increasing opportunities for synergy among these
areas. The Conference on Intelligent Computer Mathematics offers a
venue for discussing these areas and their synergy.

The conference will be organized by Serge Autexier and Michael
Kohlhase at Jacobs University in Bremen and consist of five tracks:

Artificial Intelligence and Symbolic Computation (AISC)
 Co-Chairs: John A. Campbell, Jacques Carette
Calculemus
 Chair: Gabriel Dos Reis
Digital Mathematical Libraries (DML)
 Chair: Petr Sojka
Mathematical Knowledge Management (MKM)
 Chair: Makarius Wenzel
Systems and Projects
 Chair: Volker Sorge

The overall programme will be organized by the General Program Chair
Johan Jeuring.

----------------------------------------------------------------
                            Important dates
----------------------------------------------------------------

Abstract submission:          20 February 2012
Submission deadline:          26 February 2012
Reviews sent to authors:     23 March 2012
Rebuttals due:                     30 March 2012
Notification of acceptance: 6  April 2012
Camera ready copies due:   20 April 2012
Conference:                         9-13 July 2012

----------------------------------------------------------------
                              Tracks
----------------------------------------------------------------

*** AISC ***

Symbolic computation can be roughly described as the study of
algorithms which operate on expression trees. Another way to phrase
this is to say that the denotational semantics of expressions trees is
not fixed, but is rather context dependent. Expression simplification
is probably the archetypal symbolic computation. Mathematically
oriented software (such as the so-called computer algebra systems)
have been doing this for decades, but not long thereafter, systems
doing proof planning and theorem discovery also started doing the
same; some attempts at knowledge management and 'expert systems' were
also symbolic, but less successfully so. More recently, many different
kinds of program analyses have gotten `symbolic', as well as some of
the automated theorem proving (SMT, CAV, etc).

But a large number of the underlying problems solved by symbolic
techniques are well known to be undecidable (never mind the many that
are EXP-time complete, etc). Artificial Intelligence has been
attacking many of these different sub-problems for quite some time,
and has also built up a solid body of knowledge. In fact, most
symbolic computation systems grew out of AI projects.

These two fields definitely intersect. One could say that in the
intersection lies all those problems for which we have no decision
procedures. In other words, decision procedures mark a definite phase
shift in our understanding, but are not always possible. Yet we still
want to solve certain problems, and must find 'other' means of
(partial) solution. This is the fertile land which comprises the core
of AISC.

Rather than try to exhaustively list topics of interest, it is
simplest to say that AISC seeks work which advances the understanding
of

Solving problems which fundamentally involve the manipulation of
expressions, but for which decision procedures are unlikely to ever
exist.


*** Calculemus ***

Calculemus is a series of conferences dedicated to the integration of
computer algebra systems (CAS) and systems for mechanised reasoning,
the interactive theorem provers or proof assistants (PA) and the
automated theorem provers (ATP). Currently, symbolic computation is
divided into several (more or less) independent branches: traditional
ones (e.g., computer algebra and mechanised reasoning) as well as
newly emerging ones (on user interfaces, knowledge management, theory
exploration, etc.) The main concern of the Calculemus community is to
bring these developments together in order to facilitate the theory,
design, and implementation of integrated systems for computer
mathematics that will routinely be used by mathematicians, computer
scientists and engineers in their every day business.

The topics of interest of Calculemus include but are not limited to:

       * Theorem proving in computer algebra (CAS)
       * Computer algebra in theorem proving (PA and ATP)
       * Case studies and applications that both involve computer
               algebra and mechanised reasoning
       * Representation of mathematics in computer algebra
       * Adding computational capabilities to PA and ATP
       * Formal methods requiring mixed computing and proving
       * Combining methods of symbolic computation and formal
                deduction
       * Mathematical computation in PA and ATP
       * Theory, design and implementation of interdisciplinary
               systems for computer mathematics
       * Theory exploration techniques
       * Input languages, programming languages, types and constraint
               languages, and modeling languages for mechanised
               mathematics systems (PA, CAS, and ATP).
       * Infrastructure for mathematical services

*** DML ***

Mathematicians dream of a digital archive containing all peer-reviewed
mathematical literature ever published, properly linked, validated and
verified.  It is estimated that the entire corpus of mathematical
knowledge published over the centuries does not exceed 100,000,000
pages, an amount easily manageable by current information
technologies. Following success of DML 2008, DML 2009 DML 2010, and
DML 2011 track objectives are to formulate the strategy and goals of a
global mathematical digital library and to summarize the current
successes and failures of ongoing technologies and related projects as
EuDML, asking such questions as:

       * What technologies, standards, algorithms and formats should
               be used and what metadata should be shared?
       * What business models are suitable for publishers of
               mathematical literature, authors and funders of their
               projects and institutions?
       * Is there a model of sustainable, interoperable, and
               extensible mathematical library that mathematicians
               can use in their everyday work?
       * What is the best practice for
               * retrodigitized mathematics (from images via OCR to
                        MathML or TeX);
               * retro-born-digital mathematics (from existing
                       electronic copy in DVI, PS or PDF to MathML or
                       TeX);
               * born-digital mathematics (how to make needed
                       metadata and file formats available as a side
                       effect of publishing workflow [CEDRAM/Euclid
                       model])?

*** MKM ***

Mathematical Knowledge Management is an interdisciplinary field of
research in the intersection of mathematics, computer science, library
science, and scientific publishing. The objective of MKM is to develop
new and better ways of managing sophisticated mathematical knowledge,
based on innovative technology of computer science, the Internet, and
intelligent knowledge processing. MKM is expected to serve
mathematicians, scientists, and engineers who produce and use
mathematical knowledge; educators and students who teach and learn
mathematics; publishers who offer mathematical textbooks and
disseminate new mathematical results; and librarians and
mathematicians who catalog and organize mathematical knowledge.

The conference is concerned with all aspects of mathematical knowledge
management. A non-exclusive list of important topics includes:

       * Representations of mathematical knowledge
       * Authoring languages and tools
       * Repositories of formalized mathematics
       * Deduction systems
       * Mathematical digital libraries
       * Diagrammatic representations
       * Mathematical OCR
       * Mathematical search and retrieval
       * Math assistants, tutoring and assessment systems
       * MathML, OpenMath, and other mathematical content standards
       * Web presentation of mathematics
       * Data mining, discovery, theory exploration
       * Computer algebra systems
       * Collaboration tools for mathematics
       * Challenges and solutions for mathematical workflows

*** Systems and Projects ***

The Systems and Projects track of the Conferences on Intelligent
Computer Mathematics is a forum for presentation of systems and new
and ongoing projects in all areas and topics related to the CICM
conferences:

       * AI and Symbolic Computation
       * Deduction and Computer Algebra
       * Mathematical Knowledge Management
       * Digital Mathematical Libraries

The track aims to provide an overview of the latest developments and
trends within the CICM community as well as to exchange ideas between
developers and introduce systems to an audience of potential users.

We solicit submissions for two page abstracts in the categories of
system descriptions and project presentations. System description
should present

       * newly developed systems,
       * systems that have not previously been presented to the CICM
                community, or
       * significant updates to existing systems.

Project presentation should describe

       * projects that are new or about to start,
       * ongoing projects that have not yet been presented to the
                CICM community.
       * significant new developments in ongoing previously presented
                projects.

All submissions should contain links to demos, downloadable systems,
or project pages. Availability of such accompanying material will be a
strong prerequisite for acceptance.

Accepted abstracts will be published in the CICM proceedings in
Springer's LNAI series. Author's are expected to present their
abstracts in 5-10 minute teaser talks followed by an open demo/poster
session. System papers must be accompanied by a system demonstration,
while project papers must be accompanied by a poster presentation.

----------------------------------------------------------------
                             Submitting
----------------------------------------------------------------

Submissions to tracks A to D must not exceed 15 pages and will be
reviewed and evaluated with respect to relevance, clarity, quality,
originality, and impact.  Shorter papers, e.g., for system
descriptions, are welcome. Authors will have an opportunity to respond
to their papers' reviews before the programme committee makes a
decision.

Submissions to the Systems & Projects track must not exceed four
pages. The accepted abstracts will be presented at CICM in a fast
presentation session, followed by an open demo/poster session. System
papers must be accompanied by a system demonstration, and project
papers must be accompanied by a poster presentation. The four pages of
the abstract should be new material, accompanied by links to
demos/downloads/project-pages and [existing] system descriptions.
Availability of such accompanying material will be a strong
prerequisite for acceptance.

Accepted conference submissions from all tracks will be published as a
volume in the series Lecture Notes in Artificial Intelligence (LNAI)
by Springer. In addition to these formal proceedings, authors are
permitted and encouraged to publish the final versions of their papers
on arXiv.org.

Work-in-progress submissions are intended to provide a forum for the
presentation of original work that is not (yet) in a suitable form for
submission as a full or system description paper. This includes work
in progress and emerging trends. Their size is not limited, but we
recommend 5 - 10 pages.

The programme committee may offer authors of rejected formal
submissions to publish their contributions as work-in-progress papers
instead. Depending on the number of work-in-progress papers accepted,
they will be presented at the conference either as short talks or as
posters. The work-in-progress proceedings will be published as a
technical report.

All papers should be prepared in LaTeX and formatted according to the
requirements of Springer's LNCS series (the corresponding style files
can be downloaded from
http://www.springer.de/comp/lncs/authors.html). By submitting a paper
the authors agree that if it is accepted at least one of the authors
will attend the conference to present it.

Electronic submission is done through easychair
(http://www.easychair.org/conferences/?conf=cicm2012).

----------------------------------------------------------------
                           Program Committees
----------------------------------------------------------------

General chair: Johan Jeuring (Utrecht University and Open Universiteit
the Netherlands)

AISC track
       John A. Campbell; University College London, UK; Co-chair
       Jacques Carette; McMaster University, Canada; Co-chair
      Serge Autexier; DFKI Bremen, Germany
      Jacques Calmet; University of Karlsruhe, Germany
      Jacques Fleuriot; University of Edinburgh, UK
      Andrea Kohlhase; International University Bremen, Germany
      Erik Postma; Maplesoft Inc., Canada
      Alan Sexton; University of Birmingham, UK
      Chung-chieh Shan; Cornell University, USA.
      Stephen Watt; University of Western Ontario, Canada

Calculemus track
       Gabriel Dos Reis; Texas A&M University, USA; Chair
       Andrea Asperti; University of Bologna, Italy
       Laurent Bernardin; Maplesoft, Canada
       James Davenport; University of Bath, UK
       Ruben Gamboa; University of Wyoming, USA
       Mark Giesbrecht; University of Waterloo, Canada
       Sumit Gulwani; Microsoft Research, USA
       John Harrison; Intel, USA
       Joris van der Hoeven; École Polytechnique, France
       Hoon Hong; North Carolina State University, USA
       Loïc Pottier; INRIA, France
       Wolfgang Windsteiger; RISC, Austria

DML track
       Petr Sojka; Masaryk University, Brno, CZ; Chair
        José Borbinha; Technical University of Lisbon,  PT
       Thierry Bouche; University Grenoble, FR
       Michael Doob; University of Manitoba, Winnipeg, CA
       Thomas Fischer; Goettingen University,  DE
       Yannis Haralambous; Télécom Bretagne, FR
       Václav Hlaváč; Czech Technical University, Prague, CZ
       Michael Kohlhase; Jacobs University Bremen, DE
       Janka Chlebíková; Portsmouth University, UK
       Enrique Maciás-Virgós; University of Santiago de Compostela,
         ES
       Bruce Miller; NIST, USA
       Jiří Rákosník; Academy of Sciences, Prague, CZ
       Eugenio Rocha; University of Aveiro, PT
       David Ruddy; Cornell University, US
       Volker Sorge; University of Birmingham, UK
       Masakazu Suzuki; Kyushu University, JP

MKM track
       Makarius Wenzel; University of Paris-South, France; Chair
       David Aspinall; University of Edinburgh, Scotland
       Jeremy Avigad; Carnegie Mellon University, USA
       Mateja Jamnik; University of Cambridge, UK
       Cezary Kaliszyk; University of Tsukuba, Japan
       Manfred Kerber; University of Birmingham, UK
       Christoph Lüth; DFKI Bremen, Germany
       Adam Naumowicz; University of Białystok, Poland
       Jim Pitman; University of California, Berkeley, USA
       Pedro Quaresma; Universidade de Coimbra, Portugal
       Florian Rabe; Jacobs University Bremen, Germany
       Claudio Sacerdoti Coen; University of Bologna, Italy
       Enrico Tassi; INRIA Saclay, France

Systems & Projects track
       Volker Sorge; University of Birmingham, UK; Chair
       Josef Baker; University of Birmingham, UK
       John Charnley; Imperial College, UK
       Manuel Kauers; RISC, Austria
       Koji Nakagawa; Kyushu University, Japan
       Piotr Rudnicki; University of Alberta, Canada
       Josef Urban; Radboud University Nijmegen, The Netherlands
       Richard Zanibbi; Rochester Institute of Technologies, USA

Received on Thursday, 9 February 2012 03:39:09 UTC