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

This book constitutes the refereed proceedings of the 15th International Conference on Intelligent Computer Mathematics, CICM 2022, held in Tbilisi, Georgia, in September 2022. The 17 full papers, 1 project/ survey paper, 4 short papers, and 2 abstracts of invited papers presented were carefully reviewed and selected from a total of 37 submissions. The papers focus on theoretical and practical solutions for these challenges including computation, deduction, narration, and data management. 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