Email Gateway (Aug 18 2022 at 19:13): Email Gateway (Aug 18 2022 at 19:13):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
I am not sure if the subsequent CFP made it on the list as intended. The
abstract deadline has passed already yesterday, but there is about one
more week left for the main submission deadline. Moreover, the PC chairs
have agreed to be flexible to accomodate late submissions.
Makarius
---------- Forwarded message ----------
Date: Fri, 17 Feb 2012 11:15:14 +0100
From: Johan Jeuring <J.T.Jeuring@uu.nl>
To: om@openmath.org, om-announce@openmath.org, poplmark@lists.seas.upenn.edu,
project-calculemus@lists.jacobs-university.de,
project-latexml@lists.jacobs-university.de,
projects-mkm-ig@jacobs-university.de,
project-omdoc@lists.jacobs-university.de, proofpower@lemma-one.com,
pvs@csl.sri.com
Subject: [MKM-IG] Conference on Intelligent Computer Mathematics,
last call for papers
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
[message truncated]
Last updated: Nov 21 2024 at 12:39 UTC