[SMT-LIB] CICM 2012: Last Call for Paper
Gabriel Dos Reis
gdr at integrable-solutions.net
Fri Feb 17 20:54:37 EST 2012
[ Apologies if you received multiple copies of this CFP. ]
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.
Invited talks will be given by:
Yannis Haralambous, Département Informatique, Télécom Bretagne
Conor McBride, Department of Computer and Information Sciences,
University of Strathclyde
Cezar Ionescu, Potsdam Institute for Climate Impact Research
----------------------------------------------------------------
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])?
DML is an opportunity to share experience and best practices between
projects in any area (MKM, NLP, OCR, pattern recognition, whatever)
that could change the paradigm for searching, accessing, and
interacting with the mathematical corpus. The track is
trans/interdisciplinary and contributions from any kind of people on
any aspect of the DML building are welcome.
*** 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; Ecole Polytechnique, France
Hoon Hong; North Carolina State University, USA
Loic Pottier; INRIA, France
Wolfgang Windsteiger; RISC, Austria
DML track
Petr Sojka; Masaryk University, Brno, CZ; Chair
Jose 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
Vaclav Hlava; Czech Technical University, Prague, CZ
Michael Kohlhase; Jacobs University Bremen, DE
Janka Chlebikova; Portsmouth University, UK
Enrique Macias-Virgos; University of Santiago de Compostela, ES
Bruce Miller; NIST, USA
JiÅ™i RakosnÃ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 Lueth; 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
Freek Wiedijk; Radboud University Nijmegen, The Netherlands
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
More information about the SMT-LIB
mailing list