TY  - BOOK
AU  - Kohlhase,Andrea
AU  - Kovács,Laura
ED  - SpringerLink (Online service)
TI  - Intelligent Computer Mathematics: 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings 
T2  - Lecture Notes in Artificial Intelligence,
SN  - 9783031669972
AV  - Q334-342 
U1  - 006.3 23
PY  - 2024///
CY  - Cham
PB  - Springer Nature Switzerland, Imprint: Springer
KW  - Artificial intelligence
KW  - Machine theory
KW  - Social sciences
KW  - Data processing
KW  - Education
KW  - Algorithms
KW  - Application software
KW  - Artificial Intelligence
KW  - Formal Languages and Automata Theory
KW  - Computer Application in Social and Behavioral Sciences
KW  - Computers and Education
KW  - Design and Analysis of Algorithms
KW  - Computer and Information Systems Applications
N1  -  -- 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
N2  - 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
UR  - http://libcon.rec.uabc.mx:2048/login?url=https://doi.org/10.1007/978-3-031-66997-2
ER  -