Home Summary Team Publications

Publications

2025

Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang and Fabian Mitterwallner and Jan Jakubuv and Cezary Kaliszyk
IJCAI 2025
BibTeX arXiv preprint
The Dependently Typed Higher-Order Form for the TPTP World
Daniel Ranalter and Cezary Kaliszyk and Florian Rabe and Geoff Sutcliffe
FroCoS 2025
BibTeX arXiv preprint
Hammering Higher Order Set Theory
Chad E. Brown and Cezary Kaliszyk and Martin Suda and Josef Urban
CICM 2025
BibTeX arXiv preprint
Exploring Formal Math on the Blockchain: An Explorer for Proofgold
Chad E. Brown and Cezary Kaliszyk and Josef Urban
CICM 2025
BibTeX arXiv preprint
Transformers are Efficient Compilers, Provably
Xiyu Zhai and Runlong Zhou and Liao Zhang and Simon Shaolei Du
COLM 2025
BibTeX arXiv preprint
Payment Channels with Proofs
Chad E. Brown and Cezary Kaliszyk and Josef Urban
BCCA 2025
BibTeX arXiv preprint

2024

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Johannes Niederhauser and Chad E. Brown and Cezary Kaliszyk
IJCAR, 2024
BibTeX Publisher arXiv preprint
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Kristina Aleksandrova and Jan Jakubův and Cezary Kaliszyk
LPAR, 2024
BibTeX Publisher arXiv preprint
Experiments with Choice in Dependently-Typed Higher-Order Logic
Daniel Ranalter and Chad E. Brown and Cezary Kaliszyk
LPAR, 2024
BibTeX Publisher arXiv preprint
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Jan Jakubův and Mikoláš Janota and Josef Urban
Intelligent Computer Mathematics - 17th International Conference, CICM 2024
BibTeX Publisher arXiv preprint
Guiding Enumerative Program Synthesis with Large Language Models
Yixuan Li and Julian Parsert and Elizabeth Polgreen
CAV, 2024
BibTeX Publisher arXiv preprint
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
Karol Pąk and Cezary Kaliszyk
ITP, 2024
BibTeX Publisher arXiv preprint
Learning Guided Automated Reasoning: A Brief Survey
Lasse Blaauwbroek and David M. Cerna and Thibault Gauthier and Jan Jakubuv and Cezary Kaliszyk and Martin Suda and Josef Urban
Logics and Type Systems in Theory and Practice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday, 2024
BibTeX Publisher arXiv preprint
Machine Learning for Quantifier Selection in cvc5
Jan Jakubuv and Mikolás Janota and Jelle Piepenbrock and Josef Urban
ECAI 2024
BibTeX Publisher arXiv preprint