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))
Chairs:
13:00-14:30 Session 2: Automatic Theorem Proving and Machine Learning (I)
Regular papers
Chair:
| 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
Chair:
| 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
Chair:
| 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
Chair:
| 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
Chair:
| 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
Chair:
| 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
Chair:
| 16:30 | Formalization of RBD-based Cause Consequence Analysis in HOL (abstract) |
17:30-18:30 Session 9: Doctoral Programme (II)
Doctoral programme
Chair:
| 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
Chair:
| 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) PRESENTER: Asta Halkjær From |
14:30-15:00Coffee Break
15:00-16:00 Session 11: Invited Talk (III)
Invited speaker
Chair:
| 15:00 | Logic at work, and some research challenges for computer mathematics |
16:00-16:30Coffee Break
16:30-17:00 Session 12: Automatic Theorem Proving and Machine Learning (III)
Short papers
Chair:
| 16:30 | Improving Stateful Premise Selection withTransformers (abstract) |
| 16:45 | Inductive Benchmarks for Automated Reasoning (abstract) |
17:30-18:30 Session 13: Doctoral Programme (III)
Chair:
| 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
Chair:
| 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
Chair:
| 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
Chair:
| 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
Chair:
| 13:30 | Porting Mathlib (invited talk) (abstract) |
| 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
Chair:
| 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
Chair:
| 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) |
| 15:30 | Future of OpenMath (discussion) |
16:00-16:30Coffee Break
16:30-18:30 Session 20A: FMM2
Chair:
| 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
Chair:
| 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
Chair:
| 16:30 | Proactive Diagnosis of Traffic Safety: From Data to Formalization (Invited Talk) (abstract) |
| 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) |
18:30-19:15 Session 21: Towards Formal Mathematics Activities at International Research Institutes
A discussion on the possibility of organizing high-profile events for formal mathematics and knowledge management at Maths institutes.
We will use the FMM2 zoom room
Chair:
Saturday, July 31st
View this program: with abstractssession overviewtalk overview
14:00-16:00 Session 22A: FMM3
Chair:
| 14:00 | Fighting the Curse of De Bruijn (invited talk) (abstract) |
| 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 22B: NatFoM1
Chair:
| 14:00 | Assimilating the structure of formal and informal proof (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 23A: FMM4
Chair:
| 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 23B: NatFoM2
Chair:
| 16:30 | Formal Mathematics for the Masses (abstract) |
| 17:00 | sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents (abstract) |
| 17:30 | Semantic parsing of geometry statements using supervised machine learning on synthetic data (abstract) |