CICM 2021: 14TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS

This page contains an index consisting of author-provided keywords.

A
aaa	Logic at work, and some research challenges for computer mathematics
abstraction	Generating Custom Set Theories with Non-Set Structured Objects
Annotation tool	MioGatto: A Math Identifier-oriented Grounding Annotation Tool
ARQMath	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
artificial intelligence	Deep Learning for Automated Theorem Proving
asymptotics	Fighting the Curse of De Bruijn (invited talk)
Authoring tools	Scenarios of copy-and-paste of mathematical objects
automated exam generation	Automated Generation of Exam Sheets for Automated Deduction
automated geometry proving	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
automated reasoning	Inductive Benchmarks for Automated Reasoning Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics
automated reasoning in teaching	Automated Generation of Exam Sheets for Automated Deduction
automated theorem proving	Deep Learning for Automated Theorem Proving
automatic geometric reasoning	Learning to solve geometric construction problems from images
automatic theorem production	Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
automation	Automatically Generalizing Theorems Using Typeclasses
Axiomatic Systems	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
B
bbb	Logic at work, and some research challenges for computer mathematics
border array	Computing the Border Array in Isabelle/HOL
C
Calculation Tools	Scenarios of copy-and-paste of mathematical objects
Cause-Consequence Diagram	Formalization of RBD-based Cause Consequence Analysis in HOL
ccc	Logic at work, and some research challenges for computer mathematics
circle homeomorphisms	Formalizing rotation number and its properties in Lean
client
collaboration	Sophize Markdown and Collaboration Interface
Combinatorial Design Theory	A Modular First Formalisation of Combinatorial Designs
Combinatorics	A Modular First Formalisation of Combinatorial Designs
combinatorics on words	Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
communication vs. certification	Formal Mathematics for the Masses
Commutative diagrams	Natural Typesetting of Naproche Formalizations
Completeness	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
Complex Networks	Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs
Computational topology	Gauss-lintel, an algorithm suite for chord diagrams exploration
Computer Algebra	A Heuristic Prover for Elementary Analysis in Theorema (System Description)
computer vision	Learning to solve geometric construction problems from images
confluence	A Formalization of the (Compositional) Z Property
Copy-and-paste	Scenarios of copy-and-paste of mathematical objects
Coq proof assistant	A Formalization of the (Compositional) Z Property
Coreference resolution	MioGatto: A Math Identifier-oriented Grounding Annotation Tool
D
deep learning	Deep Learning for Automated Theorem Proving
definition extraction	Develop a mathematical e-dictionary and test it
Dependent Type Theory	Elements of Differential Geometry in Lean: A Report for Mathematicians
Development Tool	Dynamic User Interfaces via Incremental Knowledge Management
didactics	Develop a mathematical e-dictionary and test it
Differential Geometry	Elements of Differential Geometry in Lean: A Report for Mathematicians
Digital Mathematical Libraries	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
digital model to learn workflows in math	Story based content structuring in MATh
diophantine set	Formalization of Prime Representing Polynomial in Mizar
Disambiguation	Towards Math-Term Disambiguation Using Machine Learning
disciplined convex programming	Verified Optimization (work in progress)
Docker Virtualization	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
Dual setting directional overcurrent relay	Formal Verification of Single Dual Setting Overcurrent Directional Relay Based Line Protection Logic for Smart Grids
Dynamic documents	Natural Typesetting of Naproche Formalizations
dynamic geometry	Monitoring the impact of teacher's intervention in inquiry-based mathematics learning with the use of dynamic geometry
dynamic geometry software	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
dynamical systems	Formalizing rotation number and its properties in Lean
E
elpi	Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics
equality	A Language with Type-Dependent Equality
Euclidean planar geometry	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
EuDML	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
Event Tree	Formalization of RBD-based Cause Consequence Analysis in HOL
Experimental Mathematics	Gauss-lintel, an algorithm suite for chord diagrams exploration
experimental setup	A Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking
export	A New Export of the Mizar Mathematical Library
eye-tracking	A Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking
F
Fibonacci	Formalizing Fibonacci Squares
Fibonacci squares	Formalizing Fibonacci Squares
flexiformal mathematics	Formal Mathematics for the Masses
formal abstracts	Formal Mathematics for the Masses
formal logic	Formal Mathematics for the Masses
Formal Mathematics	Beautiful Formalizations in Isabelle/Naproche Natural Typesetting of Naproche Formalizations sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents Formal Mathematics for the Masses Elements of Differential Geometry in Lean: A Report for Mathematicians
formal methods	Formal Verification for Secure Hardware Systems Formal Probabilistic Risk Assessment using Theorem Proving Applied to Power Systems Formal Verification of Single Dual Setting Overcurrent Directional Relay Based Line Protection Logic for Smart Grids Formalization of Transform Methods in Higher-order Logic: A Survey
formal methods in math teaching	Story based content structuring in MATh
formal proof	Assimilating the structure of formal and informal proof Automatically Generalizing Theorems Using Typeclasses
formal proofs	A Formalization of the (Compositional) Z Property
formal system	A Language with Type-Dependent Equality
formal verification	Formal Verification for Secure Hardware Systems Formalization of Gambler’s Ruin Problem Verified Optimization (work in progress)
Formalisation	A Modular First Formalisation of Combinatorial Designs
Formalization	Beautiful Formalizations in Isabelle/Naproche Formalizing Fibonacci Squares Computing the Border Array in Isabelle/HOL Formalizing the Gromov-Hausdorff space Formalization of Transform Methods in Higher-order Logic: A Survey
formalized mathematics	A New Export of the Mizar Mathematical Library
formula embedding	Searching for mathematical formulas based on graph representation learning
foundations of mathematics	Generating Custom Set Theories with Non-Set Structured Objects
G
Gambler's Ruin Problem	Formalization of Gambler’s Ruin Problem
Game Engine	Dynamic User Interfaces via Incremental Knowledge Management
Gauss diagrams	Gauss-lintel, an algorithm suite for chord diagrams exploration
GeoGebra	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
geometric inequality	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
geometry	Semantic parsing of geometry statements using supervised machine learning on synthetic data
graph representation learning	Searching for mathematical formulas based on graph representation learning
Gromov-Hausdorff space	Formalizing the Gromov-Hausdorff space
Grounding of formulae	MioGatto: A Math Identifier-oriented Grounding Annotation Tool
group actions	Scalar actions in Lean's mathlib
H
here	Future of OpenMath (discussion)
Heuristic Optimisation	Heterogeneous Heuristic Optimisation and Selection for First-Order Theorem Proving
Heuristic Selection	Heterogeneous Heuristic Optimisation and Selection for First-Order Theorem Proving
Higher-Order Logic	Formalization of RBD-based Cause Consequence Analysis in HOL Formalization of Transform Methods in Higher-order Logic: A Survey
horn clauses	Formal Verification for Secure Hardware Systems
I
IDE front-ends
Implicit arguments	Natural Typesetting of Naproche Formalizations
inductive benchmarks	Inductive Benchmarks for Automated Reasoning
inductive data types	Inductive Benchmarks for Automated Reasoning
Informal Documents	sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents
informal proof	Assimilating the structure of formal and informal proof
information retrieval	Pattern matching for mathematical expressions with OpenMath
inquiry-based learning	Monitoring the impact of teacher's intervention in inquiry-based mathematics learning with the use of dynamic geometry
integers	Inductive Benchmarks for Automated Reasoning
interactive theorem proving	Generating Custom Set Theories with Non-Set Structured Objects Beautiful Formalizations in Isabelle/Naproche
Isabelle	A Modular First Formalisation of Combinatorial Designs
Isabelle/HOL	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL Computing the Border Array in Isabelle/HOL Fighting the Curse of De Bruijn (invited talk)
K
keywords	Future of OpenMath (discussion)
Knowledge Management	Dynamic User Interfaces via Incremental Knowledge Management OpenMath-RDF: RDF encodings for OpenMath objects and Content Dictionaries
L
lambda calculus	A Formalization of the (Compositional) Z Property
LaTeX	Towards Math-Term Disambiguation Using Machine Learning sTeX2.0 - A LaTeX-based Ecosystem for Semantic/Active Mathematical Documents
Lean	Formalizing Fibonacci Squares Scalar actions in Lean's mathlib Elements of Differential Geometry in Lean: A Report for Mathematicians Formalizing the Gromov-Hausdorff space Porting Mathlib (invited talk)
library	A New Export of the Mizar Mathematical Library
library maintainence	Automatically Generalizing Theorems Using Typeclasses
Linear Algebra	ATLAS: Interactive and Educational Linear Algebra System Containing Non-Standard Methods
linebreaking	A Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking
Linked OpenData	10 Years Later: The Mathematics Subject Classification and Linked Open Data
Locales	A Modular First Formalisation of Combinatorial Designs
LOD	10 Years Later: The Mathematics Subject Classification and Linked Open Data
log data of manipulation	Monitoring the impact of teacher's intervention in inquiry-based mathematics learning with the use of dynamic geometry
Logic Programming	Gauss-lintel, an algorithm suite for chord diagrams exploration
M
Machine Learning	Heterogeneous Heuristic Optimisation and Selection for First-Order Theorem Proving Towards Math-Term Disambiguation Using Machine Learning Improving Stateful Premise Selection withTransformers Online Machine Learning Techniques for Coq: A Comparison
markdown	Sophize Markdown and Collaboration Interface
math formula search	Searching for mathematical formulas based on graph representation learning
Math Information Retrieval	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
Math Web Search	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
Math-Term	Towards Math-Term Disambiguation Using Machine Learning
mathematical content structuring	Story based content structuring in MATh
Mathematical Documents	Scenarios of copy-and-paste of mathematical objects
Mathematical Equations	Towards Math-Term Disambiguation Using Machine Learning
mathematical expressions	A Conceptual Design for an Eye-Tracking Experiment on Formula Linebreaking
mathematical knowledge management	A Web Platform for Hosting the Mizar Mathematical Library
Mathematical language processing	MioGatto: A Math Identifier-oriented Grounding Annotation Tool
mathematical practice	Formal Mathematics for the Masses
mathematical programming	Verified Optimization (work in progress)
mathematical software	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
mathematics	Pattern matching for mathematical expressions with OpenMath
mathematics practitioner	Formal Mathematics for the Masses
Mathematics Subject Classification	10 Years Later: The Mathematics Subject Classification and Linked Open Data
mathlib	Scalar actions in Lean's mathlib Porting Mathlib (invited talk)
MathML	Scenarios of copy-and-paste of mathematical objects OpenMath-RDF: RDF encodings for OpenMath objects and Content Dictionaries
metamath	Sophize Markdown and Collaboration Interface
MIaS	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
Mizar	Formalization of Prime Representing Polynomial in Mizar
Mizar Mathematical Library	A Web Platform for Hosting the Mizar Mathematical Library
MMT	A New Export of the Mizar Mathematical Library Dynamic User Interfaces via Incremental Knowledge Management
Moodle	Monitoring the impact of teacher's intervention in inquiry-based mathematics learning with the use of dynamic geometry
MSC	10 Years Later: The Mathematics Subject Classification and Linked Open Data
N
Naproche	Natural Typesetting of Naproche Formalizations
natural language	Beautiful Formalizations in Isabelle/Naproche Assimilating the structure of formal and informal proof
Natural language processing	MioGatto: A Math Identifier-oriented Grounding Annotation Tool
Natural-style Proofs	A Heuristic Prover for Elementary Analysis in Theorema (System Description)
neural networks	Improving Stateful Premise Selection withTransformers
no	Future of OpenMath (discussion)
O
online course examination	Automated Generation of Exam Sheets for Automated Deduction
Online Learning	Online Machine Learning Techniques for Coq: A Comparison
OpenMath	Scenarios of copy-and-paste of mathematical objects Pattern matching for mathematical expressions with OpenMath OpenMath-RDF: RDF encodings for OpenMath objects and Content Dictionaries
P
pattern matching	Pattern matching for mathematical expressions with OpenMath
polymath	Sophize Markdown and Collaboration Interface
porting tools	Porting Mathlib (invited talk)
premise selection	Improving Stateful Premise Selection withTransformers
prime numbers	Formalization of Prime Representing Polynomial in Mizar
primitive word	Computing the Border Array in Isabelle/HOL
Probabilistic Model Checking	Formal Verification of Single Dual Setting Overcurrent Directional Relay Based Line Protection Logic for Smart Grids
Probability Theory	Formalization of Gambler’s Ruin Problem
proof assistant	A New Export of the Mizar Mathematical Library
Proof Assistants	Online Machine Learning Techniques for Coq: A Comparison Formal Mathematics for the Masses
proof automation	Fighting the Curse of De Bruijn (invited talk)
proof graph	Sophize Markdown and Collaboration Interface
Proof Mining	Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs
Proof Synthesis	Online Machine Learning Techniques for Coq: A Comparison
Propositional Logic	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
ProVerif	Formal Verification for Secure Hardware Systems
python
Q
QED manifesto	A Web Platform for Hosting the Mizar Mathematical Library
QED system
QEPCAD B	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
quotient types	A Language with Type-Dependent Equality
R
RDF	Pattern matching for mathematical expressions with OpenMath OpenMath-RDF: RDF encodings for OpenMath objects and Content Dictionaries
real quantifier elimination	Extending GeoGebra/realgeom with QEPCAD B to obtain proofs on geometric inequalities
Realizability conditions	Gauss-lintel, an algorithm suite for chord diagrams exploration
record types	A Language with Type-Dependent Equality
Reliability Block Diagram	Formalization of RBD-based Cause Consequence Analysis in HOL
reversal symmetry	Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
rotation number	Formalizing rotation number and its properties in Lean
rrr	Referential Semantics -- a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge
S
Satisfiability Checking	A Heuristic Prover for Elementary Analysis in Theorema (System Description)
Satisfiability Modulo Theories	A Heuristic Prover for Elementary Analysis in Theorema (System Description)
self-supervised learning	Searching for mathematical formulas based on graph representation learning
semantic parsing	Semantic parsing of geometry statements using supervised machine learning on synthetic data
Semantic Web	OpenMath-RDF: RDF encodings for OpenMath objects and Content Dictionaries
sequence-to-sequence model	Semantic parsing of geometry statements using supervised machine learning on synthetic data
Serious Games	Dynamic User Interfaces via Incremental Knowledge Management
set theory	Generating Custom Set Theories with Non-Set Structured Objects
Simple Knowledge Organisation System	10 Years Later: The Mathematics Subject Classification and Linked Open Data
simple type theory	Formal Mathematics for the Masses
SKOS	10 Years Later: The Mathematics Subject Classification and Linked Open Data
smart power grids	Formal Probabilistic Risk Assessment using Theorem Proving Applied to Power Systems
soft types	Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics
Software Engineering	Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs
solving geometric construction problems	Learning to solve geometric construction problems from images
sophize	Sophize Markdown and Collaboration Interface
Soundness	Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
sss	Referential Semantics -- a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge
Strassen	ATLAS: Interactive and Educational Linear Algebra System Containing Non-Standard Methods
structure	Assimilating the structure of formal and informal proof
structured data	Sophize Markdown and Collaboration Interface
Symbolic Computation	A Heuristic Prover for Elementary Analysis in Theorema (System Description)
symbolic security analysis	Formal Verification for Secure Hardware Systems
synthetic data	Semantic parsing of geometry statements using supervised machine learning on synthetic data
T
Tactical Learning	Online Machine Learning Techniques for Coq: A Comparison
tba1	Databases of problems, algorithmic contests and Openmath Proactive Diagnosis of Traffic Safety: From Data to Formalization (Invited Talk)
tba2	Databases of problems, algorithmic contests and Openmath Proactive Diagnosis of Traffic Safety: From Data to Formalization (Invited Talk)
tba3	Databases of problems, algorithmic contests and Openmath Proactive Diagnosis of Traffic Safety: From Data to Formalization (Invited Talk)
tbd1	The design of mathematical language (invited talk)
tbd2	The design of mathematical language (invited talk)
tbd3	The design of mathematical language (invited talk)
Teaching	ATLAS: Interactive and Educational Linear Algebra System Containing Non-Standard Methods
terminology	Develop a mathematical e-dictionary and test it
Theorem Provers	A Modular First Formalisation of Combinatorial Designs
Theorem Proving	Formalization of RBD-based Cause Consequence Analysis in HOL Online Machine Learning Techniques for Coq: A Comparison Structure in Theorem Proving: Analyzing and Improving the Isabelle Archive of Formal Proofs Formalizing Fibonacci Squares Formalization of Gambler’s Ruin Problem Formalization of Transform Methods in Higher-order Logic: A Survey
theory assistants	Formal Mathematics for the Masses
tool platform
Transform Methods	Formalization of Transform Methods in Higher-order Logic: A Survey
ttt	Referential Semantics -- a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge
type	A Language with Type-Dependent Equality
type-checking	Semantic parsing of geometry statements using supervised machine learning on synthetic data
typeclass diamonds	Scalar actions in Lean's mathlib
typeclasses	Automatically Generalizing Theorems Using Typeclasses Scalar actions in Lean's mathlib
Typesetting	Natural Typesetting of Naproche Formalizations
U
undefinedness	Reasoning Support for Undefinedness and Soft Typing in Formal Mathematics
Unity	Dynamic User Interfaces via Incremental Knowledge Management
User Experience	Dynamic User Interfaces via Incremental Knowledge Management
User Interfaces	Dynamic User Interfaces via Incremental Knowledge Management
V
verification	Formal Probabilistic Risk Assessment using Theorem Proving Applied to Power Systems
visual recognition	Learning to solve geometric construction problems from images
W
Web service	A Web Platform for Hosting the Mizar Mathematical Library
Web-Browsers	Scenarios of copy-and-paste of mathematical objects
WebMIaS	WebMIaS on Docker: Deploying Math-Aware Search in a Single Line of Code
X
xxx	Induction in Saturation-Based Reasoning Doing Number Theory in Weak Systems of Arithmetic
Y
yyy	Induction in Saturation-Based Reasoning Doing Number Theory in Weak Systems of Arithmetic
Z
Z property	A Formalization of the (Compositional) Z Property
zzz	Induction in Saturation-Based Reasoning Doing Number Theory in Weak Systems of Arithmetic

Disclaimer | Powered by EasyChair Smart Program