CICM 2015
CICM 2015 - Conferences on Intelligent Computer Mathematics
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.
2015-07-17
2015-07-13
George Washington University New York, USA
General Program Chair
Local Arrangements Chair
Towards a Global Digital Mathematics Library
Math Search for the Masses: Multimodal Search Interfaces and Appearance-Based Retrieval
Mining the Archive of Formal Proofs
Formalizing mathematics using the Lean Theorem Prover
Towards Formal Fault Tree Analysis using Theorem Proving
Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Type Inference for ZFH
Generic Literals
Ranking/unranking of Lambda Terms with Compressed de Bruijn Indices
A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics
Structure Formation in Large Theories
Formal Logic Definitions for Interchange Languages
Math Literate Knowledge Management via Induced Material
Strategies for Parallel Markup
Readable Formalization of Euler's Partition Theorem in Mizar
Automating change of representation for proofs in discrete mathematics
Performance Evaluation and Optimization of Math-Similarity Search
Formalizing Physics: Automation, Presentation and Foundation Issues
Towards the Formalization of Fractional Calculus in Higher-order Logic
LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners
Mizar: State-of-the-art and Beyond
A Survey on Retrieval of Mathematical Knowledge
Growing the Digital Repository of Mathematical Formulae with Generic LaTeX Sources
TIP: Tons of Inductive Problems
Semantic Enrichment of Mathematics via `tooltips'
Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
Tools for MML Environment Analysis
Enabling Symbolic and Numerical Computations in HOL Light
Parsing Texts and Checking Proofs in LaTeX
Arithmetic in Metamath, Case Study: Bertrand's Postulate
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
A Web Environment for Geometry
Auto-hyperlinking the Stacks Project
The SMGloM Project and System
A web-based word processor with mathematical semantics
Math Chat in Collaborative Computer Algebra Shells
The OAF Project: An Open Archive of Formalizations
Isabelle Tutorial
Business Meeting
Literate Development of Families of Mathematical Models
Knowledge Management across Formal Libraries
Free and infinitely scalable advanced mathematics education
Formal Reliability Analysis using Higher-order Logic Theorem Proving
Change of representation in discrete mathematics
Visual Geometry Proofs in a Learning Context
Argumentative Effects of a Geometric Construction Tutorial System in Solving Problems of Proof
Creating Usable Computer Tools that Reason Mathematically
Mathtoys Demo
The large variety of form factors to view web pages and the proliferation of the pinch-to-zoom paradigm requires web-content to adapt both font sizes and reflow to the requirements of diverse displays and varying magnification. For specialist web content, such as mathematical formulas, this is not straight forward. We present a first approach to ``responsive equations'', a rendering method for MathML that adapts gracefully to small screens. The main idea is to reduce size of equations by abstracting over well-defined parts of formulas without obscuring the overall structure of an expression. We achieve this by embedding a semantic structure into the MathML representation underlying the rendering process and by collapsing mathematically meaningful sub-expressions.
Towards Meaningful Visual Abstraction of Mathematical Notation
Authorea is a collaborative platform for writing in research and education, with a focus on web-first, high quality scientific documents. We offer a tour through our integration of technologies that evolve math-rich papers into transparent, active objects. To enumerate, we currently employ Pandoc and LaTeXML (for authoring), MathJax (for math rendering and clipboard), D3.js (data visualization), iPython (computation), Flotchart and Bokeh (interactive plots). This paper presents the challenges and rewards of integrating active web components for mathematics, while preserving backwards-compatibility with classic publishing formats. We conclude with an outlook to the next-to-come mathematics enhancements on Authorea, and a technology wishlist for the coming year.
Live Mathematics in Authorea: Data, Computation and Visualization
Contemporary natural language processing (NLP) systems are based on corpora of annotated documents for training and evaluation. To extend NLP to documents from Science, Technology, Engineering, and Mathematics (STEM) we need annotation systems that can dealwith structured elements like mathematical formulae, tables, and possibly even diagrams. Current linguistic annotation systems treat documents as word sequences and disregard the structure of complex document elements, and are therefore unsuited for STEM annotation as this very structure carries important syntactic and semantic information. We present the KAT system, a browser-based annotation tool for linguistic/semantic annotations in structured (XHTML5, i.e. HTML + MathML + SVG in XML serialization) documents. As KAT is parametric in the annotation ontology and represents annotations as RDF, it can easily be integrated into RDF-based corpus management systems; we present an integration into the CorTeX system.
KAT: an Annotation Tool for STEM Documents
Visualization of knowledge is important to foster learning. Especially so in Mathematics where students have to understand not just the topic hand but also related concepts. It would therefore be ideal to have a simple way to find dependencies and present students with an easy way to catch up on topics they have not learned yet without losing context. Our research takes an existing annotated corpus and presents its contents while allowing students to see dependencies between topics and encouraging them to explore related mathematical concepts. Thus stu- dents can interactively learn the concepts the current topic depends on by taking small detours through those topics, should they need to refresh their memories. This approach to presenting learning materials changes how we interact with course materials and it is ultimately applicable to almost all areas in which knowledge needs to be transferred.
Relational Presentation Using Semantic Closeness
Our paper presents a research project of the didactics of mathematics and computer engineering in which solving problems is both a condition and a result of mathematical learning. We introduce the concept of connected problems as a means used by a teacher agent to relaunch a solving process among students when a blockage has been reached. Whilst our theoretical approach focuses on educational and cognitive interactions, we give special attention to the cKĀ¢ model of knowledge, the model of the mathematical working space and the concept of a zone of proximal development. In particular, we show how the notion of interaction connects theoretical and methodological challenges of the project.
Interactive management of problems in geometry for the development of student skills and the acquisition of mathematical knowledge
We are interested in the spreadsheet as a form of mathematical user interface and especially in the underlying human-spreadsheet interaction with respect to the target groups of readers and authors of spreadsheets. For understanding users' comprehension of a spreadsheet we looked into the context space, i.e., the space build up of information dimensions along which users try to grasp the presented content. Our recent research has shown that, on the one hand, there is a clear difference of the context space between spreadsheet readers and authors. On the other hand, spreadsheet complexity does not distinguish the users' context space. Here, we are looking even deeper into the elicited data to find out whether and if so, how context dimensions depend on each other. If there are significant differences between such co-occurrences with respect to user roles or complexity, then we can make use of the results to enhance user-assistance systems for spreadsheets.
Co-Occurrences of Context Dimensions of Spreadsheets
Invited talk: Learning to parse mathematics from aligned corpora
Understanding Mathematical Theory Formation via Theory Intersections in MMT
A symbolic approach to abstract algebra in HOL Light
A formalisation of metric spaces in HOL Light
Formalizing Divisibility Rules as a Student Case Study
GCH implies AC, a Metamath Formalization
Improving Legibility of Proof Scripts in Mizar
Publicity Chair
Calculemus Chair
DML Chair
Doctoral Program Chair
MathUI Chair
MKM Chair
SysData Chair
ThEdu Chair
CICM-15 Calculemus Track
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.
CICM-15 Digital Math Libraries Track
DML track is an opportunity to share experience and best practices between projects in many areas (MKM, NLP, OCR, IR, DL, pattern recognition,...) 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.
CICM-15 Doctoral Programme
The Doctoral Programme provides a dedicated forum for PhD students to present and discuss their ideas, ongoing or planned research, and achieved results in an open atmosphere. It will consist of presentations by the PhD students to get constructive feedback, advice, and suggestions from the research advisory board, researchers, and other PhD students. Each PhD student will be assigned to an experienced researcher from the research advisory board who will act as a mentor and who will provide detailed feedback and advice on their intended and ongoing research.
FMM - Formal Mathematics for Mathematicians
FMM is a new workshop affiliated with CICM 2015 intended to gather together mathematicians interested in computer assistance and researchers in formal and computer-understandable mathematics.
CICM-15 Invited Talks
MathUI 2015 - 10th Workshop on Mathematical User Interfaces
<p>MathUI is an international workshop to discuss how users can be best supported when doing/learning/searching for/interacting with mathematics using a computer.</p><ul><li>Is mathematical user interface design a design for representing mathematics, embedding mathematical context, or a specific design for mathematicians?</li><li>How is mathematics for which purpose best represented?</li><li>What specifically math-oriented support is needed?</li><li>Does learning of math require a platform different than other learning platforms? </li><li>Which mathematical services can be offered?</li><li>Which services can be meaningfully combined?</li><li>What best practices wrt. mathematics can be found and how can they be best communicated?</li></ul> <p>We invite all questions, that care for the use of mathematics on computers and how the user experience can be improved, to be discussed in the workshop.</p>
2015-07-13
2015-07-13
CICM-15 Mathematical Knowledge Management Track
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.
CICM-15 Projects and Surveys
CICM-15 Systems and Data Track
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.
ThEdu'15 - Theorem Provers Components for Educational Software
ThEdu is a forum to gather the research communities for computer Theorem Proving (TP), Automated Theorem Proving (ATP), Interactive Theorem Proving (ITP) as well as for Computer Algebra Systems (CAS) and Dynamic Geometry Systems (DGS). The goal of this union is to combine and focus systems of these areas and to enhance existing educational software as well as studying the design of the next generation of educational mathematical tools.
CICM-15 Tutorials
CICM-15 Work in Progress