| Description |
1 online resource |
| Series |
Lecture notes in artificial intelligence |
|
Lecture notes in computer science ; 12833 |
|
LNCS sublibrary, SL 7, Artificial intelligence |
|
Lecture notes in computer science. Lecture notes in artificial intelligence.
|
|
Lecture notes in computer science ; 12833.
|
|
LNCS sublibrary. SL 7, Artificial intelligence.
|
| Contents |
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 |
| Summary |
This book constitutes the refereed proceedings of the 14th International Conference on Intelligent Computer Mathematics, CICM 2021, held in Timisoara, Romania, in July 2021*. The 12 full papers, 7 system descriptions, 1 system entry, and 3 abstracts of invited papers presented were carefully reviewed and selected from a total of 38 submissions. The papers focus on advances in formalization, automatic theorem proving and learning, search and classification, teaching and geometric reasoning, and logic and systems, among other topics. * The conference was held virtually due to the COVID-19 pandemic |
| Notes |
"This year's meeting was supposed to be held in Timisoara, Romania, but again due to the pandemic, it was held online."--Preface |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
Online resource; title from PDF title page (SpringerLink, viewed August 5, 2021) |
| Subject |
Computer science -- Mathematics -- Congresses
|
|
Artificial intelligence -- Mathematics -- Congresses
|
|
Artificial intelligence -- Mathematics
|
|
Computer science -- Mathematics
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Kamareddine, Fairouz D.
|
|
Coen, Claudio Sacerdoti.
|
| ISBN |
9783030810979 |
|
3030810976 |
|
