Intelligent Computer Mathematics
Springer International Publishing (Verlag)
978-3-032-07020-3 (ISBN)
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.
.- 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.
| Erscheinungsdatum | 08.10.2025 |
|---|---|
| Reihe/Serie | Lecture Notes in Artificial Intelligence | Lecture Notes in Computer Science |
| Zusatzinfo | XXIII, 470 p. 200 illus., 170 illus. in color. |
| Verlagsort | Cham |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Themenwelt | Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik |
| Schlagworte | automated reasoning • Automated Theorem Proving • formal grammars • Formalizations • Formal Libraries • formal mathematics • interactive theorem proving • Isabelle Prover • Language of mathematics • Large Language Models • Lean Prover • machine learning • mathematical knowledge management • Natural Language Processing • Proof Assistants • Rocq Prover |
| ISBN-10 | 3-032-07020-1 / 3032070201 |
| ISBN-13 | 978-3-032-07020-3 / 9783032070203 |
| Zustand | Neuware |
| Informationen gemäß Produktsicherheitsverordnung (GPSR) | |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
