@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}
}