Publications in 2023

Lambert Series
Manuel Eberl
Archive of Formal Proofs 2023.

The Polylogarithm Function
Manuel Eberl
Archive of Formal Proofs 2023.

The Cardinality of the Continuum
Manuel Eberl
Archive of Formal Proofs 2023.

Two theorems about the geometry of the critical points of a complex polynomial
Manuel Eberl
Archive of Formal Proofs 2023.

Elimination of Repeated Factors Algorithm
Katharina Kreuzer, Manuel Eberl
Archive of Formal Proofs 2023.

Perfect Fields
Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2023.

Chebyshev Polynomials
Manuel Eberl
Archive of Formal Proofs 2023.

Learning Proof Transformations and Its Applications in Interactive Theorem Proving
Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
Frontiers of Combining Systems – 14th International Symposium, FroCoS 2023,   pp. 236-254, 2023.

Confluence Criteria for Logically Constrained Rewrite Systems
Jonas Schöpf, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 474-490, 2023.

Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 401-418, 2023.

VizAR: Visualization of Automated Reasoning Proofs (System Description)
Jan Jakubův and Cezary Kaliszyk
Intelligent Computer Mathematics – 16th International Conference, CICM 2023,   pp. 303-308, 2023.

Formalizing Almost Development Closed Critical Pairs
Christina Kohl, Aart Middeldorp
Proceedings of the 14th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics 268, pp. 38:1-38:8, 2023.

MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olšák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
14th International Conference on Interactive Theorem Proving,   pp. 19:1-19:22, 2023.

Hydra Battles and AC Termination
Nao Hirokawa, Aart Middeldorp
Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 260, pp. 22:1-12:16, 2023.

Executable Randomized Algorithms
Emin Karayel, Manuel Eberl
Archive of Formal Proofs 2023.

Experiments on Infinite Model Finding in SMT Solving
Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning,   pp. 317-328, 2023.

A Verified Efficient Implementation of the Weighted Path Order
René Thiemann, Elias Wenninger
Archive of Formal Proofs 2023.

Combining Higher-Order Logic with Set Theory Formalizations
Cezary Kaliszyk and Karol Pąk
Journal of Automated Reasoning 2023.

First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
Aart Middeldorp, Alexander Lochmann, Fabian Mitterwallner
Journal of Automated Reasoning 67, 2023.

A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Christina Kohl, Aart Middeldorp
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023),   pp. 197-210, 2023.