Publications in 2022

The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections
Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel, Patrick Lederer 🌐
Archive of Formal Proofs 2022.

Proofgold: Blockchain for Formal Methods
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
4th International Workshop on Formal Methods for Blockchains, FMBC 2022,   pp. 4:1-4:15, 2022.

The Hales-Jewett Theorem
Ujkan Sulejmani, Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2022.

Lazy Paramodulation in Practice
Grzegorz Prusak, Cezary Kaliszyk
Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022,  2022.

The Isabelle Enigma
Zar Goerzel, Jan Jakubův, Cezary Kaliszyk, Mirek Olšák, Jelle Piepenbroek, Josef Urban
13th International Conference on Interactive Theorem Proving, ITP 2022,   pp. 16:1—16:21, 2022.

Formalizing a diophantine description of the set of primes (short paper)
Karol Pąk, Cezary Kaliszyk
13th International Conference on Interactive Theorem Proving, ITP 2022,   pp. 26:1—26:8, 2022.

Learning Higher-Order Programs without Meta-Interpretive Learning
Stanisław Purgał, David Cerna, Cezary Kaliszyk
31st International Joint Conference on Artificial Intelligence, IJCAI 2022,   pp. 2726-2733, 2022.

Lash 1.0 (System Description)
Chad E. Brown, Cezary Kaliszyk
Automated Reasoning – 11th International Joint Conference, IJCAR 2022,   pp. 250-358, 2022.

Development Closed Critical Pairs: Towards a Formalized Proof
Christina Kohl, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022),   pp. 2-6, 2022.

Pólya’s Proof of the Weighted Arithmetic-Geometric Mean Inequality
Manuel Eberl
Archive of Formal Proofs 2022.

Formalized Signature Extension Results for Equivalence
Alexander Lochmann, Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 11th International Workshop on Confluence (IWC 2022),   pp. 42-47, 2022.

Polynomial Termination over N is Undecidable
Fabian Mitterwallner, Aart Middeldorp
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 228, pp. 27:1-27:17, 2022.

A Formalization of the Smith Normal Form in Higher-Order Logic
Jose Divasón, René Thiemann
Journal of Automated Reasoning online first, 2022.

Clique is not solvable by monotone circuits of polynomial size
René Thiemann
Archive of Formal Proofs 2022.

The Generalized Multiset Ordering is NP-Complete
René Thiemann, Lukas Schmidinger
Archive of Formal Proofs 2022.

The Sophomore’s Dream
Manuel Eberl
Archive of Formal Proofs 2022.

Adversarial Learning to Reason in an Arbitrary Logic
Stanisław Purgał and Cezary Kaliszyk
Proceedings of the Thirty-Fifth International Florida Artificial Intelligence Research Society Conference,  2022.

A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangen
Manuel Eberl
 2022.

First-Order Theory of Rewriting
Alexander Lochmann, Bertram Felgenhauer
Archive of Formal Proofs 2022 2022.

Duality of Linear Programming
René Thiemann
Archive of Formal Proofs 2022.