@article{CKKP-JAR2023, author = {Cezary Kaliszyk and Karol Pak}, title = {Combining Higher-Order Logic with Set Theory Formalizations}, journal = {J. Autom. Reason.}, volume = {67}, number = {2}, pages = {1--20}, year = {2023}, url = {https://doi.org/10.1007/s10817-023-09663-5}, doi = {10.1007/s10817-023-09663-5}, timestamp = {Fri, 02 Jun 2023 21:23:51 +0200}, biburl = {https://dblp.org/rec/journals/jar/KaliszykP23.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } @InProceedings{KPCK-ITP2022, 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}, 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 Representation of the Set of Prime Numbers}, url = {https://doi.org/10.4230/LIPIcs.ITP.2022.26}, doi = {10.4230/LIPIcs.ITP.2022.26}, volume = {237}, year = {2022} } @InProceedings{CBCKKP-ITP2019, author = {Chad E. Brown and Cezary Kaliszyk and Karol P\k{a}k}, title = {{Higher-Order Tarski Grothendieck as a Foundation for Formal Proof}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {9:1--9:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11064}, URN = {urn:nbn:de:0030-drops-110643}, doi = {10.4230/LIPIcs.ITP.2019.9}, annote = {Keywords: model, higher-order, Tarski Grothendieck, proof foundation} } @inProceedings{CKKP-ITP2019, author = {Cezary Kaliszyk and Karol P\k{a}k}, title = {{Declarative Proof Translation (Short Paper)}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {35:1--35:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11090}, URN = {urn:nbn:de:0030-drops-110903}, doi = {10.4230/LIPIcs.ITP.2019.35}, annote = {Keywords: Declarative Proof, Translation, Isabelle/Isar, Mizar} } @inproceedings{CBKP-CICM/MKM19, author = {Brown, Chad E. and Karol P\k{a}k}, editor = {Kaliszyk, Cezary and Brady, Edwin and Kohlhase, Andrea and Sacerdoti Coen, Claudio}, title = {A Tale of Two Set Theories}, booktitle = {Intelligent Computer Mathematics - 12th International Conference, {CICM} 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, pages = {44--60}, year = {2019}, volume = {11617}, publisher = {Springer}, doi = {10.1007/978-3-030-23250-4_4} } @article{CKKP-JAR2018, author = {Cezary Kaliszyk and Karol P\k{a}k}, title = {Semantics of Mizar as an Isabelle Object Logic}, journal = {Journal of Automated Reasoning}, year = {2018}, url = {https://doi.org/10.1007/s10817-018-9479-z}, doi = {doi.org/10.1007/s10817-018-9479-z}, } @inproceedings{KP-Fedcsis2018, author = {Karol P\k{a}k}, editor = {Maria Ganzha and Leszek A. Maciaszek and Marcin Paprzycki}, title = {Combining the {S}yntactic and {S}emantic {R}epresentations of {M}izar {P}roofs}, booktitle = {Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, FedCSIS 2018, Poznan, Poland, September 9-12, 2018}, pages = {145--153}, year = {2018}, doi = {10.15439/2018F248}, publisher = {IEEE}, volume = {15}, series = {Annals of Computer Science and Information Systems} } @inproceedings{KP-Fedcsis2018S, author = {Karol P\k{a}k}, editor = {Maria Ganzha and Leszek A. Maciaszek and Marcin Paprzycki}, title = {Mizar {S}et {C}omprehension in {I}sabelle {F}ramework}, booktitle = {Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, FedCSIS 2018, Poznan, Poland, September 9-12, 2018}, pages = {23--26}, year = {2018}, doi = {10.15439/2018F106}, publisher = {IEEE}, volume = {15}, series = {Annals of Computer Science and Information Systems} } @inproceedings{CKKP-CICM/MKM18, author = {Cezary Kaliszyk and Karol P\k{a}k}, editor = {Florian Rabe and William M. Farmer and Grant O. Passmore and Abdou Youssef}, title = {Isabelle Import Infrastructure for the Mizar Mathematical Library}, booktitle = {Intelligent Computer Mathematics - 11th International Conference, {CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings}, series = {Lecture Notes in Computer Science}, pages = {131--146}, year = {2018}, volume = {11006}, publisher = {Springer}, doi = {10.1007/978-3-319-96812-4_13} } @ARTICLE{BGKMNP-JAR2018, author = {Grzegorz Bancerek and Czeslaw Byli\'nski and Adam Grabowski and Artur Korni\l owicz and Roman Matuszewski and Adam Naumowicz and Karol P\k{a}k}, title = {The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar}, journal = {J. Autom. Reasoning}, volume = {61}, number = {1-4}, pages = {9--32}, year = {2018}, doi = {10.1007/s10817-017-9440-6}, } @ARTICLE{TDKP-PlosONE, AUTHOR = {Tomaszuk, Dominik and P\k{a}k, Karol}, TITLE = {Reducing vertices in property graphs}, JOURNAL = {Plos One}, YEAR = {2018}, volume = {13}, number = {2}, pages = {1--25}, doi = {10.1371/journal.pone.0191917} } @article{GBCBAGAKRMANKP-JAR17, author = {Grzegorz Bancerek and Czes\l{}aw Byli\'n{}ski and Adam Grabowski and Artur Korni\l{}owicz and Roman Matuszewski and Adam Naumowicz and Karol P\k{a}k}, title = {The {R}ole of the {M}izar {M}athematical {L}ibrary for {I}nteractive {P}roof {D}evelopment in {M}izar}, journal = {Journal of Automated Reasoning}, pages = {1--24}, year = {2017}, doi = {10.1007/s10817-017-9440-6}, note = {to appear} } @inproceedings{CKKP-MACIS2017, author = {Cezary Kaliszyk and Karol P\k{a}k}, title = {Isabelle {F}ormalization of {S}et {T}heoretic {S}tructures and {C}omprehensions}, booktitle = {Mathematical Aspects of Computer and Information Sciences - 7th International Conference, {MACIS} 2017, Vienna, Austria, November 15-17, 2017}, series = {Lecture Notes in Computer Science}, year = {2017}, pages = {163--178}, publisher = {Springer}, volume = {10693} } @inproceedings{MAKP-Fedcsis2017, author = {Marcin Acewicz and Karol P\k{a}k}, editor = {Maria Ganzha and Leszek A. Maciaszek and Marcin Paprzycki}, title = {Formalization of {P}ell`s {E}quations in the {M}izar {S}ystem}, booktitle = {Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, Prague, Czech Republic, September 3-6, 2017}, year = {2017}, pages = {223--226}, volume = {10693}, doi = {10.15439/2017F314}, publisher = {IEEE}, volume = {11}, series = {Annals of Computer Science and Information Systems} } @inproceedings{CKKP-Fedcsis2017, author = {Cezary Kaliszyk and Karol P\k{a}k}, editor = {Maria Ganzha and Leszek A. Maciaszek and Marcin Paprzycki}, title = {Progress in the {I}ndependent {C}ertification 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, Prague, Czech Republic, September 3-6, 2017}, pages = {227--236}, year = {2017}, doi = {10.1007/978-3-319-62075-6_14}, publisher = {IEEE}, volume = {11}, series = {Annals of Computer Science and Information Systems} } @inproceedings{CKKP-CICM/MKM17, author = {Cezary Kaliszyk and Karol P\k{a}k}, editor = {Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke}, title = {Presentation and {M}anipulation of {M}izar {P}roperties in an {I}sabelle {O}bject {L}ogic}, booktitle = {Intelligent Computer Mathematics - 10th International Conference, {CICM} 2017, Edinburgh, UK, July 17-21, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, pages = {193--207}, year = {2017}, volume = {10383}, publisher = {Springer}, doi = {10.1007/978-3-319-62075-6_14} } @inproceedings{KP-CICM16/FM4M, author = {Karol P\k{a}k}, 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}, title = {Topological {F}oundations for a {F}ormal {T}heory of {M}anifolds}, booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics {(CICM} 2016), Bialystok, Poland, July 25-29, 2016.}, pages = {14--16}, year = {2016}, series = {{CEUR} Workshop Proceedings}, volume = {1785}, publisher = {CEUR-WS.org}, } @inproceedings{KP-CICM16/MKM/WP, author = {Karol P\k{a}k}, 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}, title = {Lemma {E}xtraction {C}riteria {B}ased on {P}roperties of {T}heorem {S}tatements}, booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics {(CICM} 2016), Bialystok, Poland, July 25-29, 2016.}, pages = {158--171}, year = {2016}, series = {{CEUR} Workshop Proceedings}, volume = {1785}, publisher = {CEUR-WS.org} } @inproceedings{KPAS-CICM16/MKM/WP, author = {Karol P\k{a}k and Aleksy Schubert}, 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}, title = {The {I}mpact of {P}roof {S}teps {S}equence on {P}roof {R}eadability - {E}xperimental {S}etting}, booktitle = {Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics {(CICM} 2016), Bialystok, Poland, July 25-29, 2016.}, pages = {172--186}, year = {2016}, series = {{CEUR} Workshop Proceedings}, volume = {1785}, publisher = {CEUR-WS.org} } @inproceedings{CKKPJU-CPP16, author = {Cezary Kaliszyk and Karol P\k{a}k and Josef Urban}, title = {Towards a {M}izar {E}nvironment for {I}sabelle: {F}oundations and {L}anguage}, booktitle = {Proc. 5th Conference on Certified Programs and Proofs (CPP 2016)}, pages = {58--65}, year = {2016}, editor = {Jeremy Avigad and Adam Chlipala}, publisher = {{ACM}}, url = {http://doi.acm.org/10.1145/2854065.2854070}, doi = {10.1145/2854065.2854070}, } @article{KP-JAR15, author = {Karol P\k{a}k}, title = {Improving {L}egibility of {F}ormal {P}roofs {B}ased on the {C}lose {R}eference {P}rinciple is {NP}-{H}ard}, journal = {Journal of Automated Reasoning}, volume = {55}, number = {3}, pages = {295--306}, year = {2015}, doi = {10.1007/s10817-015-9337-1} } @inproceedings{KP-CICM15/MKM, author = {Karol P\k{a}k}, editor = {Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florian Rabe and Volker Sorge}, title = {Readable {F}ormalization of {E}uler's {P}artition {T}heorem in {M}izar}, 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}, pages = {211--226}, year = {2015}, doi = {10.1007/978-3-319-20615-8_14} } @inproceedings{Mizar-CICM15/MKM, author = {Grzegorz Bancerek and Czeslaw Bylinski and Adam Grabowski and Artur Korni\l{}owicz and Roman Matuszewski and Adam Naumowicz and Karol P\k{a}k and Josef Urban}, editor = {Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florian Rabe and Volker Sorge}, title = {Mizar: {S}tate-of-the-art and {B}eyond}, 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}, pages = {261--279}, doi = {10.1007/978-3-319-20615-8_17} } @article{KP-LMCS14, author = {Karol P\k{a}k}, title = {Improving {L}egibility of {N}atural {D}eduction {P}roofs is not {T}rivial}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {3}, year = {2014}, doi = {10.2168/LMCS-10(3:23)2014} } @inproceedings{KP-CICM14/MKM, author = {Karol P\k{a}k}, editor = {Stephen M. Watt and James H. Davenport and Alan P. Sexton and Petr Sojka and Josef Urban}, title = {Automated {I}mproving of {Pr}oof {L}egibility in the {M}izar {S}ystem}, booktitle = {Intelligent Computer Mathematics - International Conference, {CICM} 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings}, pages = {373--387}, series = {Lecture Notes in Computer Science}, volume = {8543}, publisher = {Springer}, year = {2014} } @article{KP-JAR13, author = {Karol P\k{a}k}, title = {Methods of {L}emma {E}xtraction in {N}atural {D}eduction {P}roofs}, journal = {Journal of Automated Reasoning}, volume = {50}, number = {2}, pages = {217--228}, year = {2013}, doi = {10.1007/s10817-012-9267-0} } @inproceedings{DTKPHR-ADBIS12, author = {Dominik Tomaszuk and Karol P\k{a}k and Henryk Rybinski}, editor = {Tadeusz Morzy and Theo H{\"{a}}rder and Robert Wrembel}, title = {Trust in {RDF} {G}raphs}, booktitle = {Advances in Databases and Information Systems - 16th East European Conference, {ADBIS} 2012, Pozna{\'{n}}, Poland, September 18-21, 2012. Proceedings {II}}, pages = {273--283}, series = {Advances in Intelligent Systems and Computing}, volume = {186}, publisher = {Springer}, year = {2012}, doi = {10.1007/978-3-642-32741-4_25} } @ARTICLE{KP-SLGR, AUTHOR = {Karol P\k{a}k}, TITLE = {The {A}lgorithms for {I}mproving and {R}eorganizing {N}atural {D}eduction {P}roofs}, JOURNAL = {Studies in Logic, Grammar and Rhetoric}, YEAR = {2010}, volume = {22}, number = {35}, pages = {95--112} } @INPROCEEDINGS{KP-PCM14, AUTHOR = {Karol P\k{a}k}, editor = {Anna Gomoli\'nska and Adam Grabowski and Ma\l{}gorzata Hryniewicka and Magdalena Kacprzak and Ewa Schmeidel }, BOOKTITLE = {Trends in Contemporary Computer Science Podlasie 2014}, TITLE = {Improving Legibility of Proof Scripts Based on Quantity of Introduced Labels}, pages = {71--82}, PUBLISHER = {Bialystok University of Technology Publishing Office}, YEAR = {2014} } @INPROCEEDINGS{BPJRLKKP-SPECOM06, AUTHOR = {Bo\.zena Pi\'orkowska and Janusz Rafa\l{}ko and \L{}ukasz Kalinowski and Karol P\k{a}k}, TITLE = {Parts of Speech Recognition System for the Text-Based, Polish Speech Synthesizer}, BOOKTITLE = {11th International Conference on Speech and Computer (SPECOM 2006), St. Petersburg, 25-29 June 2006}, YEAR = {2006}, pages = {471--473} }