Intelligent Computer Mathematics: 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings

Preface
Organization
Invited Talks
Logics at Work, and Some Challenges for Computer Mathematics
Induction in Saturation-Based Reasoning
Doing Number Theory in Weak Systems of Arithmetic
Contents
Formalizations
A Modular First Formalisation of Combinatorial Design Theory
	1 Introduction
	2 Background
		2.1 Mathematical Background
		2.2 Isabelle and Locales
	3 The Basic Design Formalisation
		3.1 Pre-designs
		3.2 Basic Design Properties
		3.3 Basic Design Operations
	4 The Block Design Hierarchy
		4.1 Restricting Block Size
		4.2 Balanced Designs
		4.3 T-Designs
		4.4 Uniform Replication Number
		4.5 BIBDs and Proofs
		4.6 BIBD Extensions
	5 Extending the Formalisation
		5.1 Resolvable Designs
		5.2 Group Divisible Designs
		5.3 Design Isomorphisms
		5.4 Graph Theory
	6 The Modular Approach
		6.1 The Formal Design Hierarchy
		6.2 The Little Theories Approach
		6.3 Notational Benefits
		6.4 Reasoning on Locales
		6.5 Limitations
	7 Conclusion and Future Work
	References
Beautiful Formalizations in Isabelle/Naproche
	1 Introduction
	2 Naproche, ForTheL, and LaTeX
	3 Example: Cantor\'s Theorem
	4 Example: König\'s Theorem
	5 Example: Euclid\'s Theorem
	6 Example: Furstenberg\'s Topological Proof
	7 Example: The Knaster–Tarski Theorem
	8 Outlook
	References
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL
	1 Introduction
	2 Related Work
	3 Implication and Falsity
		3.1 Language
		3.2 Wajsberg 1937
		3.3 Wajsberg 1939
		3.4 Shortest Axiom
	4 Disjunction and Negation
		4.1 Language
		4.2 Rasiowa 1949
		4.3 Russell 1908 and Bernays 1926
		4.4 Whitehead and Russell 1910
	5 Challenges and Benefits
	6 Conclusion
	References
Formalization of RBD-Based Cause Consequence Analysis in HOL
	1 Introduction
	2 Preliminaries
		2.1 RBD Formalization
		2.2 ET Formalization
	3 Cause-Consequence Diagram Formalization
		3.1 Formal CCD Modeling
		3.2 Formal CCD Analysis
	4 Conclusion
	References
Automatic Theorem Proving and Machine Learning
Online Machine Learning Techniques for Coq: A Comparison
	1 Introduction
		1.1 Contributions
	2 Tactic and Proof State Representation
	3 Prediction Models
		3.1 Locality Sensitive Hashing Forests for Online k-NN
		3.2 Online Random Forest
		3.3 Boosted Trees
	4 Experimental Evaluation
		4.1 Split Evaluation
		4.2 Chronological Evaluation
		4.3 Evaluation in Tactician
		4.4 Feature Evaluation
	5 Related Work
	6 Conclusion
	References
Improving Stateful Premise Selection with Transformers
	1 Introduction
	2 Data
	3 Experiments
	4 Conclusion and Future Work
	References
Towards Math Terms Disambiguation Using Machine Learning
	1 Introduction
	2 Related Works
		2.1 The DLMF Dataset
		2.2 Part-of-Math Tagger
		2.3 Word Sense Disambiguation in NLP
		2.4 Machine Learning Models
		2.5 Math Language Processing
	3 The Dataset
	4 Machine Learning Approach
		4.1 Data Prepossessing
		4.2 Feature Engineering
		4.3 Training the Models
		4.4 Evaluation Metric
	5 Results
		5.1 Gamma
		5.2 Prime
		5.3 Superscript
	6 Conclusion and Future Work
	References
Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving
	1 Introduction
	2 Hyper-Parameter Optimisation
	3 Heterogeneous Heuristic Optimisation and Scheduling
	4 Heuristic Optimisation for Heterogeneous Instances
		4.1 Dynamic Evaluation Clustering
		4.2 Local Heuristic Optimisation
		4.3 Embedding Unsolved Problems
	5 Local Schedules for Heterogeneous Instances
	6 Schedule Selection
	7 Experimental Evaluation
		7.1 Discovering New Heuristics
		7.2 Revealing Homogeneity with Admissible Evaluation Clustering
		7.3 Embedding Evaluation Features
		7.4 Optimal Scheduling of Heuristics
		7.5 Overall Performance Contribution
	8 Conclusion
	References
Inductive Benchmarks for Automated Reasoning
	1 Introduction
	2 Benchmark Format
	3 Benchmark Categories
		3.1 dty - Benchmarks with Inductively Defined Data Types
		3.2 int - Benchmarks with Integers
	4 Conclusions
	References
A Heuristic Prover for Elementary Analysis in Theorema
	1 Introduction
	2 Application of Special Techniques
	3 Conclusion and Further Work
	References
Search and Classification
Searching for Mathematical Formulas Based on Graph Representation Learning
	1 Introduction
	2 Related Work
	3 Graph Representation for Mathematical Formula
	4 Formula Embedding Model
		4.1 Self-supervised Learning Tasks
		4.2 Graph Neural Networks
		4.3 Hyperparameter Choices
	5 Experiments and Evaluation
		5.1 Evaluation Metric
		5.2 Evaluation Results
	6 Conclusion and Future Work
	References
10 Years Later: The Mathematics Subject Classification and Linked Open Data
	1 Introduction
	2 MSC 2020 SKOSification
		2.1 Reasons for a New Version
	3 Conclusion and Future Work
	References
WebMIaS on Docker
	1 Introduction
	2 Deployment Process Description
	3 Evaluation
	4 Conclusion
	References
Teaching and Geometric Reasoning
Learning to Solve Geometric Construction Problems from Images
	1 Introduction
	2 Related Work
	3 Our Euclidea Geometric Construction Environment
	4 Supervised Visual Learning Approach
		4.1 Action to Mask: Generating Training Data
		4.2 Mask to Action: Converting Output Masks to Euclidea Actions
		4.3 Solving Construction Problems by Sequences of Actions
		4.4 Additional Components of the Approach
	5 Solving Unseen Geometric Problems via Hypothesis Tree Search
		5.1 Generating Action Hypotheses
		5.2 Tree Search for Exploring Construction Hypotheses
	6 Experiments
		6.1 Benefits of Different Components of Our Approach
		6.2 Evaluation of the Supervised Learning Approach
		6.3 Evaluation on Unseen Problems
		6.4 Qualitative Example
	7 Conclusion
	References
Automated Generation of Exam Sheets for Automated Deduction
	1 Motivation
	2 Random Problem Generation
		2.1 Boolean Satisfiability (SAT)
		2.2 Non-ground Superposition with Redundancy
	3 Random Variation of Problem Templates
		3.1 Satisfiability Modulo Theories (SMT)
		3.2 Ground Superposition
	4 Implementation
	5 Evaluation of Online Exam Outcomes
	6 Conclusion
	References
Gauss-Lintel, an Algorithm Suite for Exploring Chord Diagrams
	1 Gauss Diagrams and Their Properties
	2 Even-Odd Matchings and Lintels
	3 Implementation
		3.1 Lintel Generation and Canonization
		3.2 Properties/Conditions Checking
	4 Experiments and Results
	5 Related Work
	References
Logic and Systems
A New Export of the Mizar Mathematical Library
	1 Introduction
	2 Design
		2.1 Formalizing the Mizar Logic
		2.2 Exporting the MML as XML
		2.3 Reading the XML into Scala Classes
		2.4 Translating the Scala Classes to MMT
	3 Conclusion and Future Work
	References
A Language with Type-Dependent Equality
	1 Introduction
	2 Motivating Considerations and Related Work
		2.1 Type-Dependent Equality
		2.2 Abstract Definitions and Quotient Types
		2.3 Predicate and Quotient Types
		2.4 Records and Predicate/Quotient Types
	3 Formal Language Definition
		3.1 Syntax and Inference System
		3.2 Semantics
		3.3 Lax Record Types
	4 Conclusion
	References
Generating Custom Set Theories with Non-set Structured Objects
	1 Introduction
	2 Logical Framework
	3 Example Axiomatizations of Generalized Set Theories
	4 Model Building Kit
	5 Connecting Models to Domains
	6 Examples of Models of GSTs
	7 Conclusion and Future Work
	References
CICM\'21 Systems Entries
	References
Author Index