CICM 2021: 14TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS
PROGRAM

Days: Monday, July 26th Tuesday, July 27th Wednesday, July 28th Thursday, July 29th Friday, July 30th Saturday, July 31st

Monday, July 26th

View this program: with abstractssession overviewtalk overview

12:45-13:00 Session 1: Opening of CICM 2021

Opening of CICM 2021

(Remark: All times mentioned in this program are in CEST (UTC+2))

13:00-14:30 Session 2: Automatic Theorem Proving and Machine Learning (I)

Regular papers

13:00
Online Machine Learning Techniques for Coq: A Comparison (abstract)
13:30
Towards Math-Term Disambiguation Using Machine Learning (abstract)
14:00
Heterogeneous Heuristic Optimisation and Selection for First-Order Theorem Proving (abstract)
14:30-15:00Coffee Break
15:00-16:00 Session 3: Invited Talk (I)

Invited speaker

15:00
Induction in Saturation-Based Reasoning
16:00-16:30Coffee Break
16:30-17:00 Session 4: Automatic Theorem Proving and Machine Learning (II) + Geometric Reasoning (I)

Regular papers

16:30
A Heuristic Prover for Elementary Analysis in Theorema (System Description) (abstract)
16:45
Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities (abstract)
17:30-18:30 Session 5: Doctoral Programme (I)

Doctoral programme

17:30
Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs (abstract)
18:00
Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics (abstract)
Tuesday, July 27th

View this program: with abstractssession overviewtalk overview

13:00-14:30 Session 6: Logic and Systems + Geometric Reasoning (II)

Regular papers

13:00
A Language with Type-Dependent Equality (abstract)
13:30
Generating Custom Set Theories with Non-Set Structured Objects (abstract)
14:00
A New Export of the Mizar Mathematical Library (abstract)
PRESENTER: Colin Rothgang
14:15
Gauss-lintel, an algorithm suite for chord diagrams exploration (abstract)
14:30-15:00Coffee Break
15:00-16:00 Session 7: Invited Talk (II)

Invited speaker

15:00
Doing Number Theory in Weak Systems of Arithmetic
16:00-16:30Coffee Break
16:30-17:00 Session 8: Formalization (I)

Regular papers

16:30
Formalization of RBD-based Cause Consequence Analysis in HOL (abstract)
17:30-18:30 Session 9: Doctoral Programme (II)

Doctoral programme

17:30
Deep Learning for Automated Theorem Proving (abstract)
18:00
Develop a mathematical e-dictionary and test it (abstract)
Wednesday, July 28th

View this program: with abstractssession overviewtalk overview

13:00-14:30 Session 10: Formalizations (II)

Regular papers

13:00
A Modular First Formalisation of Combinatorial Designs (abstract)
13:30
Beautiful Formalizations in Isabelle/Naproche (abstract)
14:00
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL (abstract)
14:30-15:00Coffee Break
15:00-16:00 Session 11: Invited Talk (III)

Invited speaker

15:00
Logic at work, and some research challenges for computer mathematics
16:00-16:30Coffee Break
17:30-18:30 Session 13: Doctoral Programme (III)
17:30
Formal Verification for Secure Hardware Systems (abstract)
18:00
Formal Probabilistic Risk Assessment using Theorem Proving Applied to Power Systems (abstract)
Thursday, July 29th

View this program: with abstractssession overviewtalk overview

13:00-14:30 Session 14: Teaching and Geometric Reasoning + Search and Classification (I)

Regular papers

13:00
Automated Generation of Exam Sheets for Automated Deduction (abstract)
13:30
Learning to solve geometric construction problems from images (abstract)
14:00
10 Years Later: The Mathematics Subject Classification and Linked Open Data (abstract)
14:15
WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code (abstract)
PRESENTER: Dávid Lupták
14:30-15:00Coffee Break
15:00-16:00 Session 15: Invited Talk (IV)

Invited speaker

15:00
Referential Semantics -- a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge
16:00-16:30Coffee Break
16:30-17:00 Session 16: Search and Classification (II)

Regular papers

16:30
Searching for mathematical formulas based on graph representation learning (abstract)
Friday, July 30th

View this program: with abstractssession overviewtalk overview

13:30-16:00 Session 18: FMM1
13:30
TBA (invited talk)
14:30
Computing the Border Array in Isabelle/HOL (abstract)
15:00
Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL (abstract)
15:30
A Formalization of the (Compositional) Z Property (abstract)
14:00-16:00 Session 19A: MathUI1
14:00
Monitoring the impact of teacher's intervention in inquiry-based mathematics learning with the use of dynamic geometry (abstract)
14:30
A Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking (abstract)
15:00
Scenarios of copy-and-paste of mathematical objects (abstract)
15:30
MioGatto: A Math Identifier-oriented Grounding Annotation Tool (abstract)
14:00-16:00 Session 19B: OpenMath
14:00
Databases of problems, algorithmic contests and Openmath
14:30
OpenMath-RDF: RDF encodings for OpenMath objects and Content Dictionaries (abstract)
15:00
Pattern matching for mathematical expressions with OpenMath (abstract)
16:00-16:30Coffee Break
16:30-18:30 Session 20A: FMM2
16:30
Formalization of Gambler’s Ruin Problem (abstract)
17:00
Formalizing Fibonacci Squares (abstract)
17:30
Formalization of Prime Representing Polynomial in Mizar (abstract)
18:00
Verified Optimization (work in progress) (abstract)
16:30-18:30 Session 20B: MathUI2
16:30
Sophize Markdown and Collaboration Interface (abstract)
17:00
Story based content structuring in MATh (abstract)
17:30
Dynamic User Interfaces via Incremental Knowledge Management (abstract)
18:00
ATLAS: Interactive and Educational Linear Algebra System Containing Non-Standard Methods (abstract)
16:30-18:30 Session 20C: FVPS
16:30
Proactive Diagnosis of Traffic Safety: From Data to Formalization (Invited Talk)
17:30
Formalization of Transform Methods in Higher-order Logic: A Survey (abstract)
18:00
Formal Verification of Single Dual Setting Overcurrent Directional Relay Based Line Protection Logic for Smart Grids (abstract)
Saturday, July 31st

View this program: with abstractssession overviewtalk overview

14:00-16:00 Session 21A: FMM3
14:00
TBA (invited talk)
15:00
Formalizing the Gromov-Hausdorff space (abstract)
15:30
Elements of Differential Geometry in Lean: A Report for Mathematicians (abstract)
14:00-16:00 Session 21B: NatFoM1
14:00
Semantic parsing of geometry statements using supervised machine learning on synthetic data (abstract)
14:30
Natural Typesetting of Naproche Formalizations (abstract)
15:00
The design of mathematical language (invited talk)
16:00-16:30Coffee Break
16:30-18:30 Session 22A: FMM4
16:30
Formalizing rotation number and its properties in Lean (abstract)
17:00
A Web Platform for Hosting the Mizar Mathematical Library (abstract)
17:30
Scalar actions in Lean's mathlib (abstract)
18:00
Automatically Generalizing Theorems Using Typeclasses (abstract)
16:30-18:30 Session 22B: NatFoM2
16:30
Formal Mathematics for the Masses (abstract)
17:00
sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents (abstract)
17:30
Assimilating the structure of formal and informal proof (abstract)