CICM 2014
General Program Chair
Local Arrangements Chair
Publicity and Workshop Chair
CICM 2014 - Conferences on Intelligent Computer Mathematics
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 Conferences on Intelligent Computer Mathematics (CICM) offer a venue for discussing these areas and their synergy.<br/> The 2014 conference is organized by Pedro Quaresma, takes place at University of Coimbra and consists of four tracks <ul> <li> Track A: Calculemus (chair: James Davenport)</li> <li>Track B: Digital Mathematical Libraries (DML) (chair: Petr Sojka)</li> <li>Track C: Mathematical Knowledge Management (MKM) (chair: Josef Urban)</li> <li>Track D: Systems & Projects (chair: Alan Sexton)</li></ul> The overall programme is organized by the General Program Chair Stephen Watt. The publicity chair is Serge Autexier.
2014-07-11
2014-07-07
University of Coimbra, Portugal
CICM-14 Calculemus Track
CICM-14 Digital Math Libraries Track
CICM-14 Doctoral Programme
CICM-14 Invited Talks
CICM-14 Mathematical Knowledge Management Track
CICM-14 Workshop Math User Interfaces
CICM-14 Workshop on The Notion of Proof
CICM-14 OpenMath Workshop
CICM-14 Track Systems and Projects
CICM-14 Theorem proving components for Educational software (ThEdu) Track
CICM-14 Work in Progress Track
A naive view of Homotopy Type Theory and its relation to the calculus of constructions
What international studies say about the importance and limitations of using computers to teach mathematics in secondary schools
Teaching Tiles
Towards Robust Hyperlinks for Web-Based Scholarly Communication
Computable data, mathematics, and digital libraries in Mathematica and Wolfram|Alpha
Towards the Formal Reliability Analysis of Oil and Gas Pipelines
A Tableaux Based Decision Procedure for Multi-Parameter Propositional Schemata
Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
Detecting unknots via equational reasoning, I: Exploration
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
Formalization of Complex Vectors in Higher-Order Logic
Hipster: Integrating Theory Exploration in a Proof Assistant
Mathematical structures enabling the decidability of the patentability and patent eligibility of a patent application
Search Interfaces for Mathematicians
A Data Model and Encoding for a Semantic, Multilingual Glossary of Mathematics
PDF/A-3u as an archival format for Accessible mathematics
Which one is better: presentation-based or content-based math search?
POS Tagging and its Applications for Mathematics
This paper has been awarded best DML paper prize
Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for Wikipedia
Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
Realms: A Structure for Consolidating Knowledge about Mathematical Theories
Mining State-Based Models from Proof Corpora
Matching concepts across HOL libraries
Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices
Flexary Operators for Formalized Mathematics
Interactive Simplifier Tracing and Debugging in Isabelle
Towards an Interaction-based Integration of MKM Services into End-User Applications
Towards Knowledge Management for HOL Light
Automated improving of proof legibility in the Mizar system
A Vernacular for Coherent Logic
An Approach to Math-Similarity Search
Semantics-Sensitive Math-Similarity Search
Digital Repository of Mathematical Formulae
NNexus Reloaded
E-books and Graphics with LaTeXML
System Description: MathHub.info
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description
System Description: A Semantics-Aware LaTeX-to-Office Converter
Math Indexer and Searcher Web Interface: Towards Fulfillment of Mathematicians' Information Needs
SAT-enhanced Mizar Proof Checking
A Framework for Formal Reasoning about Geometrical Optics
The SymbolicData Project - Towards a Computer Algebra Social Network
Mathematical Language Processing Project
Towards the Structure of Mathematical Proof
Certified proofs in programs involving exceptions
Formalizing a Named Explicit Substitutions Calculus in Coq
Reproducing a Geometric Working Session
Concepts and realisations of flexible exercise design and feedbackgeneration in an e-assessment system for mathematics
Design of Search Interfaces for Mathematicians
Author profile pages in zbMATH – improving accuracy through user
Visualization of Tangent Developables on a Volumetric Display
OpenMathMap: Interaction
FEncy: Spreadsheet Formulae Exploration
Developing visualisations for spreadsheet formulae: towards increasing the accessibility of science, technology, engineering and maths subjects
Firefox OS Web Apps for Science
Formula Collection Mobile Apps Realized by Teachers
Towards a Universal Interface for Real-Time Mathematical Communication
The eval symbol for axiomatising variadic functions
OpenMath Language Extensions
Extension Proposal: Records in Pragmatic OpenMath
Literate Sources for Content Dictionaries: a Progress Report
MMT Objects
Another Look at Formal Mathematical Properties
Short introduction by example to Coq and Formalising ZF ⊆ ZF_ε in Coq
Using Small-Step Refinement For Algorithm Verification In Computer Science Education
GCD — a Case Study on Lucas-Interpretation
Proof Auditing for Formalised Mathematics
Can Computer Proving Replace Traditional Proving?
Short introduction by example to Coq
The representation of mathematical proof through gestalt and metaphors
Quasigroups, Loops and Automated Deduction, or How I Learned To Stop Worrying and Start Letting Computers Prove Theorems
Extreme mathematics
Mathematical Document Classification via the Pachinko Allocation Model
Maths Information Retrieval for Digital Libraries
Content Based Formula Search
Formal Analysis of Reliability Block Diagrams
Formal Analysis of Geometrical Optics in HOL
Certification of programs with computational effects
Formalizing a named calculus modulo alpha-equivalence
Machine learning and computer algebra
Algebraic Algorithms for Numerical Semigroups
Extracted from the Conference Web site
CICM-14: General Information