default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID15th CICM 2022: Tbilisi, Georgia
- Kevin Buzzard
, Temur Kutsia:
Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings. Lecture Notes in Computer Science 13467, Springer 2022, ISBN 978-3-031-16680-8
Invited Talk
- Sébastien Gouëzel:
A Formalization of the Change of Variables Formula for Integrals in mathlib. 3-18
Formalizations
- Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar:
On the Formalization of the Heat Conduction Problem in HOL. 21-37 - Ciarán Dunne, J. B. Wells:
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. 38-55 - David Fuenmayor, Fabián Fernando Serrano Suárez:
Formalising Basic Topology for Computational Logic in Simple Type Theory. 56-74 - Bhavik Mehta:
Formalising the Kruskal-Katona Theorem in Lean. 75-91 - Lawrence C. Paulson:
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. 92-106 - Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón, Thaynara Arielly de Lima:
Hall's Theorem for Enumerable Families of Finite Sets. 107-121 - Eric Wieser, Jujian Zhang:
Graded Rings in Lean's Dependent Type Theory. 122-137
Digital Libraries and Mathematical Knowledge Management
- Hideharu Furushima, Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki:
An Integrated Web Platform for the Mizar Mathematical Library. 141-146 - Fabian Huch:
Formal Entity Graphs as Complex Networks: Assessing Centrality Metrics of the Archive of Formal Proofs. 147-161 - Carlin MacKenzie, Fabian Huch, James Vaughan, Jacques D. Fleuriot:
Re-imagining the Isabelle Archive of Formal Proofs. 162-167 - Dennis Müller, Michael Kohlhase:
Injecting Formal Mathematics Into LaTeX. 168-183 - Michael Kohlhase, Dennis Müller:
System Description STEX3 - A LATEX-Based Ecosystem for Semantic/Active Mathematical Documents. 184-188
Theorem Proving and Expression Transformation
- Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger:
Lemmaless Induction in Trace Logic. 191-208 - Alan Bundy, Kwabena Nuamah:
Unified Decomposition-Aggregation (UDA) Rules: Dynamic, Schematic, Novel Axioms. 209-221 - David J. Jeffrey, Stephen M. Watt:
Working with Families of Inverse Functions. 222-237
Satisfiability, QBF, and SMT Solving
- Edith Hemaspaandra, David E. Narváez:
Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification. 241-255 - Jan Hula, Jan Jakubuv, Mikolás Janota, Lukás Kubej:
Targeted Configuration of an SMT Solver. 256-271 - Ankit Shukla, Sibylle Möhle, Manuel Kauers, Martina Seidl:
OuterCount: A First-Level Solution-Counter for Quantified Boolean Formulas. 272-284
Computer-Aided Teaching
- Isabela Dramnesc, Erika Ábrahám, Tudor Jebelean, Gábor Kusper, Sorin Stratulat:
Experiments with Automated Reasoning in the Class. 287-304 - Wolfgang Windsteiger:
Learning to Reason Assisted by Automated Reasoning. 305-320
Datasets and System Entries
- Katja Bercic, Filip Koprivec:
Making the Census of Cubic Vertex Transitive Graphs Searchable and FAIR. 323-328 - Emma Hamel, Hongbo Zheng, Nickvash Kani:
An Evaluation of NLP Methods to Extract Mathematical Token Descriptors. 329-343 - Peter Koepke, Anton Lorenzen, Boris Shminke:
CICM'22 System Entries. 344-348
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-13 20:19 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:
