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

Description

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