Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1484.68013].
Indexed articles:
Gouëzel, Sébastien, A formalization of the change of variables formula for integrals in mathlib, 3-18 [Zbl 07691287]
Deniz, Elif; Rashid, Adnan; Hasan, Osman; Tahar, Sofiène, On the formalization of the heat conduction problem in HOL, 21-37 [Zbl 07691288]
Dunne, Ciarán; Wells, J. B., Isabelle/HOL/GST: a formal proof environment for generalized set theories, 38-55 [Zbl 07691289]
Fuenmayor, David; Serrano Suárez, Fabián Fernando, Formalising basic topology for computational logic in simple type theory, 56-74 [Zbl 07691290]
Mehta, Bhavik, Formalising the Kruskal-Katona theorem in Lean, 75-91 [Zbl 07691291]
Paulson, Lawrence C., Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis, 92-106 [Zbl 07691292]
Serrano Suárez, Fabián Fernando; Ayala-Rincón, Mauricio; de Lima, Thaynara Arielly, Hall’s theorem for enumerable families of finite sets, 107-121 [Zbl 07691293]
Wieser, Eric; Zhang, Jujian, Graded rings in Lean’s dependent type theory, 122-137 [Zbl 07691294]
Furushima, Hideharu; Yamamichi, Daichi; Shigenaka, Seigo; Nakasho, Kazuhisa; Wasaki, Katsumi, An integrated web platform for the Mizar Mathematical Library, 141-146 [Zbl 07691295]
Huch, Fabian, Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs, 147-161 [Zbl 07691296]
MacKenzie, Carlin; Huch, Fabian; Vaughan, James; Fleuriot, Jacques, Re-imagining the Isabelle archive of formal proofs, 162-167 [Zbl 07691297]
Müller, Dennis; Kohlhase, Michael, Injecting formal mathematics into LaTeX, 168-183 [Zbl 07691298]
Kohlhase, Michael; Müller, Dennis, System description STEX3 – a L^AT_EX-based ecosystem for semantic/active mathematical documents, 184-188 [Zbl 07691299]
Bhayat, Ahmed; Georgiou, Pamina; Eisenhofer, Clemens; Kovács, Laura; Reger, Giles, Lemmaless induction in trace logic, 191-208 [Zbl 07691300]
Bundy, Alan; Nuamah, Kwabena, Unified decomposition-aggregation (UDA) rules: dynamic, schematic, novel axioms, 209-221 [Zbl 07691301]
Jeffrey, David J.; Watt, Stephen M., Working with families of inverse functions, 222-237 [Zbl 07691302]
Hemaspaandra, Edith; Narváez, David E., Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification, 241-255 [Zbl 07691303]
Hůla, Jan; Jakubův, Jan; Janota, Mikoláš; Kubej, Lukáš, Targeted configuration of an SMT solver, 256-271 [Zbl 07691304]
Shukla, Ankit; Möhle, Sibylle; Kauers, Manuel; Seidl, Martina, OuterCount: a first-level solution-counter for quantified Boolean formulas, 272-284 [Zbl 07691305]
Drămnesc, Isabela; Ábrahám, Erika; Jebelean, Tudor; Kusper, Gábor; Stratulat, Sorin, Experiments with automated reasoning in the class, 287-304 [Zbl 07691306]
Windsteiger, Wolfgang, Learning to reason assisted by automated reasoning, 305-320 [Zbl 07691307]
Berčič, Katja; Koprivec, Filip, Making the census of cubic vertex transitive graphs searchable and FAIR, 323-328 [Zbl 07691308]
Hamel, Emma; Zheng, Hongbo; Kani, Nickvash, An evaluation of NLP methods to extract mathematical token descriptors, 329-343 [Zbl 07691309]
Koepke, Peter; Lorenzen, Anton; Shminke, Boris, CICM’22 system entries, 344-348 [Zbl 07691310]