@inproceedings{jpcbmjck-lpar23,
author = {Julian Parsert and Chad E. Brown and Mikolas Janota and Cezary Kaliszyk},
editor = {Ruzica Piskac and Andrei Voronkov},
title = {Experiments on Infinite Model Finding in {SMT} Solving},
booktitle = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
for Programming, Artificial Intelligence and Reasoning},
series = {EPiC},
volume = {94},
pages = {317--328},
publisher = {EasyChair},
year = {2023},
url = {https://doi.org/10.29007/slrm},
doi = {10.29007/SLRM},
}
@article{ckkp-jar23,
author = {Cezary Kaliszyk and Karol Pąk},
title = {Combining Higher-Order Logic with Set Theory Formalizations},
journal = {J. Autom. Reason.},
volume = {67},
number = {2},
pages = {20},
year = {2023},
url = {https://doi.org/10.1007/s10817-023-09663-5},
doi = {10.1007/S10817-023-09663-5},
}
@inproceedings{jjkczgckmobpssmsju-itp23,
author = {Jan Jakubuv and
Karel Chvalovsk{\'{y}} and
Zarathustra Amadeus Goertzel and
Cezary Kaliszyk and
Mirek Ols{\'{a}}k and
Bartosz Piotrowski and
Stephan Schulz and
Martin Suda and
Josef Urban},
editor = {Adam Naumowicz and Ren{\'{e}} Thiemann},
title = {{MizAR} 60 for {M}izar 50},
booktitle = {14th International Conference on Interactive Theorem Proving, {ITP} 2023},
series = {LIPIcs},
volume = {268},
pages = {19:1--19:22},
publisher = {Schloss Dagstuhl},
year = {2023},
url = {https://doi.org/10.4230/LIPIcs.ITP.2023.19},
doi = {10.4230/LIPICS.ITP.2023.19},
}
@inproceedings{jjck-cicm23,
author = {Jan Jakubuv and Cezary Kaliszyk},
editor = {Catherine Dubois and Manfred Kerber},
title = {{VizAR: V}isualization of Automated Reasoning Proofs (System Description)},
booktitle = {Intelligent Computer Mathematics - 16th International Conference, {CICM} 2023},
series = {LNCS},
volume = {14101},
pages = {303--308},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-42753-4\_22},
doi = {10.1007/978-3-031-42753-4\_22},
}
@inproceedings{lzlbckju-frocos23,
author = {Liao Zhang and Lasse Blaauwbroek and Cezary Kaliszyk and Josef Urban},
editor = {Uli Sattler and Martin Suda},
title = {Learning Proof Transformations and Its Applications in Interactive Theorem Proving},
booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023},
series = {LNCS},
volume = {14279},
pages = {236--254},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_13},
doi = {10.1007/978-3-031-43369-6\_13},
}
@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{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{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 = {26:1--26:8},
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{spjpck-jlc21,
author = {Purgał, Stanisław and Parsert, Julian and Kaliszyk, Cezary},
title = {A study of continuous vector representations for theorem proving},
journal = {Journal of Logic and Computation},
month = {02},
year = {2021},
issn = {0955-792X},
doi = {10.1093/logcom/exab006},
url = {https://doi.org/10.1093/logcom/exab006},
}
@article{tgckjurkmn-jar21,
author = {Thibault Gauthier and
Cezary Kaliszyk and
Josef Urban and
Ramana Kumar and
Michael Norrish},
title = {{TacticToe}: {L}earning to Prove with Tactics},
journal = {J. Autom. Reason.},
volume = {65},
number = {2},
pages = {257--286},
year = {2021},
url = {https://doi.org/10.1007/s10817-020-09580-x},
doi = {10.1007/s10817-020-09580-x},
}
@article{mfckju-jar21,
author = {Michael F{\"{a}}rber and
Cezary Kaliszyk and
Josef Urban},
title = {Machine Learning Guidance for Connection Tableaux},
journal = {J. Autom. Reason.},
volume = {65},
number = {2},
pages = {287--320},
year = {2021},
url = {https://doi.org/10.1007/s10817-020-09576-7},
doi = {10.1007/s10817-020-09576-7},
}
@inproceedings{lzlbbppcckju-cicm21,
author = {Liao Zhang and Lasse Blaauwbroek and Bartosz Piotrowski and Prokop \v{C}ern\'{y} and Cezary Kaliszyk and Josef Urban},
title = {Online Machine Learning Techniques for {C}oq: A Comparison},
booktitle = {Intelligent Computer Mathematics (CICM 2021)},
year = {2021},
series = {LNCS},
editor = {Fairouz Kamareddine and Claudio Sacerdoti-Coen},
url = {https://doi.org/10.1007/978-3-030-81097-9\_5},
doi = {10.1007/978-3-030-81097-9\_5},
}
@inproceedings{dmck-iclr21,
author = {Dennis M\"{u}ller and Cezary Kaliszyk},
title = {Disambiguating Symbolic Expressions in Informal Documents},
booktitle = {9th International Conference on Learning Representations, {ICLR} 2021},
year = {2021},
url = {https://openreview.net/forum?id=K5j7D81ABvt},
}
@inproceedings{zzachmckju-tableaux21,
author = {Zsolt Zombori and Adrián Csiszárik and Henryk Michalewski and Cezary Kaliszyk and Josef Urban},
title = {Towards Finding Longer Proofs},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021)},
year = {2021},
series = {LNCS},
editor = {Anupam Das and Sara Negri},
url = {https://doi.org/10.1007/978-3-030-86059-2_10},
doi = {10.1007/978-3-030-86059-2_10},
}
@inproceedings{qwck-frocos21,
author = {Qingxiang Wang and Cezary Kaliszyk},
editor = {Boris Konev and Giles Reger},
title = {{JEFL:} {J}oint Embedding of Formal Proof Libraries},
booktitle = {Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021},
series = {LNCS},
volume = {12941},
pages = {154--170},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-86205-3\_9},
doi = {10.1007/978-3-030-86205-3\_9},
}
@article{jjck-mcs20,
author = {Jan Jakubuv and Cezary Kaliszyk},
title = {Relaxed Weighted Path Order in Theorem Proving},
journal = {Math. Comput. Sci.},
volume = {14},
number = {3},
pages = {657--670},
year = {2020},
url = {https://doi.org/10.1007/s11786-020-00474-0},
doi = {10.1007/s11786-020-00474-0},
}
@inproceedings{mockju-ecai20,
author = {Miroslav Ols{\'{a}}k and
Cezary Kaliszyk and
Josef Urban},
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},
title = {Property Invariant Embedding for Automated Reasoning},
booktitle = {{ECAI} 2020 - 24th European Conference on Artificial Intelligence},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {325},
pages = {1395--1402},
publisher = {{IOS} Press},
year = {2020},
url = {https://doi.org/10.3233/FAIA200244},
doi = {10.3233/FAIA200244},
}
@inproceedings{qwcbckju-cpp20,
author = {Qingxiang Wang and
Chad E. Brown and
Cezary Kaliszyk and
Josef Urban},
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Exploration of neural machine translation in autoformalization of
mathematics in {M}izar},
booktitle = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
pages = {85--98},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885.3373827},
doi = {10.1145/3372885.3373827},
}
@inproceedings{ckfr-cicm20,
author = {Cezary Kaliszyk and Florian Rabe},
title = {A Survey of Languages for Formalizing Mathematics},
booktitle = {Intelligent Computer Mathematics (CICM 2020)},
year = {2020},
series = {LNCS},
pages = {138--156},
url = {https://doi.org/10.1007/978-3-030-53518-6\_9},
doi = {10.1007/978-3-030-53518-6\_9},
publisher = {Springer, Cham},
volume = {12236},
editor = {Benzmueller C., Miller B.},
}
@inproceedings{jpsack-gcai20,
author = {Julian Parsert and Stephanie Autherith and Cezary Kaliszyk},
title = {Property Preserving Embedding of First-order Logic},
booktitle = {GCAI 2020. 6th Global Conference on Artificial Intelligence (GCAI 2020)},
editor = {Gregoire Danoy and Jun Pang and Geoff Sutcliffe},
series = {EPiC Series in Computing},
volume = {72},
pages = {70--82},
year = {2020},
publisher = {EasyChair},
url = {https://easychair.org/publications/paper/Cwgq},
doi = {10.29007/18t1}
}
@article{beck-mcs20,
author = {Burak Ekici and
Cezary Kaliszyk},
title = {{M}ac {L}ane's Comparison Theorem for the {K}leisli Construction Formalized
in {C}oq},
journal = {Math. Comput. Sci.},
volume = {14},
number = {3},
pages = {533--549},
year = {2020},
url = {https://doi.org/10.1007/s11786-020-00450-8},
doi = {10.1007/s11786-020-00450-8},
}
@Article{tgck-jsc19,
author = {Thibault Gauthier and Cezary Kaliszyk},
title = {Aligning Concepts across Proof Assistant Libraries},
journal = {J. Symbolic Computation},
volume = {90},
pages = {89--123},
year = {2019},
url = {https://doi.org/10.1016/j.jsc.2018.04.005},
doi = {10.1016/j.jsc.2018.04.005},
}
@inproceedings{ckkp-itp19,
author = {Cezary Kaliszyk and Karol Pąk},
title = {Declarative Proof Translation (short paper)},
booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
year = {2019},
series = {LIPIcs},
pages = {35:1--35:7},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.35},
doi = {10.4230/LIPIcs.ITP.2019.35},
editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
volume = {141},
}
@inproceedings{cbckkp-itp19,
author = {Chad Brown and Cezary Kaliszyk and Karol Pąk},
title = {Higher-order {T}arski {G}rothendieck as a Foundation for Formal Proof},
booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
year = {2019},
series = {LIPIcs},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
pages = {9:1--9:16},
url = {https://doi.org/10.4230/LIPIcs.ITP.2019.9},
doi = {10.4230/LIPIcs.ITP.2019.9},
editor = {John Harrison and
John O'Leary and
Andrew Tolmach},
volume = {141},
}
@inproceedings{mfck-tableaux19,
author = {Michael Färber and Cezary Kaliszyk},
title = {Certification of Nonclausal Connection Tableaux Proofs},
booktitle = {28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019)},
year = {2019},
series = {LNCS},
pages = {21--38},
url = {https://doi.org/10.1007/978-3-030-29026-9\_2},
doi = {10.1007/978-3-030-29026-9\_2},
publisher = {Springer},
volume = {11714},
editor = {Serenella Cerrito and
Andrei Popescu},
}
@inproceedings{cbtgckgsju-cade19,
author = {Chad Brown and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban},
title = {{GRUNGE:} {A} Grand Unified {ATP} Challenge},
booktitle = {The 27th International Conference on Automated Deduction (CADE 2019)},
year = {2019},
series = {LNCS},
pages = {123--141},
editor = {Pascal Fontaine},
volume = {11716},
publisher = {Springer},
url = {https://doi.org/10.1007/978-3-030-29436-6\_8},
doi = {10.1007/978-3-030-29436-6\_8},
}
@article{ckkp-jar19,
author = {Cezary Kaliszyk and Karol P\k{a}k},
title = {Semantics of {M}izar as an {I}sabelle Object Logic},
journal = {J. Autom. Reasoning},
year = {2019},
url = {https://doi.org/10.1007/s10817-018-9479-z},
doi = {10.1007/s10817-018-9479-z},
volume = {63},
number = {3},
pages = {557--595},
}
@incollection{bpjucbck-lrgsr19,
title = {Can Neural Networks Learn Symbolic Rewriting?},
author = {Bartosz Piotrowski and Josef Urban and Chad Brown and Cezary Kaliszyk},
booktitle = {Learning and Reasoning with Graph-Structured Representations -- ICML 2019 Workshop},
pages = {1--4},
year = {2019},
url = {https://graphreason.github.io/papers/40.pdf}
}
@proceedings{ckebakcsc-cicm19,
editor = {Cezary Kaliszyk and
Edwin Brady and
Andrea Kohlhase and
Claudio Sacerdoti Coen},
title = {Intelligent Computer Mathematics - 12th International Conference,
{CICM} 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11617},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-23250-4},
doi = {10.1007/978-3-030-23250-4},
isbn = {978-3-030-23249-8},
}
@incollection{ckjuhmmo-nips18,
title = {Reinforcement Learning of Theorem Proving},
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},
year = {2018},
publisher = {Curran Associates, Inc.},
url = {http://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.pdf}
}
@article{lcck-jar18,
author = {\L{}ukasz Czajka and Cezary Kaliszyk},
title = {Hammer for {C}oq: Automation for Dependent Type Theory},
journal = {J. Autom. Reasoning},
volume = {61},
number = {1-4},
pages = {423--453},
year = {2018},
url = {https://doi.org/10.1007/s10817-018-9458-4},
doi = {10.1007/s10817-018-9458-4},
}
@inproceedings{jjck-icms18,
author = {Jan Jakubuv and Cezary Kaliszyk},
title = {Towards a Unified Ordering for Superposition-Based Automated Reasoning},
booktitle = {6th International Conference on Mathematical Software (ICMS 2018)},
pages = {245--254},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96418-8\_29},
doi = {10.1007/978-3-319-96418-8\_29},
editor = {James H. Davenport and
Manuel Kauers and
George Labahn and
Josef Urban},
series = {LNCS},
volume = {10931},
publisher = {Springer},
year = {2018},
}
@inproceedings{lcbeck-cicm18,
author = {\L{}ukasz Czajka and
Burak Ekici and
Cezary Kaliszyk},
title = {Concrete Semantics with {C}oq and {CoqH}ammer},
booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
pages = {53--58},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96812-4\_5},
doi = {10.1007/978-3-319-96812-4\_5},
editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
series = {LNCS},
volume = {11006},
publisher = {Springer},
}
@inproceedings{lcbeck-cicm18,
author = {\L{}ukasz Czajka and
Cezary Kaliszyk},
title = {{CoqHammer}: Strong Automation for Program Verification},
booktitle = {Fourth International Workshop on Coq for Programming Languages, CoqPL 2018}
}
@inproceedings{ckkp-cicm18,
author = {Cezary Kaliszyk and Karol P\k{a}k},
title = {Isabelle Import Infrastructure for the {M}izar Mathematical Library},
booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
pages = {131--146},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96812-4\_13},
doi = {10.1007/978-3-319-96812-4\_13},
editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
series = {LNCS},
volume = {11006},
publisher = {Springer},
}
@inproceedings{qwckju-cicm18,
author = {Qingxiang Wang and
Cezary Kaliszyk and
Josef Urban},
title = {First Experiments with Neural Translation of Informal to Formal Mathematics},
booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
pages = {255--270},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-96812-4\_22},
doi = {10.1007/978-3-319-96812-4\_22},
editor = {Florian Rabe and
William M. Farmer and
Grant O. Passmore and
Abdou Youssef},
series = {LNCS},
volume = {11006},
publisher = {Springer},
}
@inproceedings{jpck-itp18,
author = {Julian Parsert and
Cezary Kaliszyk},
title = {Towards Formal Foundations for Game Theory},
booktitle = {Interactive Theorem Proving - 9th International Conference, {ITP} 2018},
pages = {495--503},
year = {2018},
doi = {10.1007/978-3-319-94821-8\_29},
url = {https://doi.org/10.1007/978-3-319-94821-8\_29},
editor = {Jeremy Avigad and
Assia Mahboubi},
series = {LNCS},
volume = {10895},
publisher = {Springer},
}
@inproceedings{jpck-cpp18,
author = {Julian Parsert and Cezary Kaliszyk},
title = {Formal Microeconomic Foundations and the {First Welfare Theorem}},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs (CPP 2018)},
doi = {10.1145/3167100},
url = {http://doi.acm.org/10.1145/3167100},
pages = {91-101},
year = {2018},
editor = {June Andronick and Amy P. Felty},
publisher = {{ACM}},
}
@article{fksu-aicomm18,
author = {Pascal Fontaine and
Cezary Kaliszyk and
Stephan Schulz and
Josef Urban},
title = {Foreword to the Special Issue on Automated Reasoning},
journal = {{AI} Commun.},
volume = {31},
number = {3},
pages = {235--236},
year = {2018},
url = {https://doi.org/10.3233/AIC-180765},
doi = {10.3233/AIC-180765},
}
@inproceedings{ckkp-macis17,
author = {Cezary Kaliszyk and Karol Pak},
title = {Isabelle Formalization of Set Theoretic Structures and Set Comprehensions},
pages = {163--178},
doi = {10.1007/978-3-319-72453-9\_12},
booktitle = {International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017)},
year = {2017},
editor = {Blömer J. and Kotsireas I. and Kutsia T. and Simos D.},
series = {LNCS},
volume = {10693},
publisher = {Springer},
}
@inproceedings{ckjujv-synasc17,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
title = {System Description: Statistical Parsing of Informalized {M}izar Formulas},
editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephen M. Watt},
booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017},
year = {2017},
publisher = {{IEEE} Computer Society},
pages = {169--172},
}
@article{thetal-pi17,
title={A Formal Proof of the {K}epler conjecture},
volume={5},
doi={10.1017/fmp.2017.1},
journal={Forum of Mathematics, Pi},
publisher={Cambridge University Press},
author={
THOMAS HALES and
MARK ADAMS and
GERTRUD BAUER and
TAT DAT DANG and
JOHN HARRISON and
LE TRUONG HOANG and
CEZARY KALISZYK and
VICTOR MAGRON and
SEAN MCLAUGHLIN and
TAT THANG NGUYEN and
QUANG TRUONG NGUYEN and
TOBIAS NIPKOW and
STEVEN OBUA and
JOSEPH PLESO and
JASON RUTE and
ALEXEY SOLOVYEV and
THI HOAI AN TA and
NAM TRUNG TRAN and
THI DIEP TRIEU and
JOSEF URBAN and
KY VU and
ROLAND ZUMKELLER},
year={2017}
}
@inproceedings{ckjujv-itp17,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
title = {Automating Formalization by Statistical and Semantic Parsing of Mathematics},
booktitle = {8th International Conference on Interactive Theorem Proving (ITP 2017)},
pages = {12--27},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66107-0\_2},
doi = {10.1007/978-3-319-66107-0\_2},
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and C{\'{e}}sar A. Mu{\~{n}}oz},
series = {Lecture Notes in Computer Science},
volume = {10499},
publisher = {Springer},
}
@inproceedings{mfckju-cade17,
author = {Michael F{\"{a}}rber and
Cezary Kaliszyk and
Josef Urban},
title = {{M}onte {C}arlo Tableau Proof Search},
booktitle = {26th International Conference on Automated Deduction (CADE 2017)},
pages = {563--579},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-63046-5\_34},
doi = {10.1007/978-3-319-63046-5\_34},
editor = {Leonardo de Moura},
series = {LNCS},
volume = {10395},
publisher = {Springer},
}
@inproceedings{ckfccs-iclr17,
author = {Cezary Kaliszyk and
Fran{\c{c}}ois Chollet and
Christian Szegedy},
title = {{HolStep}: {A} Machine Learning Dataset for Higher-order Logic Theorem
Proving},
booktitle = {5th International Conference on Learning Representations, {ICLR} 2017,
Toulon, France, April 24-26, 2017, Conference Track Proceedings},
year = {2017},
url = {https://openreview.net/forum?id=ryuxYmvel},
}
@inproceedings{slgicsck-lpar17,
author = {Sarah Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk},
title = {Deep Network Guided Proof Search},
booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
editor = {Thomas Eiter and David Sands},
series = {EPiC Series in Computing},
volume = {46},
pages = {85--105},
year = {2017},
publisher = {EasyChair},
url = {https://doi.org/10.29007/8mwc},
doi = {10.29007/8mwc},
issn = {2398-7340}}
@inproceedings{tgckju-lpar17,
author = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban},
title = {{TacticToe}: Learning to Reason with {HOL4} Tactics},
booktitle = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
editor = {Thomas Eiter and David Sands},
series = {EPiC Series in Computing},
volume = {46},
pages = {125--143},
year = {2017},
publisher = {EasyChair},
url = {https://doi.org/10.29007/ntlb},
doi = {10.29007/ntlb},
issn = {2398-7340}}
@inproceedings{ckkp-fedcsis17,
author = {Cezary Kaliszyk and
Karol P\k{a}k},
title = {Progress in the Independent Certification of {M}izar {M}athematical {L}ibrary
in {I}sabelle},
booktitle = {Proceedings of the 2017 Federated Conference on Computer Science and
Information Systems, FedCSIS 2017},
pages = {227--236},
url = {https://doi.org/10.15439/2017F289},
doi = {10.15439/2017F289},
editor = {Maria Ganzha and
Leszek A. Maciaszek and
Marcin Paprzycki},
year = {2017},
}
@inproceedings{ckkp-cicm17,
author = {Cezary Kaliszyk and Karol Pak},
title = {Presentation and Manipulation of {M}izar Properties in an {I}sabelle Object Logic},
pages = {193--207},
doi = {10.1007/978-3-319-62075-6\_14},
booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
year = {2017},
editor = {Herman Geuvers and
Matthew England and
Osman Hasan and
Florian Rabe and
Olaf Teschke},
series = {LNCS},
volume = {10383},
publisher = {Springer},
}
@inproceedings{dmtgckmkfr-cicm17,
author = {Dennis M{\"{u}}ller and
Thibault Gauthier and
Cezary Kaliszyk and
Michael Kohlhase and
Florian Rabe},
title = {Classification of Alignments Between Concepts of Formal Mathematical
Systems},
booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
pages = {83--98},
year = {2017},
doi = {10.1007/978-3-319-62075-6\_7},
editor = {Herman Geuvers and
Matthew England and
Osman Hasan and
Florian Rabe and
Olaf Teschke},
series = {LNCS},
volume = {10383},
publisher = {Springer},
}
@article{jbdgckdkju-jar-mash16,
author = {Jasmin Christian Blanchette and
David Greenaway and
Cezary Kaliszyk and
Daniel K{\"{u}}hlwein and
Josef Urban},
title = {A Learning-Based Fact Selector for {Isabelle/HOL}},
journal = {J. Autom. Reasoning},
volume = {57},
number = {3},
pages = {219--244},
year = {2016},
url = {http://dx.doi.org/10.1007/s10817-016-9362-8},
doi = {10.1007/s10817-016-9362-8},
}
@article{jbcklpju-h4qed-jfr,
author = {Jasmin C. Blanchette and Cezary Kaliszyk and Lawrence C. Paulson and Josef Urban},
title = {Hammering towards {QED}},
journal = {J. Formalized Reasoning},
volume = {9},
number = {1},
year = {2016},
issn = {1972-5787},
url = {http://jfr.unibo.it/article/view/4593},
doi = {10.6092/issn.1972-5787/4593},
pages = {101--148}
}
@inproceedings{dack-fase16,
author = {David Aspinall and Cezary Kaliszyk},
title = {Towards Formal Proof Metrics},
booktitle = {19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016)},
pages = {325--341},
year = {2016},
editor = {Perdita Stevens and Andrzej Wasowski},
series = {Lecture Notes in Computer Science},
volume = {9633},
publisher = {Springer},
doi = {10.1007/978-3-662-49665-7\_19},
}
@inproceedings{dack-itp16,
author = {David Aspinall and Cezary Kaliszyk},
title = {What’s in a Theorem Name? (Rough Diamond)},
booktitle = {7th Conference on Interactive Theorem Proving (ITP 2016)},
pages = {459--465},
doi = {10.1007/978-3-319-43144-4\_28},
editor = {Jasmin Blanchette and Stephan Merz},
series = {LNCS},
publisher = {Springer},
volume = {9807},
year = {2016},
}
@inproceedings{ckkpju-cpp16,
author = {Cezary Kaliszyk and Karol P\k{a}k and Josef Urban},
title = {Towards a {M}izar Environment for {I}sabelle: Foundations and Language},
booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
and Proofs (CPP 2016)},
doi = {10.1145/2854065.2854070},
pages = {58--65},
year = {2016},
editor = {Jeremy Avigad and Adam Chlipala},
publisher = {{ACM}},
}
@inproceedings{ckgsfr-paar16,
author = {Cezary Kaliszyk and
Geoff Sutcliffe and
Florian Rabe},
title = {{TH1:} The {TPTP} Typed Higher-Order Form with Rank-1 Polymorphism},
pages = {41--55},
booktitle = {Proc. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016)},
year = {2016},
editor = {Pascal Fontaine and
Stephan Schulz and
Josef Urban},
series = {{CEUR}},
volume = {1635},
publisher = {CEUR-WS.org},
}
@inproceedings{mfck-paar16,
author = {Michael F{\"{a}}rber and
Cezary Kaliszyk},
title = {No Choice: Reconstruction of First-order {ATP} Proofs without Skolem Functions},
pages = {24--31},
booktitle = {Proc. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016)},
year = {2016},
editor = {Pascal Fontaine and
Stephan Schulz and
Josef Urban},
series = {{CEUR}},
volume = {1635},
publisher = {CEUR-WS.org},
}
@inproceedings{tgckju-cicm16,
author = {Thibault Gauthier and
Cezary Kaliszyk and
Josef Urban},
title = {Initial Experiments with Statistical Conjecturing over Large Formal
Corpora},
pages = {219--228},
year = {2016},
editor = {Andrea Kohlhase and
Paul Libbrecht and
Bruce R. Miller and
Adam Naumowicz and
Walther Neuper and
Pedro Quaresma and
Frank Wm. Tompa and
Martin Suda},
booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral
Program, and Work in Progress at the Conference on Intelligent Computer
Mathematics 2016 (CICM-WiP 2016)},
series = {{CEUR}},
volume = {1785},
publisher = {CEUR-WS.org},
}
@inproceedings{ckmkdmfr-cicm16,
author = {Cezary Kaliszyk and
Michael Kohlhase and
Dennis M{\"{u}}ller and
Florian Rabe},
title = {A Standard for Aligning Mathematical Concepts},
pages = {229--244},
year = {2016},
editor = {Andrea Kohlhase and
Paul Libbrecht and
Bruce R. Miller and
Adam Naumowicz and
Walther Neuper and
Pedro Quaresma and
Frank Wm. Tompa and
Martin Suda},
booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral
Program, and Work in Progress at the Conference on Intelligent Computer
Mathematics 2016 (CICM-WiP 2016)},
series = {{CEUR}},
volume = {1785},
publisher = {CEUR-WS.org},
}
@inproceedings{ckju-swcs16,
author = {Cezary Kaliszyk and
Josef Urban},
title = {Wikis and Collaborative Systems for Large Formal Mathematics},
booktitle = {Semantic Web Collaborative Spaces},
pages = {35--52},
doi = {10.1007/978-3-319-32667-2\_3},
editor = {Pascal Molli and
John G. Breslin and
Maria{-}Esther Vidal},
series = {LNCS},
volume = {9507},
publisher = {Springer},
year = {2016},
}
@inproceedings{lcck-hatt16,
author = {\L{}ukasz Czajka and
Cezary Kaliszyk},
title = {Goal Translation for a Hammer for {C}oq (Extended Abstract)},
booktitle = {Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016)},
pages = {13--20},
year = {2016},
doi = {10.4204/EPTCS.210.4},
editor = {Jasmin Blanchette and
Cezary Kaliszyk},
series = {{EPTCS}},
volume = {210},
}
@article{ckju-miz40-jar15,
author = {Cezary Kaliszyk and
Josef Urban},
title = {{MizAR} 40 for {M}izar 40},
journal = {J. Autom. Reasoning},
volume = {55},
number = {3},
pages = {245--256},
year = {2015},
url = {http://dx.doi.org/10.1007/s10817-015-9330-8},
doi = {10.1007/s10817-015-9330-8},
}
@article{ckju-jsc15,
author = {Cezary Kaliszyk and Josef Urban},
title = {Learning-assisted Theorem Proving with Millions of Lemmas},
journal = {Journal of Symbolic Computation},
volume = {69},
pages = {109-128},
year = {2015},
doi = {10.1016/j.jsc.2014.09.032},
}
@article{ckju-mcs-hh,
author = {Cezary Kaliszyk and Josef Urban},
title = {{HOL(y)Hammer}: Online {ATP} Service for {HOL Light}},
journal = {Mathematics in Computer Science},
volume = {9},
number = {1},
pages = {5--22},
year = {2015},
url = {https://doi.org/10.1007/s11786-014-0182-0},
doi = {10.1007/s11786-014-0182-0},
}
@inproceedings{ckjujv-itp15,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
title = {Learning To Parse on Aligned Corpora (Rough Diamond)},
booktitle = {Proc. 6h Conference on Interactive Theorem Proving (ITP'15)},
editor = {Christian Urban and Xingyuan Zhang},
series = {LNCS},
volume = {9236},
pages = {227-233},
year = 2015,
doi = {10.1007/978-3-319-22102-1\_15},
publisher = {Springer-Verlag},
}
@InProceedings{mfck-frocos15,
author = {Michael F\"arber and Cezary Kaliszyk},
title = {Random Forests for Premise Selection},
booktitle = {Frontiers of Combining Systems (FroCoS'15)},
year = 2015,
editor = {Carsten Lutz and Silvio Ranise},
series = {LNCS},
pages = {325-340},
volume = {9322},
publisher= {Springer},
doi = {10.1007/978-3-319-24246-0\_20},
}
@InProceedings{ckjujv-frocos15,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
title = {Lemmatization for Stronger Reasoning in Large Theories},
booktitle = {Frontiers of Combining Systems (FroCoS'15)},
year = 2015,
editor = {Carsten Lutz and Silvio Ranise},
series = {LNCS},
pages = {341-356},
volume = {9322},
publisher= {Springer},
doi="10.1007/978-3-319-24246-0\_21",
}
@inproceedings{ck-tableaux15,
author = {Cezary Kaliszyk},
title = {Efficient Low-Level Connection Tableaux},
booktitle = {Proc. 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'15)},
editor = {Hans De Nivelle},
series = {LNCS},
volume = {9323},
pages = {102-111},
year = 2015,
doi = {10.1007/978-3-319-24312-2\_8},
publisher = {Springer-Verlag},
}
@inproceedings{ckjujv-cpp15,
author = {Cezary Kaliszyk and Josef Urban and Jiří Vyskočil},
title = {Certified Connection Tableaux Proofs for {HOL L}ight and {TPTP}},
booktitle = {Proc. of the 4th Conference on Certified Programs and Proofs (CPP'15)},
editor = {Xavier Leroy and Alwen Tiu},
isbn = {978-1-4503-3296-5},
pages = {59-66},
year = 2015,
doi = {10.1145/2676724.2693176},
publisher = {{ACM}}
}
@inproceedings{tgck-cpp15,
author = {Thibault Gauthier and Cezary Kaliszyk},
title = {Premise Selection and External Provers for {HOL4}},
booktitle = {Proc. of the 4th Conference on Certified Programs and Proofs (CPP'15)},
editor = {Xavier Leroy and Alwen Tiu},
isbn = {978-1-4503-3296-5},
pages = {49-57},
year = 2015,
doi = {10.1145/2676724.2693173},
publisher = {{ACM}}
}
@inproceedings{ckjujv-ijcai15,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
title = {Efficient Semantic Features for Automated Reasoning over Large Theories},
booktitle = {Proc. of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15)},
editor = {Qiang Yang and Michael Wooldridge},
publisher = {{AAAI} Press},
year = {2015},
pages = {3084--3090},
}
@inproceedings{ckssjujv-cade15,
author = {Cezary Kaliszyk and Stephan Schulz and Josef Urban and Ji\v{r}\'i Vysko\v{c}il},
title = {System Description: {E.T.} 0.1},
booktitle = {Proc. of 25th International Conference on Automated Deduction (CADE'15)},
editor = {Amy P. Felty and Aart Middeldorp},
series = {LNCS},
volume = {9195},
pages = {389-398},
year = 2015,
doi = {10.1007/978-3-319-21401-6\_27},
publisher = {Springer-Verlag},
}
@inproceedings{ckjuusskcdst-cicm15,
author = {Cezary Kaliszyk and Josef Urban and Umair Siddique and Sanaz Khan Afshar and Cvetan Dunchev and Sofi{\`{e}}ne Tahar},
title = {Formalizing Physics: Automation, Presentation and Foundation Issues},
booktitle = {Proc. of the 8th Conference on Intelligent Computer Mathematics (CICM'15)},
editor = {Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florian Rabe and Volker Sorge},
series = {LNCS},
volume = {9150},
pages = {288-295},
year = 2015,
doi = {10.1007/978-3-319-20615-8\_19},
publisher = {Springer-Verlag},
}
@inproceedings{ckju-lpar15,
author = {Cezary Kaliszyk and
Josef Urban},
title = {{FEMaLeCoP}: Fairly Efficient Machine Learning Connection Prover},
booktitle = {20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)},
pages = {88--96},
year = {2015},
editor = {Martin Davis and
Ansgar Fehnker and
Annabelle McIver and
Andrei Voronkov},
series = {Lecture Notes in Computer Science},
volume = {9450},
publisher = {Springer},
doi = {10.1007/978-3-662-48899-7\_7},
}
@inproceedings{tgck-lpar15,
author = {Thibault Gauthier and
Cezary Kaliszyk},
title = {Sharing {HOL4} and {HOL L}ight Proof Knowledge},
booktitle = {20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)},
pages = {372--386},
year = {2015},
editor = {Martin Davis and
Ansgar Fehnker and
Annabelle McIver and
Andrei Voronkov},
series = {Lecture Notes in Computer Science},
volume = {9450},
publisher = {Springer},
doi = {10.1007/978-3-662-48899-7\_26},
}
@inproceedings{ckjujv-iwil15,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'{\i} Vysko\v{c}il},
title = {Improving Statistical Linguistic Algorithms for Parsing Mathematics},
booktitle = {The 11th International Workshop on the Implementation of Logics (IWIL'15)},
editor = {Boris Konev and Stephan Schulz and Laurent Simon},
series = {EasyChair Proceedings in Computing},
volume = {40},
pages = {27-36},
year = {2016},
publisher = {EasyChair},
}
@inproceedings{mfck-gcai15,
author = {Michael F\"arber and Cezary Kaliszyk},
title = {Metis-based Paramodulation Tactic for {HOL Light}},
booktitle = {Global Conference on Artificial Intelligence (GCAI'15)},
editor = {Georg Gottlob and Geoff Sutcliffe and Andrei Voronkov},
doi = {10.29007/z9mz},
series = {EPiC},
year = 2015,
volume = {36},
pages = {127-136},
publisher = {EasyChair},
}
@proceedings{jbck-hatt16,
editor = {Jasmin Blanchette and Cezary Kaliszyk},
title = {Proceedings First Workshop on Hammers for Type Theory, HaTT 2016},
booktitle = {Proceedings First Workshop on Hammers for Type Theory, HaTT 2016},
series = {{EPTCS}},
volume = {210},
year = {2016},
url = {http://dx.doi.org/10.4204/EPTCS.210},
doi = {10.4204/EPTCS.210},
}
@proceedings{mkjcckfrvs-cicm15,
editor = {Manfred Kerber and
Jacques Carette and
Cezary Kaliszyk and
Florian Rabe and
Volker Sorge},
title = {Intelligent Computer Mathematics - International Conference, {CICM}
2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9150},
publisher = {Springer},
year = {2015},
url = {http://dx.doi.org/10.1007/978-3-319-20615-8},
doi = {10.1007/978-3-319-20615-8},
}
@proceedings{ckap-pxtp15,
editor = {Cezary Kaliszyk and
Andrei Paskevich},
title = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving,
PxTP 2015, Berlin, Germany, August 2-3, 2015},
booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving,
PxTP 2015, Berlin, Germany, August 2-3, 2015},
series = {{EPTCS}},
volume = {186},
year = {2015},
url = {http://dx.doi.org/10.4204/EPTCS.186},
doi = {10.4204/EPTCS.186},
}
@article{ckju-jar14,
author = {Cezary Kaliszyk and
Josef Urban},
title = {Learning-Assisted Automated Reasoning with {F}lyspeck},
journal = {J. Autom. Reasoning},
volume = {53},
number = {2},
pages = {173--213},
year = {2014},
url = {https://doi.org/10.1007/s10817-014-9303-3},
doi = {10.1007/s10817-014-9303-3},
}
@inproceedings{sjckju-acl214,
author = {Sebastiaan Joosten and Cezary Kaliszyk and Josef Urban},
title = {Initial Experiments with {TPTP}-style Automated Theorem Provers
on {ACL2} Problems},
booktitle = {Proc. of the 12th International Workshop on the ACL2 Theorem
Prover and its Applications (ACL2'14)},
editor = {Freek Verbeek and Julien Schmaltz},
series = {EPTCS},
volume = {152},
pages = {77-85},
year = {2014},
doi = {10.4204/EPTCS.152.6},
}
@inproceedings{cklmju-scss14,
author = {Cezary Kaliszyk and Lionel Mamane and Josef Urban},
title = {Machine Learning of {C}oq Proof Guidance: First Experiments},
booktitle = {Symbolic Computation in Software Science (SCSS 2014)},
editor = {Temur Kutsia and Andrei Voronkov},
series = {EasyChair Proceedings in Computing},
doi = {10.29007/lmmg},
volume = {30},
pages = {27-34},
year = {2014},
publisher = {EasyChair},
}
@inproceedings{tgckckmn-paar14,
author = {Thibault Gauthier and Cezary Kaliszyk and Chantal Keller and Michael Norrish},
title = {Beagle as a HOL4 external ATP method},
booktitle = {4th Workshop on Practical Aspects of Automated Reasoning (PAAR-2014)},
editor = {Stephan Schulz and Leonardo De Moura and Boris Konev},
series = {EasyChair Proceedings in Computing},
volume = {31},
pages = {50-59},
year = {2015},
publisher = {EasyChair},
}
@inproceedings{ckjujv-paar14,
author = {Cezary Kaliszyk and Josef Urban and Ji\v{r}\'i Vysko\v{c}il},
title = {Machine Learner for Automated Reasoning 0.4 and 0.5},
booktitle = {4th Workshop on Practical Aspects of Automated Reasoning (PAAR-2014)},
editor = {Stephan Schulz and Leonardo De Moura and Boris Konev},
series = {EasyChair Proceedings in Computing},
volume = {31},
pages = {60-66},
year = {2015},
publisher = {EasyChair},
}
@inproceedings{ckfr-cicm14,
author = {Cezary Kaliszyk and Florian Rabe},
title = {Towards Knowledge Management for {HOL L}ight},
booktitle = {Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
series = {LNCS},
volume = {8543},
pages = {357-372},
year = 2014,
doi = {10.1007/978-3-319-08434-3\_26},
publisher = {Springer Verlag},
}
@inproceedings{tgck-cicm14,
author = {Thibault Gauthier and Cezary Kaliszyk},
title = {Matching concepts across {HOL} libraries},
booktitle = {Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
series = {LNCS},
volume = {8543},
pages = {267-281},
year = 2014,
doi = {10.1007/978-3-319-08434-3\_20},
publisher = {Springer Verlag}
}
@inproceedings{ckjujvhg-cicm14,
author = {Cezary Kaliszyk and Josef Urban and Ji\c{r}\'i Vysko\c{c}il and Herman Geuvers},
title = {Developing Corpus-based Translation Methods between Informal and Formal Mathematics},
booktitle = {Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14)},
editor = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
series = {LNCS},
volume = {8543},
pages = {435-439},
year = 2014,
doi = {10.1007/978-3-319-08434-3\_34},
publisher = {Springer Verlag}
}
@inproceedings{ckju-lpar13,
author = {Cezary Kaliszyk and Josef Urban},
title = {Lemma Mining over {HOL Light}},
booktitle = {Proc. of the 19th International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning (LPAR'13)},
editor = {Kenneth L. McMillan and Aart Middeldorp and Andrei Voronkov},
series = {LNCS},
volume = {8312},
pages = {503-517},
year = {2013},
doi = {10.1007/978-3-642-45221-5\_34},
publisher = {Springer Verlag}
}
@inproceedings{ckju-cicm13,
author = {Cezary Kaliszyk and Josef Urban},
title = {Automated Reasoning Service for {HOL L}ight},
booktitle = {Proc. of the 6th Conference on Intelligent Computer Mathematics (CICM'13)},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7961},
pages = {120-135},
year = {2013},
editor = {Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteiger},
}
@inproceedings{ctckjuhg-cicm13,
author = {Carst Tankink and Cezary Kaliszyk and Josef Urban and Herman Geuvers},
title = {Formal Mathematics on Display: A Wiki for {F}lyspeck},
booktitle = {Proc. of the 6th Conference on Intelligent Computer Mathematics (CICM'13)},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7961},
pages = {152-167},
year = {2013},
doi = {10.1007/978-3-642-39320-4\_10},
editor = {Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteiger},
}
@inproceedings{ckju-cade13,
author = {Cezary Kaliszyk and Josef Urban},
title = {{PRocH}: Proof Reconstruction for {HOL Light}},
booktitle = {Proc. of the 24th International Conference on Automated Deduction},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7898},
pages = {267-274},
year = {2013},
editor = {Maria Paola Bonacina},
}
@inproceedings{ckak-itp13,
author = {Cezary Kaliszyk and Alexander Krauss},
title = {Scalable {LCF}-style proof translation},
url = {http://dx.doi.org/10.1007/978-3-642-39634-2\_7},
booktitle = {Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7998},
pages = {51-66},
year = {2013},
editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
}
@inproceedings{dkjbckju-itp13,
author = {Daniel K\"uhlwein and Jasmin Christian Blanchette and Cezary Kaliszyk and Josef Urban},
title = {{MaSh}: Machine Learning for {Sledgehammer}},
url = {http://dx.doi.org/10.1007/978-3-642-39634-2\_6},
booktitle = {Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7998},
pages = {35-50},
year = {2013},
editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
}
@inproceedings{ctckjuhg-itp13,
author = {Carst Tankink and Cezary Kaliszyk and Josef Urban and Herman Geuvers},
title = {Communicating Formal Proofs: The Case of {Flyspeck}},
url = {http://dx.doi.org/10.1007/978-3-642-39634-2\_32},
booktitle = {Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7998},
pages = {451-456},
year = {2013},
editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
}
@inproceedings{ckts-pxtp13,
author = {Cezary Kaliszyk and Thomas Sternagel},
title = {Initial Experiments on Deriving a Complete {HOL} Simplification Set},
booktitle = {PxTP 2013},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series},
volume = {14},
pages = {77-86},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, http://www.easychair.org},
issn = {2040-557X},
}
@inproceedings{ckju-pxtp13,
author = {Cezary Kaliszyk and Josef Urban},
title = {Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution},
booktitle = {PxTP 2013},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series},
volume = {14},
pages = {87-95},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, http://www.easychair.org},
issn = {2040-557X},
}
@inproceedings{fgakck-adg12,
author = "Fadoua Ghourabi and Asem Kasem and Cezary Kaliszyk",
title = "Algebraic Analysis of {H}uzita's Origami Operations and Their Extensions",
booktitle = {9th International Workshop on Automated Deduction in
Geometry (ADG'12), Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = 7993,
url = {http://dx.doi.org/10.1007/978-3-642-40672-0\_10},
doi = {10.1007/978-3-642-40672-0\_10},
pages = "143-160",
year = 2012
}
@article{cuck-lmcs12,
author = {Christian Urban and
Cezary Kaliszyk},
title = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle},
journal = {Logical Methods in Computer Science},
volume = {8},
number = {2},
year = {2012},
doi = {10.1007/978-3-642-19718-5\_25},
}
@inproceedings{ckju-paar12,
author = {Cezary Kaliszyk and Josef Urban},
title = {Initial Experiments with External Provers and Premise Selection on {HOL Light} Corpora},
booktitle = {Proceedings of the Third Workshop on Practical Aspects of
Automated Reasoning (PAAR-2012), Manchester, UK, June 30, 2012},
volume = 21,
pages = "72--81",
year = 2013,
editor = {Pascal Fontaine and Renate Schmidt and Stephan Schulz},
publisher = {EasyChair},
series = {EasyChair Proceedings in Computing},
}
@proceedings{ckcl-uitp12,
editor = {Cezary Kaliszyk and
Christoph L\"uth},
title = {Proceedings 10th International Workshop On User Interfaces for Theorem
Provers, {UITP} 2012, Bremen, Germany, July 11th, 2012},
booktitle = {Proceedings 10th International Workshop On User Interfaces for Theorem
Provers, {UITP} 2012, Bremen, Germany, July 11th, 2012},
series = {{EPTCS}},
volume = {118},
year = {2013},
url = {http://dx.doi.org/10.4204/EPTCS.118},
doi = {10.4204/EPTCS.118},
}
@InProceedings{ckhb-cpp11,
author = {Cezary Kaliszyk and Henk Barendregt},
title = {Reasoning about Constants in Nominal Isabelle,
or how to Formalize the Second Fixed Point Theorem},
booktitle = {Proc. of the First International Conference on Certified Programs and Proofs},
year = {2011},
pages = {87-102},
editor = {Jean-Pierre Jouannaud and Zhong Shao},
publisher = {Springer Verlag},
series = {LNCS},
volume = {7086},
}
@inproceedings{ckcu-sac11,
author = {Cezary Kaliszyk and
Christian Urban},
title = {Quotients revisited for {I}sabelle/{HOL}},
booktitle = {Proc. of the 26th ACM Symposium on Applied Computing (SAC'11)},
year = {2011},
pages = {1639-1644},
publisher = {ACM},
editor = {William C. Chu and W. Eric Wong and Mathew J. Palakal and Chih-Cheng Hung}
}
@inproceedings{cuck-esop11,
author = {Christian Urban and
Cezary Kaliszyk},
title = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle},
year = {2011},
pages = {480-500},
booktitle = {Proc. of the 20th European Symposium on Programming (ESOP'11)},
publisher = {Springer Verlag},
series = {LNCS},
volume = {6602},
editor = {Gilles Barthe}
}
@inproceedings{ckti-cicm11,
author = {Cezary Kaliszyk and Tetsuo Ida},
title = {Proof Assistant Decision Procedures for Formalizing Origami},
booktitle = {Proc. of the 18th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'11)},
year = {2011},
pages = {45-57},
editor = {James H. Davenport and William M. Farmer and Josef Urban and Florian Rabe},
publisher = {Springer Verlag},
series = {LNCS},
volume = {6824},
}
@article{cardfin2,
author = {Kaliszyk, Cezary},
title = {Counting derangements, counting non bijective functions and the
birthday problem},
journal = {Journal of Formalized Mathematics},
year = 2010,
volume = {18},
number = {4},
pages = {197--200}
}
@inproceedings{wnckfh-plmms10,
author = {Neuper, Walther and Kaliszyk, Cezary and Haftmann, Florian},
title = {CTP-based programming languages. {C}onsiderations about an experimental design},
volume = {44[1/2]},
booktitle = {Proc. of the ACM SIGSAM International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'10)},
year = {2010},
pages = {27--41},
series = {SIGSAM Bull.},
publisher = {ACM},
editor = {James Davenport and Lucas Dixon}
}
@article{mhckfrfw-adn10,
author = {Maxim Hendriks and Cezary Kaliszyk and Femke van Raamsdonk and Freek Wiedijk},
title = {Teaching logic using a state-of-the-art proof assistant},
journal = {Acta Didactica Napocensia},
year = {2010},
volume = {3},
number = {2},
pages = {35-48},
month = {June}
}
@article{ckro-jfr09,
author = {Cezary Kaliszyk and Russell O'Connor},
title = {Computing with Classical Real Numbers},
journal = {Journal of Formalized Reasoning},
year = {2009},
volume = {2},
number = {1},
doi = {10.6092/issn.1972-5787/1411},
pages = {27--39}
}
@misc{kaliszyk-habil,
author = {Cezary Kaliszyk},
title = {Learning-Assisted Automated Reasoning},
year = {2016},
note = {Habilitation thesis, University of Innsbruck},
}
@phdthesis{kaliszyk-phd,
author = {Cezary Kaliszyk},
title = {Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web.},
school = {Radboud University Nijmegen},
url = {http://cl-informatik.uibk.ac.at/cek/docs/09/kaliszyk_thesis_webdoc.pdf},
year = {2009}
}
@inproceedings{ckfw-types08,
author = {Cezary Kaliszyk and
Freek Wiedijk},
title = {Merging procedural and declarative proof},
year = {2008},
pages = {203--219},
booktitle = {Proc. of the Types for Proofs and Programs International Conference (TYPES'08)},
series = {LNCS},
volume = {5497},
publisher = {Springer Verlag},
editor = {Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro}
}
@inproceedings{kaliszyk-calculemus08,
author = {Cezary Kaliszyk},
title = {Automating Side Conditions in Formalized Partial Functions},
booktitle = {Proc. of the 15th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'08)},
year = {2008},
pages = {300-314},
publisher = {Springer Verlag},
series = {LNCS},
volume = {5144},
editor = {Serge Autexier and John Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk}
}
@inproceedings{pchgckjmfw-semwiki08,
author = {Pierre Corbineau and
Herman Geuvers and
Cezary Kaliszyk and
James McKinna and
Freek Wiedijk},
title = {A Real Semantic Web for Mathematics Deserves a Real Semantics},
year = {2008},
booktitle = {Proc. of the 3rd Semantic Wiki Workshop (SemWiki'08)},
publisher = {CEUR-WS},
volume = {360},
editor = {Christoph Lange and Sebastian Schaffert and Hala Skaf-Molli and Max V\"olkel}
}
@techreport{ckfrfwhwmhrv-icis08,
author = {{Kaliszyk}, Cezary and {Raamsdonk}, Femke van and {Wiedijk}, Freek and {Wupper}, Hanno and {Hendriks}, Maxim and {Vrijer}, Roel de},
title = {{Deduction using the ProofWeb system}},
number = {ICIS--R08016},
month = {September},
institution = {Radboud University Nijmegen},
year = {2008},
research_group = {IS},
class = {Report}
}
@inproceedings{pcck-mkm07,
author = {Pierre Corbineau and
Cezary Kaliszyk},
title = {Cooperative Repositories for Formal Proofs},
booktitle = {Proc. of the 6th International Conference on Mathematical Knowledge Management (MKM'07)},
year = {2007},
pages = {221-234},
publisher = {Springer Verlag},
series = {LNCS},
volume = {4573},
editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
url = {http://doi.org/10.1007/978-3-540-73086-6\_19},
doi = {10.1007/978-3-540-73086-6\_19},
}
@inproceedings{ckfw-calculemus07,
author = {Cezary Kaliszyk and
Freek Wiedijk},
title = {Certified Computer Algebra on Top of an Interactive Theorem Prover},
booktitle = {Proc. of the 14th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (Calculemus'07)},
year = {2007},
pages = {94-105},
publisher = {Springer Verlag},
series = {LNCS},
volume = {4573},
editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger}
}
@inproceedings{kaliszyk-uitp06,
author = {Cezary Kaliszyk},
title = {Web Interfaces for Proof Assistants},
booktitle = {Proc. of the Workshop on User Interfaces for Theorem Provers (UITP'06)},
series = {ENTCS},
volume = {174[2]},
year = {2007},
pages = {49-61},
editor = {Serge Autexier and Christoph Benzm\"uller}
}
@MastersThesis{kaliszyk-mag-inf05,
author = {Cezary Kaliszyk},
title = {Modu\l{} komunikacyjny systemu optymalizacji i personalizacji serwis\'ow WWW SIE
(Communication module of the SIE WWW service optimization and personalization system)},
school = {Warsaw University},
year = {2005},
month = {June},
}
@techreport{kaliszyk-dea05,
author = {Cezary Kaliszyk},
institution = {INRIA},
title = {Validation des preuves par r\'ecurrence implicite avec des outils bas\'es sur
le calcul des constructions inductives (Validation of implicit recurrence proofs using the calculus of
inductive constructions)},
year = {2005},
month = {June},
note = {Rapport de DEA}
}
@inproceedings{gakcmgckms-icwe04,
author = {Grzegorz Andruszkiewicz and
Krzysztof Ciebiera and
Marcin Gozdalik and
Cezary Kaliszyk and
Mateusz Srebrny},
title = {SIE - Intelligent Web Proxy Framework},
year = {2004},
pages = {373-385},
publisher = {Springer Verlag},
series = {LNCS},
volume = {3140},
editor = {Nora Koch and Piero Fraternali and Martin Wirsing},
booktitle = {4th International Conference on Web Engineering (ICWE 2004)},
}