Intelligent Computer Mathematics
Springer International Publishing (Verlag)
978-3-031-66996-5 (ISBN)
- Noch nicht erschienen - erscheint am 16.09.2024
- Versandkostenfrei innerhalb Deutschlands
- Auch auf Rechnung
- Verfügbarkeit in der Filiale vor Ort prüfen
- Artikel merken
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.
.- 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.
Erscheint lt. Verlag | 16.9.2024 |
---|---|
Reihe/Serie | Lecture Notes in Artificial Intelligence | Lecture Notes in Computer Science |
Zusatzinfo | XX, 340 p. |
Verlagsort | Cham |
Sprache | englisch |
Maße | 155 x 235 mm |
Themenwelt | Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik |
Schlagworte | AI • automated deduction • Computer Algebra • digital mathematical libraries • knowledge representation • Knowledge Representation • LLM • logical framework • mathematical knowledge formalization • proof archives • Proof Assistants • proof certification • proof search • Proof transformations • theorem proving • user interfaces • User Interfaces |
ISBN-10 | 3-031-66996-7 / 3031669967 |
ISBN-13 | 978-3-031-66996-5 / 9783031669965 |
Zustand | Neuware |
Haben Sie eine Frage zum Produkt? |
aus dem Bereich