With the continuing, rapid progress of digital methods in communications, knowledge representation, processing, and discovery, the unique character and needs of mathematical information require unique approaches. Its specialized representations and capacity for creation and proof, both automatically and formally as well as manually, set mathematical knowledge apart. The Conference on Intelligent Computer Mathematics (CICM) was initially formed in 2008 as a joint meeting of communities involved in computer algebra systems, automated theorem provers, and mathematical knowledge management, as well as those involved in a variety of aspects of scientific document archives. It has offered a venue for discussing, developing, and integrating the diverse, sometimes eclectic, approaches and research. Since 2008, CICM has been held annually: Birmingham (UK, 2008), Grand Bend (Canada, 2009), Paris (France, 2010), Bertinoro (Italy, 2011), Bremen (Germany, 2012), Bath (UK, 2013), Coimbra (Portugal, 2014), Washington D. C. (USA, 2015), Bialystok (Poland, 202016), Edinburgh (UK, 2017), Linz (Austria, 2018), Prague (Czech Republic, 2019) and Bertinoro (Italy, 2020). This latter edition, which was originally scheduled to be held in Bertinoro, Italy, was hosted online due to the COVID-19 pandemic. This year’s meeting was supposed to be held in Timisoara, Romania, but again due to the pandemic, it was held online (July 26–31, 2021). This year’s meeting exposed advances in formalizations, automatic theorem proving, applications of machine learning to mathematical documents and proof search, search and classifications of mathematical documents, teaching and geometric reasoning, and logic and systems, among other topics. This volume contains the contributions to this conference. From 38 formal submissions, the Program Committee (PC) accepted 20 papers including 12 full research papers, 7 shorter papers describing software systems or datasets and 1 paper highlighting development of systems and tools in the last year. All papers were reviewed by at least three PC members or external reviewers. The reviews were single-blind and included a response period in which the authors could respond and clarify points raised by the reviewers. In addition to the main sessions, the conference included a doctoral program, chaired by Yasmine Sharoda, which provided a forum for PhD students to present their research and get advice from senior members of the community. Additionally, the following workshops were scheduled: – The 31st OpenMath Workshop, organized by James Davenport and Michael Kohlhase. – The 2nd Workshop on Natural Formal Mathematics (NatFoM 2021), organized by Peter Koepke and Dennis Müller. – The 5th Workshop on Formal Mathematics for Mathematicians (FMM 2021), organized by Jasmine Blanchette and Adam Naumowicz. – The 2nd Workshop on Formal Verification of Physical Systems (FVPS 2021), organized by Sofiene Tahar, Osman Hasan and Adnan Rashid. – The 13th Workshop on Mathematical User Interaction (MathUI 2021), organized by Andrea Kohlhase. Finally, the conference included four invited talks: – Alessandro Cimatti (Fondazione Bruno Kessler, Italy): “Logic at work, and some research challenges for computer mathematics”. – Michael Kohlhase (FAU Erlangen-Nürnberg, Germany): “Referential Semantics – a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge”. – Laura Kovacs (TU Vienna, Austria): “Induction in Saturation-Based Reasoning”. – Angus McIntyre (Emeritus Professor, Queen Mary University of London, UK): “Doing classical number theory in weak axiomatic systems”. A successful conference is due to the efforts of many people. We thank Madalina Erascu and her colleagues at the West University of Timisoara, Romania, for the difficult task of organizing a conference with the expectation of it being held face to face but with the dynamics of COVID-19 making it difficult to accommodate in person meetings. We are grateful to Serge Autexier for his publicity work. We also thank the authors of submitted papers, the PC for their reviews, and the organizers of the workshops, as well as the invited speakers and the participants of the conference. June 2021 F. Kamareddine C. Sacerdoti Coen
Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26–31, 2021, Proceedings
Sacerdoti Coen C.
2021
Abstract
With the continuing, rapid progress of digital methods in communications, knowledge representation, processing, and discovery, the unique character and needs of mathematical information require unique approaches. Its specialized representations and capacity for creation and proof, both automatically and formally as well as manually, set mathematical knowledge apart. The Conference on Intelligent Computer Mathematics (CICM) was initially formed in 2008 as a joint meeting of communities involved in computer algebra systems, automated theorem provers, and mathematical knowledge management, as well as those involved in a variety of aspects of scientific document archives. It has offered a venue for discussing, developing, and integrating the diverse, sometimes eclectic, approaches and research. Since 2008, CICM has been held annually: Birmingham (UK, 2008), Grand Bend (Canada, 2009), Paris (France, 2010), Bertinoro (Italy, 2011), Bremen (Germany, 2012), Bath (UK, 2013), Coimbra (Portugal, 2014), Washington D. C. (USA, 2015), Bialystok (Poland, 202016), Edinburgh (UK, 2017), Linz (Austria, 2018), Prague (Czech Republic, 2019) and Bertinoro (Italy, 2020). This latter edition, which was originally scheduled to be held in Bertinoro, Italy, was hosted online due to the COVID-19 pandemic. This year’s meeting was supposed to be held in Timisoara, Romania, but again due to the pandemic, it was held online (July 26–31, 2021). This year’s meeting exposed advances in formalizations, automatic theorem proving, applications of machine learning to mathematical documents and proof search, search and classifications of mathematical documents, teaching and geometric reasoning, and logic and systems, among other topics. This volume contains the contributions to this conference. From 38 formal submissions, the Program Committee (PC) accepted 20 papers including 12 full research papers, 7 shorter papers describing software systems or datasets and 1 paper highlighting development of systems and tools in the last year. All papers were reviewed by at least three PC members or external reviewers. The reviews were single-blind and included a response period in which the authors could respond and clarify points raised by the reviewers. In addition to the main sessions, the conference included a doctoral program, chaired by Yasmine Sharoda, which provided a forum for PhD students to present their research and get advice from senior members of the community. Additionally, the following workshops were scheduled: – The 31st OpenMath Workshop, organized by James Davenport and Michael Kohlhase. – The 2nd Workshop on Natural Formal Mathematics (NatFoM 2021), organized by Peter Koepke and Dennis Müller. – The 5th Workshop on Formal Mathematics for Mathematicians (FMM 2021), organized by Jasmine Blanchette and Adam Naumowicz. – The 2nd Workshop on Formal Verification of Physical Systems (FVPS 2021), organized by Sofiene Tahar, Osman Hasan and Adnan Rashid. – The 13th Workshop on Mathematical User Interaction (MathUI 2021), organized by Andrea Kohlhase. Finally, the conference included four invited talks: – Alessandro Cimatti (Fondazione Bruno Kessler, Italy): “Logic at work, and some research challenges for computer mathematics”. – Michael Kohlhase (FAU Erlangen-Nürnberg, Germany): “Referential Semantics – a Concept for Bridging between Representations of mathematical/technical Documents and Knowledge”. – Laura Kovacs (TU Vienna, Austria): “Induction in Saturation-Based Reasoning”. – Angus McIntyre (Emeritus Professor, Queen Mary University of London, UK): “Doing classical number theory in weak axiomatic systems”. A successful conference is due to the efforts of many people. We thank Madalina Erascu and her colleagues at the West University of Timisoara, Romania, for the difficult task of organizing a conference with the expectation of it being held face to face but with the dynamics of COVID-19 making it difficult to accommodate in person meetings. We are grateful to Serge Autexier for his publicity work. We also thank the authors of submitted papers, the PC for their reviews, and the organizers of the workshops, as well as the invited speakers and the participants of the conference. June 2021 F. Kamareddine C. Sacerdoti CoenI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
