default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID17th CICM 2024: Montréal, QC, Canada
- Andrea Kohlhase
, Laura Kovács:
Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings. Lecture Notes in Computer Science 14960, Springer 2024, ISBN 978-3-031-66996-5
AI and LLM
- Ruocheng Shan, Abdou Youssef:
Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations. 3-20 - Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins:
Automated Mathematical Discovery and Verification: Minimizing Pentagons in the Plane. 21-41 - Patrick D. F. Ion, Stephen M. Watt:
Using General Large Language Models to Classify Mathematical Documents. 42-57
Proof Assistants
- Eric Wieser:
Chaining Extensionality Lemmas in Lean's Mathlib. 61-72 - Michail Karatarakis:
A Formalization of All Notions in the Statement of a Theorem by Deligne. 73-90 - David E. Narváez, Cruise Song, Ningxin Zhang:
Formalizing Finite Ramsey Theory in Lean 4. 91-108 - Sage Binder, Katherine Kosaian:
Formalizing Pick's Theorem in Isabelle/HOL. 109-126 - Katherine Kosaian, Yong Kiam Tan, Kristin Yvonne Rozier:
Formalizing Coppersmith's Method in Isabelle/HOL. 127-145 - Andrej Bauer, Katja Bercic, Gauvain Devillez, Jure Taslak:
Incorporating a Database of Graphs into a Proof Assistant. 146-162
Logical Frameworks and Transformations
- Michael Kohlhase, Marcel Schütz:
Reusing Learning Objects via Theory Morphisms. 165-182 - Ramon Fernández Mir, Paul B. Jackson, Siddharth Bhat, Andrés Goens, Tobias Grosser:
Transforming Optimization Problems into Disciplined Convex Programming Form. 183-202 - Florian Rabe:
A Logical Framework Perspective on Conservativity. 203-219
Knowledge Representation and Certication
- Luka Vrecar, Joe B. Wells, Fairouz Kamareddine:
Towards Semantic Markup of Mathematical Documents via User Interaction. 223-240 - Christian Steinfeldt, Helena Mihaljevic:
Evaluation and Domain Adaptation of Similarity Models for Short Mathematical Texts. 241-260 - Patrick Brinich, Jeremy Johnson:
Generating Formally Verified Quantum Fourier Transform Algorithms. 261-276
Proof Search and Formalization
- José Espírito Santo, Ana Catarina Sousa:
Partial Proof Terms in the Study of Idealized Proof Search. 279-297 - Mohamed Abdelghany, Adnan Rashid, Sofiène Tahar:
A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem Proving. 298-314 - Jan Jakubuv, Mikolás Janota, Josef Urban:
Solving Hard Mizar Problems with Instantiation and Strategy Invention. 315-333
System Descriptions
- Toshiki Kai, Yuta Teruya, Kazuhisa Nakasho:
Remote Verification System for Mizar Integrated with Emwiki. 337-344 - Daniel Raggi, Gem Stapleton, Aaron Stockdill, Grecia Garcia Garcia, Peter C.-H. Cheng, Mateja Jamnik:
Oruga: Implementation and Use of Representational Systems Theory. 345-351 - Nour Dekhil, Adnan Rashid, Sofiène Tahar:
HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover. 352-359
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-10-22 02:22 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
