@inproceedings{lzfmjjck-ijcai25,
arxivurl = {https://arxiv.org/abs/2411.06409},
author = {Liao Zhang and Fabian Mitterwallner and Jan Jakubuv and Cezary Kaliszyk},
booktitle = {IJCAI 2025},
note = { accepted},
title = {Automated Strategy Invention for Confluence of Term Rewrite Systems},
year = {2025}
}
@inproceedings{drckfrgs-frocos25,
arxivurl = {https://doi.org/10.48550/arXiv.2507.03208},
author = {Daniel Ranalter and
Cezary Kaliszyk and
Florian Rabe and
Geoff Sutcliffe},
booktitle = {FroCoS 2025},
note = {accepted},
title = {The Dependently Typed Higher-Order Form for the {TPTP} World},
year = {2025}
}
@inproceedings{cbckmsju-cicm25,
arxivurl = {https://arxiv.org/abs/2509.08264},
author = {Chad E. Brown and Cezary Kaliszyk and Martin Suda and Josef Urban},
booktitle = {CICM 2025},
note = {accepted},
title = {Hammering Higher Order Set Theory},
year = {2025}
}
@inproceedings{cbckju-cicm25,
arxivurl = {https://arxiv.org/abs/2509.08267},
author = {Chad E. Brown and Cezary Kaliszyk and Josef Urban},
booktitle = {CICM 2025},
note = {accepted},
title = {Exploring Formal Math on the Blockchain: An Explorer for Proofgold},
year = {2025}
}
@inproceedings{xzrzlzsd-colm25,
arxivurl = {https://arxiv.org/abs/2410.14706},
author = {Xiyu Zhai and Runlong Zhou and Liao Zhang and Simon Shaolei Du},
booktitle = {COLM 2025},
note = {accepted},
title = {Transformers are Efficient Compilers, Provably},
year = {2025}
}
@inproceedings{cbckju-bcca25,
arxivurl = {https://arxiv.org/abs/2509.08268},
author = {Chad E. Brown and Cezary Kaliszyk and Josef Urban},
booktitle = {BCCA 2025},
note = {accepted},
title = {Payment Channels with Proofs},
year = {2025}
}
@inproceedings{jncbck-ijcar24,
arxivurl = {https://arxiv.org/abs/2410.14232},
author = {Johannes Niederhauser and
Chad E. Brown and
Cezary Kaliszyk},
booktitle = {{IJCAR}},
doi = {10.1007/978-3-031-63498-7\_6},
editor = {Christoph Benzm{\"{u}}ller and
Marijn J. H. Heule and
Renate A. Schmidt},
pages = {86--104},
series = {LNCS},
title = {Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic},
url = {https://doi.org/10.1007/978-3-031-63498-7\_6},
volume = {14739},
year = {2024}
}
@inproceedings{kajjck-lpar24,
arxivurl = {https://zenodo.org/records/17089812},
author = {Kristina Aleksandrova and
Jan Jakub\r{u}v and
Cezary Kaliszyk},
booktitle = {{LPAR}},
doi = {10.29007/SD6T},
editor = {Nikolaj S. Bj{\o}rner and
Marijn Heule and
Andrei Voronkov},
pages = {360--369},
publisher = {EasyChair},
series = {EPiC Series in Computing},
title = {Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery},
url = {https://doi.org/10.29007/sd6t},
volume = {100},
year = {2024}
}
@inproceedings{drcbck-lpar24,
arxivurl = {https://arxiv.org/abs/2410.08874},
author = {Daniel Ranalter and
Chad E. Brown and
Cezary Kaliszyk},
booktitle = {{LPAR}},
doi = {10.29007/2V8H},
editor = {Nikolaj S. Bj{\o}rner and
Marijn Heule and
Andrei Voronkov},
pages = {311--320},
publisher = {EasyChair},
series = {EPiC Series in Computing},
title = {Experiments with Choice in Dependently-Typed Higher-Order Logic},
url = {https://doi.org/10.29007/2v8h},
volume = {100},
year = {2024}
}
@inproceedings{jjmjju-cicm24,
arxivurl = {https://arxiv.org/abs/2406.17762},
author = {Jan Jakubův and Mikoláš Janota and Josef Urban},
booktitle = {Intelligent Computer Mathematics - 17th International Conference, {CICM} 2024},
doi = {10.1007/978-3-031-66997-2\_18},
editor = {Andrea Kohlhase and
Laura Kov{\'{a}}cs},
pages = {315--333},
publisher = {Springer},
series = {LNCS},
title = {Solving Hard Mizar Problems with Instantiation and Strategy Invention},
url = {https://doi.org/10.1007/978-3-031-66997-2\_18},
volume = {14960},
year = {2024}
}
@inproceedings{yljpep-cav24,
arxivurl = {https://arxiv.org/abs/2403.03997},
author = {Yixuan Li and
Julian Parsert and
Elizabeth Polgreen},
booktitle = {{CAV}},
doi = {10.1007/978-3-031-65630-9\_15},
editor = {Arie Gurfinkel and
Vijay Ganesh},
pages = {280--301},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Guiding Enumerative Program Synthesis with Large Language Models},
url = {https://doi.org/10.1007/978-3-031-65630-9\_15},
volume = {14682},
year = {2024}
}
@inproceedings{kpck-itp24,
arxivurl = {https://arxiv.org/abs/2410.00065},
author = {Karol P\k{a}k and Cezary Kaliszyk},
booktitle = {{ITP}},
doi = {10.4230/LIPICS.ITP.2024.29},
editor = {Yves Bertot and
Temur Kutsia and
Michael Norrish},
pages = {29:1--29:18},
series = {LIPIcs},
title = {Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers},
url = {https://doi.org/10.4230/LIPIcs.ITP.2024.29},
volume = {309},
year = {2024}
}
@inproceedings{lbdctgjjckmsju-geuvers24,
arxivurl = {https://arxiv.org/abs/2403.04017},
author = {Lasse Blaauwbroek and
David M. Cerna and
Thibault Gauthier and
Jan Jakubuv and
Cezary Kaliszyk and
Martin Suda and
Josef Urban},
booktitle = {Logics and Type Systems in Theory and Practice - Essays Dedicated
to Herman Geuvers on The Occasion of His 60th Birthday},
doi = {10.1007/978-3-031-61716-4\_4},
editor = {Venanzio Capretta and
Robbert Krebbers and
Freek Wiedijk},
pages = {54--83},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Learning Guided Automated Reasoning: {A} Brief Survey},
url = {https://doi.org/10.1007/978-3-031-61716-4\_4},
volume = {14560},
year = {2024}
}
@inproceedings{jjmjjpju-ecai24,
arxivurl = {https://doi.org/10.48550/arXiv.2408.14338},
author = {Jan Jakubuv and
Mikol{\'{a}}s Janota and
Jelle Piepenbrock and
Josef Urban},
booktitle = {{ECAI} 2024},
doi = {10.3233/FAIA241009},
editor = {Ulle Endriss and
Francisco S. Melo and
Kerstin Bach and
Alberto Jos{\'{e}} Bugar{\'{\i}}n Diz and
Jose Maria Alonso{-}Moral and
Sen{\'{e}}n Barro and
Fredrik Heintz},
pages = {4336--4343},
publisher = {{IOS} Press},
series = {Frontiers in Artificial Intelligence and Applications},
title = {Machine Learning for Quantifier Selection in cvc5},
url = {https://doi.org/10.3233/FAIA241009},
volume = {392},
year = {2024}
}