Intelligent Computer Mathematics

18th International Conference, CICM 2025, Brasilia, Brazil, October 6-11, 2025, Proceedings
Herausgegeben:de Paiva, Valeria; Koepke, Peter

• Broschiertes Buch

Produktbeschreibung

This book constitutes the refereed proceedings of the 18th International Conference on Intelligent Computer Mathematics, CICM 2025, held in Brasilia, Brazil, during October 6 11, 2025.

The 24 full papers were presented in this volume were carefully reviewed and selected from 34 submissions. They were organized in the following topical sections as follows : Automated Reasoning; Formal Libraries; Logical and Linguistic Foundations; Mathematical Knowledge Management; Neural Language Models; and Proof Assistants and Formalizations.

Produktdetails

• Lecture Notes in Computer Science 16136
• Verlag: Springer / Springer Nature Switzerland / Springer, Berlin
• Artikelnr. des Verlages: 89538319, 978-3-032-07020-3
• Seitenzahl: 470
• Erscheinungstermin: Oktober 2025
• Englisch
• Abmessung: 235mm x 155mm
• Gewicht: 745g
• ISBN-13: 9783032070203
• ISBN-10: 3032070201
• Artikelnr.: 75264131

Inhaltsangabe

.- Automated Reasoning.

.- Hammering Higher Order Set Theory.

.- Synthesis Benchmarks for Automated Reasoning.

.- Automated Symmetric Constructions in Discrete Geometry.

.- Formal Libraries.

.- Growing Mathlib: Maintenance of a Large Scale Mathematical Library.

.- Exploring Formal Math on the Blockchain: An Explorer for Proofgold.

.- Supporting Maintenance of Formal Mathematics with Similarity Search.

.- Logical and Linguistic Foundations.

.- Graded Quantitative Narrowing.

.- Equational Generalization Problems with Atom-Variables.

.- Extending Flexible Boolean Semantics for the Language of Mathematics.

.- A Formal Definition of an Algorithm Suitable for Parsing the Language of Mathematics.

.- Mathematical Knowledge Management.

.- Reaping the Benefits of Modularization in Flexiformal Mathematics by GFbased AST Transformations.

.- Semantic Authoring in a Flexiformal Context Bulk Annotation of Rigorous Documents.

.- Michael Kohlhase and Jan Frederik Schaefer Lightweight Realms.

.- Indexing and Retrieval in a Heterogeneous Formal Library.

.- Neural Language Models.

.- Exploring Proof Autoformalization with Mistral on Herald.

.- Boosting Math Problem Solving in Small LLMs via Ensembles.

.- Proof Assistants and Formalizations.

.- Formalizing a Classification Theorem for Low-Dimensional Solvable Lie Algebras in Lean.

.- Certified Algorithms for Numerical Semigroups in Rocq.

.- Formalizing the Solow Model in Naproche.

.- Formalizing MLTL Formula Progression in Isabelle/HOL.

.- Formalising Fairness in the Assignment Problem with Ordinal Preferences in Isabelle/HOL.

.- A PVS Library on the Infinitude of Primes.

.- Vector Graphics through Category Theory.

.- A Lean-Based Language for Teaching Proof in High School.