![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
16th 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
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
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.