Intelligent computer mathematics : 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings / / Fairouz Kamareddine, Claudio Sacerdoti Coen (editors)

• Pubblicazione: Cham, Switzerland : , : Springer, , [2021]; ©2021
• Descrizione fisica: 1 online resource (263 pages)
• Disciplina: 004.0151
• Soggetto topico: Computer science - Mathematics
• Persona (resp. second.): KamareddineFairouz; CoenClaudio Sacerdoti
• Nota di contenuto: Intro -- 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.
• Titolo autorizzato: Intelligent Computer Mathematics
• ISBN: 3-030-81097-6
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996464426903316
• Lo trovi qui: Univ. di Salerno
• Serie: Lecture notes in computer science ; ; 12833.