default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID16th CICM 2023: Cambridge, UK
- Catherine Dubois
, Manfred Kerber:
Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings. Lecture Notes in Computer Science 14101, Springer 2023, ISBN 978-3-031-42752-7
Invited Talks
- Lawrence C. Paulson:
Large-Scale Formal Proof for the Working Mathematician - Lessons Learnt from the ALEXANDRIA Project. 3-15 - Martina Seidl:
Never Trust Your Solver: Certification for SAT and QBF. 16-33
Regular Papers
- Jesús Aransay, Laureano Lambán, Julio Rubio:
Evasiveness Through Binary Decision Diagrams. 37-52 - Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes-Sobrinho:
Nominal AC-Matching. 53-68 - Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott:
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. 69-83 - Marc Berges, Jonas Betzendahl, Abhishek Chugh, Michael Kohlhase, Dominic Lohr, Dennis Müller:
Learning Support Systems Based on Mathematical Knowledge Management. 84-97 - Marco B. Caminati:
Isabelle Formalisation of Original Representation Theorems. 98-112 - Robert M. Corless, David J. Jeffrey, Azar Shakoori:
Teaching Linear Algebra in a Mechanized Mathematical Environment. 113-129 - Neeraj Gangwar, Nickvash Kani:
Highlighting Named Entities in Input for Auto-formulation of Optimization Problems. 130-141 - Fabian Huch, Yiannos Stathopoulos:
Formalization Quality in Isabelle. 142-157 - Aabid Seeyal Abdul Kharim, T. V. H. Prathamesh, Shweta Rajiv, Rishi Vyas:
Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem. 158-173 - Florian Rabe, Franziska Weber:
Morphism Equality in Theory Graphs. 174-189 - Jan Frederik Schaefer, Michael Kohlhase:
Towards an Annotation Standard for STEM Documents - Datasets, Benchmarks, and Spotters. 190-205 - Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin:
Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. 206-221 - Eric Wieser:
Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies. 222-236 - Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar:
CoProver: A Recommender System for Proof Construction. 237-251
Project and Survey Papers
- James Harold Davenport:
Proving an Execution of an Algorithm Correct? 255-269 - Jeffrey O. Shallit:
Proving Results About OEIS Sequences with Walnut. 270-282
System and Dataset Descriptions
- Henry Hammer, Nanako Noda, Christopher A. Stone:
ProofLang: The Language of arXiv Proofs. 285-290 - Simone Heisinger, Martina Seidl:
True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers. 291-296 - John Hester, Briland Hitaj, Grant O. Passmore, Sam Owre, Natarajan Shankar, Eric Yeh:
An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning. 297-302 - Jan Jakubuv, Cezary Kaliszyk:
VizAR: Visualization of Automated Reasoning Proofs (System Description). 303-308 - Adam Naumowicz:
Extending Numeric Automation for Number Theory Formalizations in Mizar. 309-314 - Florian Rabe, Stephen M. Watt:
Extracting Theory Graphs from Aldor Libraries. 315-320
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-12-04 01:25 CET 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:
