@inproceedings{spdcck-ijcai22,
 arxivurl = {https://arxiv.org/abs/2112.14603},
 author = {Stanisław Purgał and David Cerna and Cezary Kaliszyk},
 booktitle = {Proceedings of the Thirty-First International Joint Conference on
Artificial Intelligence, {IJCAI} 2022},
 doi = {10.24963/ijcai.2022/378},
 editor = {Luc De Raedt},
 pages = {2726--2733},
 publisher = {ijcai.org},
 title = {Learning Higher-Order Programs without Meta-Interpretive Learning},
 url = {https://doi.org/10.24963/ijcai.2022/378},
 year = {2022}
}



@inproceedings{cbck-ijcar22,
 arxivurl = {https://arxiv.org/abs/2205.06640},
 author = {Chad E. Brown and Cezary Kaliszyk},
 booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022},
 doi = {10.1007/978-3-031-10769-6\_21},
 editor = {Jasmin Blanchette and
Laura Kov{\'{a}}cs and
Dirk Pattinson},
 pages = {350--358},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Lash 1.0 (System Description)},
 url = {https://doi.org/10.1007/978-3-031-10769-6\_21},
 volume = {13385},
 year = {2022}
}



@inproceedings{spck-flairs22,
 arxivurl = {https://arxiv.org/abs/2204.02737},
 author = {Stanisław Purgał and Cezary Kaliszyk},
 booktitle = {Proceedings of the Thirty-Fifth International Florida Artificial Intelligence
Research Society Conference, {FLAIRS} 2022},
 doi = {10.32473/flairs.v35i.130648},
 editor = {Roman Bart{\'{a}}k and
Fazel Keshtkar and
Michael Franklin},
 title = {Adversarial Learning to Reason in an Arbitrary Logic},
 url = {https://doi.org/10.32473/flairs.v35i.130648},
 year = {2022}
}



@inproceedings{kpck-itp22,
 arxivurl = {http://arxiv.org/abs/2204.12311},
 author = {Karol P\k{a}k and Cezary Kaliszyk},
 booktitle = {13th International Conference on Interactive Theorem Proving, {ITP} 2022},
 doi = {10.4230/LIPIcs.ITP.2022.26},
 editor = {June Andronick and
Leonardo de Moura},
 pages = {16:1--16:21},
 publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 series = {LIPIcs},
 title = {Formalizing a diophantine description of the set of primes (short paper)},
 url = {https://doi.org/10.4230/LIPIcs.ITP.2022.26},
 volume = {237},
 year = {2022}
}



@inproceedings{zgjjckmojpju-itp22,
 author = {Zar Goerzel and Jan Jakubuv and Cezary Kaliszyk and Mirek Olsak and Jelle Piepenbroek and Josef Urban},
 booktitle = {13th International Conference on Interactive Theorem Proving, {ITP} 2022},
 doi = {10.4230/LIPIcs.ITP.2022.16},
 editor = {June Andronick and
Leonardo de Moura},
 pages = {16:1--16:21},
 publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 series = {LIPIcs},
 title = {The Isabelle Enigma},
 url = {https://doi.org/10.4230/LIPIcs.ITP.2022.16},
 volume = {237},
 year = {2022}
}



@inproceedings{gpck-paar22,
 arxivurl = {https://zenodo.org/record/7266150},
 author = {Grzegorz Prusak and Cezary Kaliszyk},
 booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022},
 editor = {Boris Konev and Claudia Schon and Alexander Steen},
 publisher = {CEUR-WS.org},
 series = {{CEUR} Workshop Proceedings},
 title = {Lazy Paramodulation in Practice},
 url = {http://ceur-ws.org/Vol-3201/paper3.pdf},
 volume = {3201},
 year = {2022}
}



@inproceedings{cbcktgju-fmbc22,
 author = {Chad E. Brown and Cezary Kaliszyk and Thibault Gauthier and Josef Urban},
 booktitle = {4th International Workshop on Formal Methods for Blockchains, FMBC 2022},
 doi = {10.4230/OASIcs.FMBC.2022.4},
 editor = {Zaynah Dargaye and Clara Schneidewind},
 pages = {4:1--4:15},
 publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 series = {OASIcs},
 title = {Proofgold: Blockchain for Formal Methods},
 url = {https://doi.org/10.4230/OASIcs.FMBC.2022.4},
 volume = {105},
 year = {2022}
}



@article{mb-ja22,
 arxivurl = {https://arxiv.org/abs/2105.10540},
 author = {Michal Buran},
 doi = {10.1016/j.jalgebra.2021.12.041},
 journal = {J. Algebra},
 title = {Separability and randomness in free groups},
 url = {https://doi.org/10.1016/j.jalgebra.2021.12.041},
 year = {2022}
}



@inproceedings{dmck-iclr21,
 arxivurl = {https://arxiv.org/abs/2101.11716},
 author = {Dennis M\"{u}ller and Cezary Kaliszyk},
 booktitle = {9th International Conference on Learning Representations, {ICLR} 2021},
 title = {Disambiguating Symbolic Expressions in Informal Documents},
 url = {https://openreview.net/forum?id=K5j7D81ABvt},
 year = {2021}
}



@inproceedings{qwck-frocos21,
 arxivurl = {https://arxiv.org/abs/2107.10188},
 author = {Qingxiang Wang and Cezary Kaliszyk},
 booktitle = {Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021},
 doi = {10.1007/978-3-030-86205-3\_9},
 editor = {Boris Konev and Giles Reger},
 pages = {154--170},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {JEFL: Joint Embedding of Formal Proof Libraries},
 url = {https://doi.org/10.1007/978-3-030-86205-3\_9},
 volume = {12941},
 year = {2021}
}



@inproceedings{zgkcjjmoju-frocos21,
 arxivurl = {https://arxiv.org/abs/2107.06750},
 author = {Zarathustra Amadeus Goertzel and
Karel Chvalovsk{\'{y}} and
Jan Jakub\r{u}v and
Miroslav Ol\v{s}{\'{a}}k and
Josef Urban},
 booktitle = {Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021},
 doi = {10.1007/978-3-030-86205-3\_10},
 editor = {Boris Konev and
Giles Reger},
 pages = {173--191},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Fast and Slow Enigmas and Parental Guidance},
 url = {https://doi.org/10.1007/978-3-030-86205-3\_10},
 volume = {12941},
 year = {2021}
}



@inproceedings{kcjjmoju-tableaux21,
 arxivurl = {https://arxiv.org/abs/2107.10034},
 author = {Karel Chvalovsk{\'{y}} and
Jan Jakub\r{u}v and
Miroslav Ol\v{s}{\'{a}}k and
Josef Urban},
 booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 30th
International Conference, {TABLEAUX} 2021},
 doi = {10.1007/978-3-030-86059-2\_16},
 editor = {Anupam Das and
Sara Negri},
 pages = {266--278},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Learning Theorem Proving Components},
 url = {https://doi.org/10.1007/978-3-030-86059-2\_16},
 volume = {12842},
 year = {2021}
}



@inproceedings{zzachmckju-tableaux21,
 arxivurl = {https://arxiv.org/abs/1905.13100},
 author = {Zsolt Zombori and Adri\'{a}n Csisz\'{a}rik and Henryk Michalewski and Cezary Kaliszyk and Josef Urban},
 booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, {TABLEAUX} 2021},
 doi = {10.1007/978-3-030-86059-2\_10},
 editor = {Anupam Das and Sara Negri},
 pages = {167--186},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Towards Finding Longer Proofs},
 url = {https://doi.org/10.1007/978-3-030-86059-2\_10},
 volume = {12842},
 year = {2021}
}



@inproceedings{jc-itp21,
 arxivurl = {https://arxiv.org/abs/2002.09282},
 author = {Joshua Chen},
 booktitle = {12th International Conference on Interactive Theorem Proving, {ITP} 2021},
 doi = {10.4230/LIPIcs.ITP.2021.12},
 pages = {12:1--12:8},
 publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 series = {LIPIcs},
 title = {Homotopy Type Theory in Isabelle},
 url = {https://doi.org/10.4230/LIPIcs.ITP.2021.12},
 volume = {193},
 year = {2021}
}



@inproceedings{jmjsmojujs-cicm21,
 arxivurl = {https://arxiv.org/abs/2106.14195},
 author = {Jaroslav Macke and
Jir{\'{\i}} Sedl{\'{a}}r and
Miroslav Ols{\'{a}}k and
Josef Urban and
Josef Sivic},
 booktitle = {Intelligent Computer Mathematics - 14th International Conference, {CICM} 2021},
 doi = {10.1007/978-3-030-81097-9\_14},
 pages = {167--184},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Learning to Solve Geometric Construction Problems from Images},
 url = {https://doi.org/10.1007/978-3-030-81097-9\_14},
 volume = {12833},
 year = {2021}
}



@inproceedings{jjmjar-smt21,
 author = {Jan Jakubuv and
Mikol{\'{a}}s Janota and
Andrew Reynolds},
 booktitle = {Proceedings of the 19th International Workshop on Satisfiability Modulo
Theories co-located with 33rd International Conference on Computer
Aided Verification (CAV 2021)},
 editor = {Alexander Nadel and
Aina Niemetz},
 pages = {53--63},
 publisher = {CEUR-WS.org},
 series = {{CEUR} Workshop Proceedings},
 title = {Characteristic Subsets of {SMT-LIB} Benchmarks},
 url = {http://ceur-ws.org/Vol-2908/paper7.pdf},
 volume = {2908},
 year = {2021}
}



@inproceedings{lzlbbppcckju-cicm21,
 arxivurl = {https://arxiv.org/abs/2104.05207},
 author = {Liao Zhang and
Lasse Blaauwbroek and
Bartosz Piotrowski and
Prokop Cern{\'{y}} and
Cezary Kaliszyk and
Josef Urban},
 booktitle = {Intelligent Computer Mathematics - 14th International Conference, {CICM} 2021},
 doi = {10.1007/978-3-030-81097-9\_5},
 editor = {Fairouz Kamareddine and
Claudio Sacerdoti Coen},
 pages = {67--83},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Online Machine Learning Techniques for Coq: {A} Comparison},
 url = {https://doi.org/10.1007/978-3-030-81097-9\_5},
 volume = {12833},
 year = {2021}
}



@article{spjpck-jlc21,
 arxivurl = {https://arxiv.org/abs/2101.09142},
 author = {Stanisław Purgał and Julian Parsert and Cezary Kaliszyk},
 doi = {10.1093/logcom/exab006},
 issn = {0955-792X},
 journal = {Journal of Logic and Computation},
 month = {02},
 title = {A study of continuous vector representations for theorem proving},
 url = {https://doi.org/10.1093/logcom/exab006},
 year = {2021}
}



@article{tgckjurkmn-jar21,
 arxivurl = {https://arxiv.org/abs/1804.00596},
 author = {Thibault Gauthier and
Cezary Kaliszyk and
Josef Urban and
Ramana Kumar and
Michael Norrish},
 doi = {10.1007/s10817-020-09580-x},
 journal = {J. Autom. Reason.},
 number = {2},
 pages = {257--286},
 title = {{TacticToe}: {L}earning to Prove with Tactics},
 url = {https://doi.org/10.1007/s10817-020-09580-x},
 volume = {65},
 year = {2021}
}



@article{mfckju-jar21,
 arxivurl = {https://arxiv.org/abs/1805.03107},
 author = {Michael F{\"{a}}rber and
Cezary Kaliszyk and
Josef Urban},
 doi = {10.1007/s10817-020-09576-7},
 journal = {J. Autom. Reason.},
 number = {2},
 pages = {287--320},
 title = {Machine Learning Guidance for Connection Tableaux},
 url = {https://doi.org/10.1007/s10817-020-09576-7},
 volume = {65},
 year = {2021}
}



@inproceedings{yn-ijcai21,
 arxivurl = {https://arxiv.org/abs/2009.09215},
 author = {Yutaka Nagashima},
 booktitle = {International Joint Conference on Artificial Intelligence, {IJCAI} 2021},
 doi = {10.24963/ijcai.2021/273},
 editor = {Zhi{-}Hua Zhou},
 pages = {1981--1988},
 publisher = {ijcai.org},
 title = {Faster Smarter Proof by Induction in Isabelle/HOL},
 url = {https://doi.org/10.24963/ijcai.2021/273},
 year = {2021}
}



@inproceedings{zzjumo-tableaux21,
 arxivurl = {https://arxiv.org/abs/2105.14706},
 author = {Zsolt Zombori and
Josef Urban and
Miroslav Ols{\'{a}}k},
 booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 30th
International Conference, {TABLEAUX} 2021},
 doi = {10.1007/978-3-030-86059-2\_13},
 editor = {Anupam Das and
Sara Negri},
 pages = {218--235},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {The Role of Entropy in Guiding a Connection Prover},
 url = {https://doi.org/10.1007/978-3-030-86059-2\_13},
 volume = {12842},
 year = {2021}
}



@inproceedings{jjkcmobpmsjo-ijcar20,
 arxivurl = {https://arxiv.org/abs/2002.05406},
 author = {Jan Jakubuv and
Karel Chvalovsk{\'{y}} and
Miroslav Ols{\'{a}}k and
Bartosz Piotrowski and
Martin Suda and
Josef Urban},
 booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR} 2020},
 doi = {10.1007/978-3-030-51054-1\_29},
 pages = {448--463},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {{ENIGMA} Anonymous: Symbol-Independent Inference Guiding Machine (System
Description)},
 url = {https://doi.org/10.1007/978-3-030-51054-1\_29},
 volume = {12167},
 year = {2020}
}



@inproceedings{mockju-ecai20,
 arxivurl = {https://arxiv.org/abs/1911.12073},
 author = {Miroslav Ols{\'{a}}k and
Cezary Kaliszyk and
Josef Urban},
 booktitle = {24th European Conference on Artificial Intelligence, {ECAI} 2020},
 doi = {10.3233/FAIA200244},
 editor = {Giuseppe De Giacomo and
Alejandro Catal{\'{a}} and
Bistra Dilkina and
Michela Milano and
Sen{\'{e}}n Barro and
Alberto Bugar{\'{\i}}n and
J{\'{e}}r{\^{o}}me Lang},
 pages = {1395--1402},
 publisher = {{IOS} Press},
 series = {Frontiers in Artificial Intelligence and Applications},
 title = {Property Invariant Embedding for Automated Reasoning},
 url = {https://doi.org/10.3233/FAIA200244},
 volume = {325},
 year = {2020}
}



@article{jjck-mcs20,
 author = {Jan Jakubuv and
Cezary Kaliszyk},
 doi = {10.1007/s11786-020-00474-0},
 journal = {Math. Comput. Sci.},
 number = {3},
 pages = {657--670},
 title = {Relaxed Weighted Path Order in Theorem Proving},
 url = {https://doi.org/10.1007/s11786-020-00474-0},
 volume = {14},
 year = {2020}
}



@inproceedings{mo-icms20,
 arxivurl = {https://arxiv.org/abs/2005.03586},
 author = {Miroslav Ols{\'{a}}k},
 booktitle = {7th International Conference on Mathematical Software - {ICMS} 2020},
 doi = {10.1007/978-3-030-52200-1\_26},
 pages = {263--271},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry},
 url = {https://doi.org/10.1007/978-3-030-52200-1\_26},
 volume = {12097},
 year = {2020}
}



@article{beck-mcs20,
 author = {Burak Ekici and
Cezary Kaliszyk},
 doi = {10.1007/s11786-020-00450-8},
 journal = {Math. Comput. Sci.},
 number = {3},
 pages = {533--549},
 title = {{M}ac {L}ane's Comparison Theorem for the {K}leisli Construction Formalized
in {C}oq},
 url = {https://doi.org/10.1007/s11786-020-00450-8},
 volume = {14},
 year = {2020}
}



@inproceedings{qwcbckju-cpp20,
 arxivurl = {https://arxiv.org/abs/1912.02636},
 author = {Qingxiang Wang and
Chad E. Brown and
Cezary Kaliszyk and
Josef Urban},
 booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020},
 doi = {10.1145/3372885.3373827},
 editor = {Jasmin Blanchette and
Catalin Hritcu},
 pages = {85--98},
 publisher = {{ACM}},
 title = {Exploration of neural machine translation in autoformalization of
mathematics in {M}izar},
 url = {https://doi.org/10.1145/3372885.3373827},
 year = {2020}
}



@inproceedings{ckfr-cicm20,
 arxivurl = {https://arxiv.org/abs/2005.12876},
 author = {Cezary Kaliszyk and Florian Rabe},
 booktitle = {Intelligent Computer Mathematics (CICM 2020)},
 doi = {10.1007/978-3-030-53518-6\_9},
 editor = {Benzmueller C., Miller B.},
 pages = {138--156},
 publisher = {Springer, Cham},
 series = {LNCS},
 title = {A Survey of Languages for Formalizing Mathematics},
 url = {https://doi.org/10.1007/978-3-030-53518-6\_9},
 volume = {12236},
 year = {2020}
}



@inproceedings{jpsack-gcai20,
 author = {Julian Parsert and Stephanie Autherith and Cezary Kaliszyk},
 booktitle = {6th Global Conference on Artificial Intelligence (GCAI 2020)},
 doi = {10.29007/18t1},
 editor = {Gregoire Danoy and Jun Pang and Geoff Sutcliffe},
 pages = {70--82},
 publisher = {EasyChair},
 series = {EPiC Series in Computing},
 title = {Property Preserving Embedding of First-order Logic},
 url = {https://easychair.org/publications/paper/Cwgq},
 volume = {72},
 year = {2020}
}



@inproceedings{sp-ijcnn20,
 author = {Stanislaw Purgal},
 booktitle = {2020 International Joint Conference on Neural Networks, {IJCNN} 2020},
 doi = {10.1109/IJCNN48605.2020.9206591},
 pages = {1--7},
 publisher = {{IEEE}},
 title = {Improving Expressivity of Graph Neural Networks},
 url = {https://doi.org/10.1109/IJCNN48605.2020.9206591},
 year = {2020}
}



@inproceedings{mfck-tableaux19,
 author = {Michael Färber and Cezary Kaliszyk},
 booktitle = {28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019)},
 doi = {10.1007/978-3-030-29026-9\_2},
 editor = {Serenella Cerrito and
Andrei Popescu},
 pages = {21--38},
 publisher = {Springer},
 series = {LNCS},
 title = {Certification of Nonclausal Connection Tableaux Proofs},
 url = {https://doi.org/10.1007/978-3-030-29026-9\_2},
 volume = {11714},
 year = {2019}
}



@inproceedings{cbtgckgsju-cade19,
 arxivurl = {https://arxiv.org/abs/1903.02539},
 author = {Chad Brown and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban},
 booktitle = {The 27th International Conference on Automated Deduction (CADE 2019)},
 doi = {10.1007/978-3-030-29436-6\_8},
 editor = {Pascal Fontaine},
 pages = {123--141},
 publisher = {Springer},
 series = {LNCS},
 title = {{GRUNGE:} {A} Grand Unified {ATP} Challenge},
 url = {https://doi.org/10.1007/978-3-030-29436-6\_8},
 volume = {11716},
 year = {2019}
}



@inproceedings{beavyzcbct-eptcs19,
 arxivurl = {https://arxiv.org/abs/1908.09478},
 author = {Burak Ekici and
Arjun Viswanathan and
Yoni Zohar and
Clark W. Barrett and
Cesare Tinelli},
 booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving,
PxTP 2019},
 doi = {10.4204/EPTCS.301.4},
 editor = {Giselle Reis and
Haniel Barbosa},
 pages = {18--26},
 series = {{EPTCS}},
 title = {Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)},
 url = {https://doi.org/10.4204/EPTCS.301.4},
 volume = {301},
 year = {2019}
}



@article{jpck-afp19,
 author = {Julian Parsert and
Cezary Kaliszyk},
 journal = {Arch. Formal Proofs},
 title = {Linear Programming},
 url = {https://www.isa-afp.org/entries/Linear\_Programming.html},
 volume = {2019},
 year = {2019}
}



@article{tgck-jsc19,
 author = {Thibault Gauthier and Cezary Kaliszyk},
 doi = {10.1016/j.jsc.2018.04.005},
 journal = {J. Symbolic Computation},
 pages = {89--123},
 title = {Aligning Concepts across Proof Assistant Libraries},
 url = {https://doi.org/10.1016/j.jsc.2018.04.005},
 volume = {90},
 year = {2019}
}



@inproceedings{ckkp-itp19,
 author = {Cezary Kaliszyk and Karol Pąk},
 booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
 doi = {10.4230/LIPIcs.ITP.2019.35},
 editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
 pages = {35:1--35:7},
 series = {LIPIcs},
 title = {Declarative Proof Translation (short paper)},
 url = {https://doi.org/10.4230/LIPIcs.ITP.2019.35},
 volume = {141},
 year = {2019}
}



@inproceedings{cbckkp-itp19,
 author = {Chad Brown and Cezary Kaliszyk and Karol Pąk},
 booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
 doi = {10.4230/LIPIcs.ITP.2019.9},
 editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
 pages = {9:1--9:16},
 publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 series = {LIPIcs},
 title = {Higher-order {T}arski {G}rothendieck as a Foundation for Formal Proof},
 url = {https://doi.org/10.4230/LIPIcs.ITP.2019.9},
 volume = {141},
 year = {2019}
}



@article{ckkp-jar19,
 author = {Cezary Kaliszyk and Karol P\k{a}k},
 doi = {10.1007/s10817-018-9479-z},
 journal = {J. Autom. Reasoning},
 number = {3},
 pages = {557--595},
 title = {Semantics of {M}izar as an {I}sabelle Object Logic},
 url = {https://doi.org/10.1007/s10817-018-9479-z},
 volume = {63},
 year = {2019}
}



@incollection{bpjucbck-lrgsr19,
 archiveprefix = {arXiv},
 author = {Bartosz Piotrowski and Josef Urban and Chad Brown and Cezary Kaliszyk},
 booktitle = {Learning and Reasoning with Graph-Structured Representations -- ICML 2019 Workshop},
 eprint = {1911.04873},
 pages = {1--4},
 title = {Can Neural Networks Learn Symbolic Rewriting?},
 url = {https://graphreason.github.io/papers/40.pdf},
 year = {2019}
}



@article{lcck-jar18,
 author = {\L{}ukasz Czajka and Cezary Kaliszyk},
 doi = {10.1007/s10817-018-9458-4},
 journal = {J. Autom. Reasoning},
 number = {1-4},
 pages = {423--453},
 title = {Hammer for {C}oq: Automation for Dependent Type Theory},
 url = {https://doi.org/10.1007/s10817-018-9458-4},
 volume = {61},
 year = {2018}
}



@incollection{ckjuhmmo-nips18,
 arxivurl = {https://arxiv.org/abs/1805.07563},
 author = {Kaliszyk, Cezary and Urban, Josef and Michalewski, Henryk and Ol\v{s}\'{a}k, Miroslav},
 booktitle = {Advances in Neural Information Processing Systems 31},
 editor = {S. Bengio and H. Wallach and H. Larochelle and K. Grauman and N. Cesa-Bianchi and R. Garnett},
 pages = {8836--8847},
 publisher = {Curran Associates, Inc.},
 title = {Reinforcement Learning of Theorem Proving},
 url = {http://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf},
 year = {2018}
}



@inproceedings{lcck-coqpl18,
 author = {\L{}ukasz Czajka and
Cezary Kaliszyk},
 booktitle = {Fourth International Workshop on Coq for Programming Languages, CoqPL 2018},
 title = {{CoqHammer}: Strong Automation for Program Verification},
 url = {https://popl18.sigplan.org/details/CoqPL-2018/2/CoqHammer-Strong-Automation-for-Program-Verification},
 year = {2018}
}



@inproceedings{be-cicm18,
 author = {Burak Ekici},
 booktitle = {FMM 2018 - Third workshop on Formal Mathematics for Mathematicians},
 publisher = {CEUR-WS.org},
 series = {{CEUR} Workshop Proceedings},
 title = {Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction
in Coq},
 url = {http://ceur-ws.org/Vol-2307/paper11.pdf},
 volume = {2307},
 year = {2018}
}



@article{be-dmtcs18,
 arxivurl = {https://arxiv.org/abs/1503.05496},
 author = {Burak Ekici},
 journal = {Discret. Math. Theor. Comput. Sci.},
 number = {2},
 title = {{IMP} with exceptions over decorated logic},
 url = {http://dmtcs.episciences.org/4927},
 volume = {20},
 year = {2018}
}



@inproceedings{ynjp-cicm18,
 arxivurl = {https://arxiv.org/abs/1806.04774},
 author = {Yutaka Nagashima and
Julian Parsert},
 booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
 doi = {10.1007/978-3-319-96812-4\_19},
 pages = {225--231},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Goal-Oriented Conjecturing for Isabelle/HOL},
 url = {https://doi.org/10.1007/978-3-319-96812-4\_19},
 volume = {11006},
 year = {2018}
}



@article{jpck-afp18,
 author = {Julian Parsert and
Cezary Kaliszyk},
 journal = {Arch. Formal Proofs},
 title = {Von-Neumann-Morgenstern Utility Theorem},
 url = {https://www.isa-afp.org/entries/Neumann\_Morgenstern\_Utility.html},
 volume = {2018},
 year = {2018}
}



@inproceedings{jjck-icms18,
 author = {Jan Jakubuv and Cezary Kaliszyk},
 booktitle = {6th International Conference on Mathematical Software (ICMS 2018)},
 doi = {10.1007/978-3-319-96418-8\_29},
 editor = {James H. Davenport and
Manuel Kauers and
George Labahn and
Josef Urban},
 pages = {245--254},
 publisher = {Springer},
 series = {LNCS},
 title = {Towards a Unified Ordering for Superposition-Based Automated Reasoning},
 url = {https://doi.org/10.1007/978-3-319-96418-8\_29},
 volume = {10931},
 year = {2018}
}



@inproceedings{lcbeck-cicm18,
 arxivurl = {https://arxiv.org/abs/1808.06413},
 author = {\L{}ukasz Czajka and
Burak Ekici and
Cezary Kaliszyk},
 booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
 doi = {10.1007/978-3-319-96812-4\_5},
 editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
 pages = {53--58},
 publisher = {Springer},
 series = {LNCS},
 title = {Concrete Semantics with {C}oq and {CoqH}ammer},
 url = {https://doi.org/10.1007/978-3-319-96812-4\_5},
 volume = {11006},
 year = {2018}
}



@inproceedings{ckkp-cicm18,
 author = {Cezary Kaliszyk and Karol P\k{a}k},
 booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
 doi = {10.1007/978-3-319-96812-4\_13},
 editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
 pages = {131--146},
 publisher = {Springer},
 series = {LNCS},
 title = {Isabelle Import Infrastructure for the {M}izar Mathematical Library},
 url = {https://doi.org/10.1007/978-3-319-96812-4\_13},
 volume = {11006},
 year = {2018}
}



@inproceedings{qwckju-cicm18,
 arxivurl = {https://arxiv.org/abs/1805.06502},
 author = {Qingxiang Wang and
Cezary Kaliszyk and
Josef Urban},
 booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
 doi = {10.1007/978-3-319-96812-4\_22},
 editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
 pages = {255--270},
 publisher = {Springer},
 series = {LNCS},
 title = {First Experiments with Neural Translation of Informal to Formal Mathematics},
 url = {https://doi.org/10.1007/978-3-319-96812-4\_22},
 volume = {11006},
 year = {2018}
}



@inproceedings{jpck-itp18,
 author = {Julian Parsert and
Cezary Kaliszyk},
 booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP} 2018},
 doi = {10.1007/978-3-319-94821-8\_29},
 editor = {Jeremy Avigad and
Assia Mahboubi},
 pages = {495--503},
 publisher = {Springer},
 series = {LNCS},
 title = {Towards Formal Foundations for Game Theory},
 url = {https://doi.org/10.1007/978-3-319-94821-8\_29},
 volume = {10895},
 year = {2018}
}



@inproceedings{jpck-cpp18,
 author = {Julian Parsert and Cezary Kaliszyk},
 booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs (CPP 2018)},
 doi = {10.1145/3167100},
 editor = {June Andronick and Amy P. Felty},
 pages = {91-101},
 publisher = {{ACM}},
 title = {Formal Microeconomic Foundations and the {First Welfare Theorem}},
 url = {http://doi.acm.org/10.1145/3167100},
 year = {2018}
}



@inproceedings{mfckju-cade17,
 arxivurl = {https://arxiv.org/abs/1611.05990},
 author = {Michael F{\"{a}}rber and
Cezary Kaliszyk and
Josef Urban},
 booktitle = {26th International Conference on Automated Deduction (CADE 2017)},
 doi = {10.1007/978-3-319-63046-5\_34},
 editor = {Leonardo de Moura},
 pages = {563--579},
 publisher = {Springer},
 series = {LNCS},
 title = {{M}onte {C}arlo Tableau Proof Search},
 url = {https://doi.org/10.1007/978-3-319-63046-5\_34},
 volume = {10395},
 year = {2017}
}



@inproceedings{ckkp-macis17,
 author = {Cezary Kaliszyk and Karol Pak},
 booktitle = {International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017)},
 doi = {10.1007/978-3-319-72453-9\_12},
 editor = {Blömer J. and Kotsireas I. and Kutsia T. and Simos D.},
 pages = {163--178},
 publisher = {Springer},
 series = {LNCS},
 title = {Isabelle Formalization of Set Theoretic Structures and Set Comprehensions},
 volume = {10693},
 year = {2017}
}



@inproceedings{ckjujv-synasc17,
 author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
 booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017},
 editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephen M. Watt},
 pages = {169--172},
 publisher = {{IEEE} Computer Society},
 title = {System Description: Statistical Parsing of Informalized {M}izar Formulas},
 year = {2017}
}



@inproceedings{ckjujv-itp17,
 author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
 booktitle = {8th International Conference on Interactive Theorem Proving (ITP 2017)},
 doi = {10.1007/978-3-319-66107-0\_2},
 editor = {Mauricio Ayala{-}Rinc{\'{o}}n and C{\'{e}}sar A. Mu{\~{n}}oz},
 pages = {12--27},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 title = {Automating Formalization by Statistical and Semantic Parsing of Mathematics},
 url = {https://doi.org/10.1007/978-3-319-66107-0\_2},
 volume = {10499},
 year = {2017}
}



@article{jpck-afp17,
 author = {Julian Parsert and
Cezary Kaliszyk},
 journal = {Arch. Formal Proofs},
 title = {Microeconomics and the First Welfare Theorem},
 url = {https://www.isa-afp.org/entries/First\_Welfare\_Theorem.html},
 volume = {2017},
 year = {2017}
}



@inproceedings{ckfccs-iclr17,
 arxivurl = {https://arxiv.org/abs/1703.00426},
 author = {Cezary Kaliszyk and
Fran{\c{c}}ois Chollet and
Christian Szegedy},
 booktitle = {5th International Conference on Learning Representations, {ICLR} 2017,
Toulon, France, April 24-26, 2017, Conference Track Proceedings},
 title = {{HolStep}: {A} Machine Learning Dataset for Higher-order Logic Theorem
Proving},
 url = {https://openreview.net/forum?id=ryuxYmvel},
 year = {2017}
}



@inproceedings{slgicsck-lpar17,
 arxivurl = {https://arxiv.org/abs/1701.06972},
 author = {Sarah Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk},
 booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 doi = {10.29007/8mwc},
 editor = {Thomas Eiter and David Sands},
 issn = {2398-7340},
 pages = {85--105},
 publisher = {EasyChair},
 series = {EPiC Series in Computing},
 title = {Deep Network Guided Proof Search},
 url = {https://doi.org/10.29007/8mwc},
 volume = {46},
 year = {2017}
}



@inproceedings{ckkp-fedcsis17,
 author = {Cezary Kaliszyk and
Karol P\k{a}k},
 booktitle = {Proceedings of the 2017 Federated Conference on Computer Science and
Information Systems, FedCSIS 2017},
 doi = {10.15439/2017F289},
 editor = {Maria Ganzha and
Leszek A. Maciaszek and
Marcin Paprzycki},
 pages = {227--236},
 title = {Progress in the Independent Certification of {M}izar {M}athematical {L}ibrary
in {I}sabelle},
 url = {https://doi.org/10.15439/2017F289},
 year = {2017}
}



@inproceedings{ckkp-cicm17,
 author = {Cezary Kaliszyk and Karol Pak},
 booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
 doi = {10.1007/978-3-319-62075-6\_14},
 editor = {Herman Geuvers and
Matthew England and
Osman Hasan and
Florian Rabe and
Olaf Teschke},
 pages = {193--207},
 publisher = {Springer},
 series = {LNCS},
 title = {Presentation and Manipulation of {M}izar Properties in an {I}sabelle Object Logic},
 volume = {10383},
 year = {2017}
}



@inproceedings{dmtgckmkfr-cicm17,
 author = {Dennis M{\"{u}}ller and
Thibault Gauthier and
Cezary Kaliszyk and
Michael Kohlhase and
Florian Rabe},
 booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
 doi = {10.1007/978-3-319-62075-6\_7},
 editor = {Herman Geuvers and
Matthew England and
Osman Hasan and
Florian Rabe and
Olaf Teschke},
 pages = {83--98},
 publisher = {Springer},
 series = {LNCS},
 title = {Classification of Alignments Between Concepts of Formal Mathematical
Systems},
 volume = {10383},
 year = {2017}
}



@inproceedings{tgckju-lpar17,
 arxivurl = {https://arxiv.org/abs/1804.00595},
 author = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban},
 booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 doi = {10.29007/ntlb},
 editor = {Thomas Eiter and David Sands},
 issn = {2398-7340},
 pages = {125--143},
 publisher = {EasyChair},
 series = {EPiC Series in Computing},
 title = {{TacticToe}: Learning to Reason with {HOL4} Tactics},
 url = {https://doi.org/10.29007/ntlb},
 volume = {46},
 year = {2017}
}