Intelligent Computer Mathematics

17th International Conference, CICM 2024, Montréal, QC, Canada, August 5¿9, 2024, Proceedings
Herausgegeben:Kohlhase, Andrea; Kovács, Laura

• Broschiertes Buch

Produktbeschreibung

This book constitutes the refereed proceedings of the 17th International Conference on Intelligent Computer Mathematics, CICM 2024, held in Montréal, Québec, Canada, during August 5-9, 2024.

The 21 full papers presented were carefully reviewed and selected from 28 submissions. These papers have been categorized into the following sections: AI and LLM; Proof Assistants; Logical Frameworks and Transformations; Knowledge Representation and Certification; Proof Search and Formalization & System Descriptions.

Produktdetails

• Lecture Notes in Computer Science 14960
• Verlag: Springer / Springer Nature Switzerland / Springer, Berlin
• Artikelnr. des Verlages: 978-3-031-66996-5
• 2024
• Seitenzahl: 380
• Erscheinungstermin: 4. August 2024
• Englisch
• Abmessung: 235mm x 155mm x 21mm
• Gewicht: 575g
• ISBN-13: 9783031669965
• ISBN-10: 3031669967
• Artikelnr.: 70986991

Inhaltsangabe

.- AI and LLM.

.- Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations.

.- Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane.

.- Using General Large Language Models to Classify Mathematical Documents.

.- Proof Assistants.

.- Chaining extensionality lemmas in Lean's Mathlib.

.- A formalization of all notions in the statement of a theorem by Deligne.

.- Formalizing Finite Ramsey Theory in Lean 4.

.- Formalizing Pick's Theorem in Isabelle/HOL.

.- Formalizing Coppersmith's Method in Isabelle/HOL.

.- Incorporating a database of graphs into a proof assistant.

.- Logical Frameworks and Transformations.

.- Reusing Learning Objects via Theory Morphisms.

.- Transforming Optimization Problems into Disciplined Convex Programming Form.

.- A Logical Framework Perspective on Conservativity.

.- Knowledge Representation and Certification.

.- Towards Semantic Markup of Mathematical Documents via User Interaction.

.- Evaluation and Domain Adaptation of Similarity Models for Short Mathematical Texts.

.- Generating Formally Verified Quantum Fourier Transform Algorithms.

.- Proof Search and Formalization.

.- Partial proof terms in the study of idealized proof search.

.- A Framework for Formal Probabilistic Risk Assessment using HOL Theorem Proving.

.- Solving Hard Mizar Problems with Instantiation and Strategy Invention.

.- System Descriptions.

.- Remote Verification System for Mizar Integrated with Emwiki.

.- Oruga: Implementation and Use of Representational Systems Theory.

.- HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover.