Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings

Preface
Organization
Abstracts of Invited Talks
	SMT Solving for Arithmetic Theories
	Welcome to ar5iv! Wrestling with the Open Problems of Scholarly Writing
	Contents
Invited Talk
A Formalization of the Change of Variables Formula for Integrals in mathlib
	1 Introduction
	2 Sketch of Proof of Theorem 1.1
	3 A More Sophisticated Version of the Theorem
	4 The Formalized Version of the Theorem
	5 Linear Maps Rescale Lebesgue Measure According to Their Determinants
	6 Covering Theorems in Measure Theory
	7 Polish Spaces and Descriptive Set Theory
	8 Conclusion
	References
Formalizations
On the Formalization of the Heat Conduction Problem in HOL
	1 Introduction
	2 Related Work
	3 Preliminaries
	4 Formalization of the Heat Conduction Problem
		4.1 Heat Conduction Problem Formulation
		4.2 Formalization of the Heat Equation
	5 Formal Verification of the Solution of the Heat Equation
	6 Conclusion
	References
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
	1 Introduction
		1.1 Set Theory
		1.2 Higher-Order Logic
		1.3 Types
		1.4 Generalized Set Theories
		1.5 Isabelle/HOL/GST
		1.6 Summary of Contributions
	2 Mathematical Definitions and Logical Framework
		2.1 Syntax and Types
		2.2 Soft Types
		2.3 Inference Rules and Axioms
		2.4 Classes
	3 GSTs as Type Classes
		3.1 GST Features
		3.2 Example Features
		3.3 Feature Combination
	4 Examples of Working in a GST
	5 Building a Model for ZF+ in ZFC
		5.1 Building a Model in V
		5.2 Instantiating ZF+ in d0
	6 Related and Future Work
	References
Formalising Basic Topology for Computational Logic in Simple Type Theory
	1 Introduction
	2 Topological Boolean Algebras
		2.1 Boolean Algebras
		2.2 Topological Conditions
		2.3 Closure Algebras
	3 Formalising Basic Topology
		3.1 Properties of Sets
		3.2 Relativisation
		3.3 Neighborhoods and Limits
		3.4 Separation
		3.5 Connectedness
		3.6 Compactness
		3.7 Continuity and Homeomorphism
		3.8 Specialisation Orderings and Relations
	4 Methodological Remarks
	5 Related Work
	6 Further Work and Conclusions
	References
Formalising the Kruskal-Katona Theorem in Lean
	1 Introduction
	2 Related Work
	3 Mathematical Background
		3.1 LYM Inequalities and Sperner\'s Theorem
		3.2 Kruskal-Katona
	4 Formalising the Shadow
		4.1 Definitions
		4.2 Local LYM Inequality
		4.3 LYM Inequality
	5 Kruskal-Katona Theorem
		5.1 Colexicographic Ordering
		5.2 Compressions
		5.3 Main Theorem
	6 Future Work and Conclusion
	References
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis
	1 Introduction
	2 Isabelle and Set Theory
		2.1 Formalising ZF in Higher-Order Logic
		2.2 Axiomatic Type Classes
		2.3 The Development ZFC-in-HOL
		2.4 The Integration of ZFC-in-HOL with Isabelle/HOL
		2.5 Embedding Isabelle/HOL Types into V
	3 Wetzel\'s Problem: The CH Case
	4 Wetzel\'s Problem: The CH Case
		4.1 The Transfinite Construction
		4.2 The Isabelle/HOL Formalisation
		4.3 The Transfinite Construction
		4.4 Concluding the Proof
	5 Discussion
	6 Conclusions
	References
Hall\'s Theorem for Enumerable Families of Finite Sets
	1 Hall\'s Theorem
	2 Cameron\'s Informal Proof
	3 Formalisation
		3.1 Notes on the Formalisation of the Propositional Compactness Theorem
		3.2 Formalisation of Hall\'s Theorem - the Enumerable Version
	4 Related Work
	5 Conclusion
	References
Graded Rings in Lean\'s Dependent Type Theory
	1 Introduction
		1.1 Prior Formalizations
		1.2 Additive Vs Multiplicative Grading
	2 External Gradings
		2.1 Graded Semigroups
		2.2 Graded Monoids
		2.3 Graded (semi)rings
	3 Internal Gradings
		3.1 Decompositions of Sets
		3.2 Graded Monoids
		3.3 Decompositions of Additive Monoids and R-Modules
		3.4 Graded (semi)rings
	4 Graded R-Algebras
	5 Conclusions
	References
Digital Libraries and Mathematical Knowledge Management
An Integrated Web Platform for the Mizar Mathematical Library
	1 Introduction
	2 Wiki Function
	3 Search Function
	4 Visualization of Library Dependencies
	5 Conclusions and Future Work
	References
Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs
	1 Introduction
	2 Complex Network Concepts
	3 Complex Network Science in Software Engineering
	4 Analysis of Formal Entity Networks
		4.1 Dependency Graph as Complex Network
		4.2 Assessing Formalization Quality
		4.3 Predicting Important Concepts
	5 Discussion
		5.1 Threats to Validity
		5.2 Future Work
	References
Re-imagining the Isabelle Archive of Formal Proofs
	1 Introduction
	2 (Re)Design Considerations
	3 Implementation
		3.1 Metadata Model
		3.2 Searching Capabilities
		3.3 Theory Browsing
		3.4 Site and Entry Navigation
	4 Conclusion
	References
Injecting Formal Mathematics Into LaTeX
	1 Introduction
	2 Preliminaries
	3 Translating Phenomena in Informal Mathematics to a Formal System
		3.1 Formal Theories Vs. Document Fragments
		3.2 Implicit Arguments and Variables
		3.3 Flexary Operators and Argument Sequences
		3.4 Statements(Theorems, Definitions, Axioms, Proofs, …)
	4 Implementing Structural Featuresin
		4.1 Mathematical Structures (Module Types)
		4.2 Includes with Modification (Mmt-structures)
		4.3 Parametric Theories, Views, Realizations and Realms
	5 Conclusion and Future Work
	References
System Description 3 – A LaTeX-Based Ecosystem for Semantic/Active Mathematical Documents
	1 Introduction and History
	2 The 3 Package
	3 OMDoc and Mmt
	4 Ongoing and Future Work
	References
Theorem Proving and Expression Transformation
Lemmaless Induction in Trace Logic
	1 Introduction
	2 Motivating Example
	3 Related Work
	4 Preliminaries
		4.1 Trace Logic L
		4.2 Programming Model W
		4.3 Translating Expressions to Trace Logic
		4.4 Axiomatic Semantics of W in L
		4.5 Trace Lemma Reasoning
	5 Multi-Clause Goal Induction for Lemmaless Induction
	6 Array Mapping Induction for Lemmaless Induction
	7 Implementation
	8 Experimental Results
	9 Future Directions and Conclusion
	References
Unified Decomposition-Aggregation (UDA) Rules: Dynamic, Schematic, Novel Axioms
	1 Introduction
	2 Association Lists
	3 Variables in Alists
	4 UDA Rules
		4.1 The New Axiom
		4.2 Representing Uncertainty
		4.3 The Correctness of the UDA Rules
	5 Worked Example
	6 Related Work
	7 Future Work
	8 Conclusion
	References
Working with Families of Inverse Functions
	1 Introduction
	2 Basic Concepts
	3 The Elementary Functions
		3.1 Exponential and Logarithm
		3.2 Sine and Arcsine
		3.3 Inverse Cosine
		3.4 Inverse Tangent
		3.5 Fractional Powers
		3.6 Definitions in Terms of Logarithms
	4 Applications
		4.1 Plotting
		4.2 Identities
		4.3 Calculus
	5 Simplification of Lambert W
	6 Proof with Multivalued Functions
	7 Pseudoinverses
	8 Conclusions
	References
Satisfiability, QBF, and SMT Solving
Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification
	1 Introduction
	2 Background
	3 QBF Encoding
	4 Reading a Witness String from the Certificate
		4.1 What is a QSAT Certificate?
		4.2 Processing the Certificate
	5 Experiments
		5.1 Random Model
		5.2 Determining NFA Equivalence via QBFs
		5.3 Extracting Witness Strings
	6 Verifying the Encoding in Isabelle/HOL
	7 Conclusions and Future Work
	References
Targeted Configuration of an SMT Solver
	1 Introduction
	2 Grackle: Strategy Portfolio Invention System
	3 Making the Grackle Fly
	4 Strategy Selection with Boosted Decision Trees
	5 Evaluation of Grackle Strategy Invention
	6 Evaluation of Strategy Selection
	7 Conclusions and Future Work
	References
OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas
	1 Introduction
	2 Related Work
	3 Preliminaries
	4 Counting Models
	5 Counting Counter-Models
	6 Implementation
	7 Evaluation
	8 Conclusion
	References
Computer-Aided Teaching
Experiments with Automated Reasoning in the Class
	1 Introduction
	2 Tools
		2.1 Automated Reasoning in Theorema
		2.2 Synthesis and Transformation of Algorithms
		2.3 Sample Implementations
		2.4 The Coq Theorem Prover
		2.5 SAT Solvers
		2.6 SMT Solving
	3 Conclusion
	References
Learning to Reason Assisted by Automated Reasoning
	1 Introduction
	2 The Use of Software in the Teaching of Logic
		2.1 Modules, Quizzes, Bonus, Lab
		2.2 Interactive Automated Theorem Proving in Theorema
		2.3 How Software is Embedded into the Course
	3 Results
		3.1 Personal Impression of Students
		3.2 Performance in the Quizzes
	4 Conclusion
	References
Datasets and System Entries
Making the Census of Cubic Vertex Transitive Graphs Searchable and FAIR
	1 Introduction
	2 A Brief Description of the Contents and Structure
	3 FAIR-ifying the CVT Census on Zenodo
	4 Making the Dataset Searchable with MathDataHub
	References
An Evaluation of NLP Methods to Extract Mathematical Token Descriptors
	1 Introduction
	2 Related Work
	3 Dataset
		3.1 Example Entries
		3.2 Dataset Statistics
	4 Models
	5 Results
		5.1 Single-Word Descriptor Extraction
		5.2 Multi-word Definition Extraction
		5.3 Data Attributes Impacting Model Accuracy
	6 Conclusion
	1  Models
		1.1  Vanilla Sequence-to-Sequence Model
		1.2  Transformer Seq2Seq Model
		1.3  Pointer Network
		1.4  Match-LSTM Model
		1.5  Bert-Based Model
	References
CICM\'22 System Entries
	References
Author Index