Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas.

CICM has been held annually as a joint meeting since 2008, co-locating related conferences and workshops to advance work in these subjects. Previous meetings have been held in Birmingham (UK 2008), Grand Bend (Canada 2009), Paris (France 2010), Bertinoro (Italy 2011), Bremen (Germany 2012), Bath (UK 2013), and Coimbra (Portugal 2014).

This is a call for papers for CICM 2015, which will be held in Washington, D.C., 13-17 July 2015.

The principal tracks of the conference will be:

    Calculemus (Symbolic Computation and Mechanised Reasoning)
    Chair: Jacques Carette
    DML (Digital Mathematical Libraries)
    Chair: Volker Sorge
    MKM (Mathematical Knowledge Management)
    Chair: Cezary Kaliszyk
    Systems and Data
    Chair: Florian Rabe
    Doctoral Programme
    Chair: Umair Siddique

Publicity chair is Serge Autexier. The local arrangements will be coordinated by the Local Arrangements Chairs, Bruce R. Miller (National Institute of Standards and Technology, USA) and Abdou Youssef (The George Washington University, Washington, D.C.), and the overall programme will be organized by the General Program Chair, Manfred Kerber (U. Birmingham, UK).

We will have proceedings of the conference as in previous years with Springer Verlag as a volume in Lecture Notes in Artificial Intelligence (LNAI).

As in previous years, it is anticipated that there will be a number co-located workshops, including one to mentor doctoral students giving presentations.

Track Calculemus: Symbolic Computation and Mechanised Reasoning

Calculemus is dedicated to the integration of computer algebra systems (CAS) and systems for mechanized reasoning such as interactive proof assistants (PA) and automated theorem provers (ATP). Currently, symbolic computation is divided into several (more or less) independent branches: traditional ones (e.g., computer algebra and mechanized reasoning) as well as emerging ones (on user interfaces, knowledge management, theory exploration, symbolic execution, abstract interpretation, etc.) We wish to bring these developments together in order to facilitate the theory, design, and implementation of integrated systems. These systems should be convenient to use routinely by mathematicians, computer scientists and all others who need computer-supported mathematics in their daily work.

All topics in the intersection of computer algebra systems and automated reasoning systems are of interest for Calculemus. These include but are not limited to:

    Automated theorem proving in computer algebra systems.
    Computer algebra and symbolic computation in theorem proving systems.
    Adding reasoning capabilities to computer algebra systems.
    Adding computational capabilities to theorem proving systems.
    Theory, design and implementation of interdisciplinary systems for computer mathematics.
    Case studies and applications that involve a mix of computation and reasoning.
    Case studies in formalization of mathematical theories that include non-trivial computations.
    Representation of mathematics in computer algebra systems.
    Theory exploration techniques.
    Combining methods of symbolic computation and formal deduction.
    Input languages, programming languages, types and constraint languages, and modeling languages for mathematical assistant systems.
    Homotopy type theory.
    Infrastructure for mathematical services.

Track DML: Digital Mathematical Libraries

Mathematicians dream of a digital archive containing all validated mathematical literature ever published, reviewed, properly linked, 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.

The track objective is to provide a forum for the development of math-aware technologies, standards, algorithms and formats for the fulfilment of the dream of a global digital mathematical library (DML). Computer scientists (D) and librarians of the digital age (L) are especially welcome to join mathematicians (M) and discuss many aspects of DML preparation.

Track topics are all topics of mathematical knowledge management and digital libraries applicable in the context of DML building, including the processing of mathematical knowledge expressed in scientific papers in natural languages:

    Math-aware text mining (math mining) and MSC classification
    Math-aware representations of mathematical knowledge
    Math-aware computational linguistics and corpora
    Math-aware tools for [meta]data and fulltext processing
    Math-aware OCR and document analysis
    Math-aware information retrieval
    Math-aware indexing and search
    Authoring languages and tools
    MathML, OpenMath, TeX and other mathematical content markup languages
    Web interfaces for DML content
    Mathematics on the web, math crawling and indexing
    Math-aware document processing workflows
    Archives of written mathematics
    DML management, business models
    DML rights handling, funding, sustainability
    DML content acquisition, validation and curation

Track MKM: Mathematical Knowledge Management

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 catalogue and organize mathematical knowledge.

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

Track: Systems and Data

The systems and data track provides a forum to publish digital resources whose value cannot be adequately represented by a printed paper alone. It aims at an exchange of ideas between developers and users in any area related to the CICM conferences.

Systems can be for example stand-alone; plugins, libraries, or extensions of existing systems; or integrations of existing systems. Data can be for example formalizations; harvests or new processing of existing data; or case studies, test cases, or benchmark suites for systems.

In either case, the primary evaluation criteria are the

    novelty,
    value, and
    usability,

of the system/data and the

    clarity of the accompanying paper (up to 4 pages).