Edit Profile Kaliszyk, Cezary Compute Distance To: Compute Author ID: kaliszyk.cezary Published as: Kaliszyk, Cezary Documents Indexed: 60 Publications since 2007, including 2 Books all top 5 Co-Authors 3 single-authored 25 Urban, Josef 6 Gauthier, Thibault 5 Vyskočil, Jiří 4 Pąk, Karol 4 Rabe, Florian 3 Blanchette, Jasmin Christian 3 Färber, Michael 3 Geuvers, Jan Herman 2 Czajka, Łukasz 2 Ekici, Burak 2 Jakubův, Jan 2 Kühlwein, Daniel 2 Tankink, Carst 2 Urban, Christian 2 Wiedijk, Freek 1 Adams, Mark 1 Aspinall, David 1 Barendregt, Hendrik Pieter 1 Bauer, Gertrud 1 Brady, Edwin C. 1 Brown, Chad Edward 1 Carette, Jacques 1 Corbineau, Pierre 1 Dang, Tat Dat 1 Dunchev, Cvetan 1 Ghourabi, Fadoua 1 Greenaway, David 1 Hales, Thomas Callister 1 Harrison, John 1 Hoang, Le Truong 1 Ida, Tetsuo 1 Irving, Geoffrey 1 Kasem, Asem 1 Kerber, Manfred 1 Khan Afshar, Sanaz 1 Kohlhase, Andrea 1 Kohlhase, Michael 1 Krauss, Alexander 1 Loos, Sarah A. M. 1 Magron, Victor 1 McLaughlin, Sean 1 Müller, Dennis 1 Nguyen, Quang Truong 1 Nguyen, Tat Thang 1 Nipkow, Tobias 1 Obua, Steven 1 O’Connor, Russell 1 Parsert, Julian 1 Paulson, Lawrence Charles 1 Pleso, Joseph 1 Rute, Jason 1 Sacerdoti Coen, Claudio 1 Schulz, Stephan 1 Siddique, Umair 1 Solovyev, Alexey 1 Sorge, Volker 1 Sutcliffe, Geoff 1 Szegedy, Christian 1 Ta Thi Hoai An 1 Tahar, Sofiène 1 Tran, Nam Trung 1 Trieu, Thi Diep 1 Vu, Ky Minh 1 Wang, Qingxiang 1 Zumkeller, Roland all top 5 Serials 6 Journal of Automated Reasoning 3 Mathematics in Computer Science 2 Journal of Symbolic Computation 2 Lecture Notes in Computer Science 2 Journal of Formalized Reasoning 1 Logical Methods in Computer Science 1 Forum of Mathematics, Pi all top 5 Fields 60 Computer science (68-XX) 11 Mathematical logic and foundations (03-XX) 2 General and overarching topics; collections (00-XX) 2 Convex and discrete geometry (52-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Category theory; homological algebra (18-XX) 1 Optics, electromagnetic theory (78-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH 43 Publications have been cited 201 times in 97 Documents Cited by ▼ Year ▼ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 22 2014 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 19 2015 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177Kaliszyk, Cezary; Urban, Josef 13 2015 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 11 2017 Scalable LCF-style proof translation. Zbl 1317.68214Kaliszyk, Cezary; Krauss, Alexander 11 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 11 2013 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283Urban, Christian; Kaliszyk, Cezary 10 2012 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 7 2016 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220Kaliszyk, Cezary; Urban, Josef 7 2015 Matching concepts across HOL libraries. Zbl 1304.68154Gauthier, Thibault; Kaliszyk, Cezary 7 2014 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271Kaliszyk, Cezary; Urban, Josef 7 2013 Certified computer algebra on top of an interactive theorem prover. Zbl 1202.68382Kaliszyk, Cezary; Wiedijk, Freek 7 2007 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265Urban, Christian; Kaliszyk, Cezary 5 2011 Hammer for Coq: automation for dependent type theory. Zbl 1448.68458Czajka, Łukasz; Kaliszyk, Cezary 4 2018 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 06528775Kaliszyk, Cezary; Urban, Josef 4 2015 Lemma mining over HOL Light. Zbl 1407.68437Kaliszyk, Cezary; Urban, Josef 4 2013 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 4 2013 Web interfaces for proof assistants. Zbl 1278.68266Kaliszyk, Cezary 4 2007 System description: E.T. 0.1. Zbl 06515521Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 3 2015 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 3 2014 Automated reasoning service for HOL Light. Zbl 1390.68576Kaliszyk, Cezary; Urban, Josef 3 2013 Computing with classical real numbers. Zbl 1194.68097Kaliszyk, Cezary; O’Connor, Russell 3 2008 Cooperative repositories for formal proofs. A wiki-based solution. Zbl 1202.68377Corbineau, Pierre; Kaliszyk, Cezary 3 2007 Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian 2 2017 Hammering towards QED. Zbl 07106506Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 2 2016 Lemmatization for stronger reasoning in large theories. Zbl 06688824Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 2 2015 Random forests for premise selection. Zbl 06688823Färber, Michael; Kaliszyk, Cezary 2 2015 Sharing HOL4 and HOL light proof knowledge. Zbl 06528794Gauthier, Thibault; Kaliszyk, Cezary 2 2015 Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015Kerber, Manfred (ed.); Carette, Jacques (ed.); Kaliszyk, Cezary (ed.); Rabe, Florian (ed.); Sorge, Volker (ed.) 2 2015 Towards knowledge management for HOL Light. Zbl 1304.68158Kaliszyk, Cezary; Rabe, Florian 2 2014 Algebraic analysis of Huzita’s origami operations and their extensions. Zbl 1306.52008Ghourabi, Fadoua; Kasem, Asem; Kaliszyk, Cezary 2 2013 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 GRUNGE: a grand unified ATP challenge. Zbl 07178973Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 1 2019 Aligning concepts across proof assistant libraries. Zbl 1395.68247Gauthier, Thibault; Kaliszyk, Cezary 1 2019 Towards formal foundations for game theory. Zbl 06946998Parsert, Julian; Kaliszyk, Cezary 1 2018 Towards a unified ordering for superposition-based automated reasoning. Zbl 1395.68248Jakubuv, Jan; Kaliszyk, Cezary 1 2018 Isabelle formalization of set theoretic structures and set comprehensions. Zbl 07036050Kaliszyk, Cezary; Pąk, Karol 1 2017 Automating formalization by statistical and semantic parsing of mathematics. Zbl 06821841Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2017 Presentation and manipulation of Mizar properties in an Isabelle object logic. Zbl 1367.68250Kaliszyk, Cezary; Pąk, Karol 1 2017 What’s in a theorem name? Zbl 06644760Aspinall, David; Kaliszyk, Cezary 1 2016 Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène 1 2015 Learning to parse on aligned corpora (rough diamond). Zbl 06481866Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2015 Merging procedural and declarative proof. Zbl 1246.68198Kaliszyk, Cezary; Wiedijk, Freek 1 2009 GRUNGE: a grand unified ATP challenge. Zbl 07178973Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 1 2019 Aligning concepts across proof assistant libraries. Zbl 1395.68247Gauthier, Thibault; Kaliszyk, Cezary 1 2019 Hammer for Coq: automation for dependent type theory. Zbl 1448.68458Czajka, Łukasz; Kaliszyk, Cezary 4 2018 Towards formal foundations for game theory. Zbl 06946998Parsert, Julian; Kaliszyk, Cezary 1 2018 Towards a unified ordering for superposition-based automated reasoning. Zbl 1395.68248Jakubuv, Jan; Kaliszyk, Cezary 1 2018 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 11 2017 Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian 2 2017 Isabelle formalization of set theoretic structures and set comprehensions. Zbl 07036050Kaliszyk, Cezary; Pąk, Karol 1 2017 Automating formalization by statistical and semantic parsing of mathematics. Zbl 06821841Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2017 Presentation and manipulation of Mizar properties in an Isabelle object logic. Zbl 1367.68250Kaliszyk, Cezary; Pąk, Karol 1 2017 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 7 2016 Hammering towards QED. Zbl 07106506Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 2 2016 What’s in a theorem name? Zbl 06644760Aspinall, David; Kaliszyk, Cezary 1 2016 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 19 2015 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177Kaliszyk, Cezary; Urban, Josef 13 2015 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220Kaliszyk, Cezary; Urban, Josef 7 2015 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 06528775Kaliszyk, Cezary; Urban, Josef 4 2015 System description: E.T. 0.1. Zbl 06515521Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 3 2015 Lemmatization for stronger reasoning in large theories. Zbl 06688824Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 2 2015 Random forests for premise selection. Zbl 06688823Färber, Michael; Kaliszyk, Cezary 2 2015 Sharing HOL4 and HOL light proof knowledge. Zbl 06528794Gauthier, Thibault; Kaliszyk, Cezary 2 2015 Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015Kerber, Manfred (ed.); Carette, Jacques (ed.); Kaliszyk, Cezary (ed.); Rabe, Florian (ed.); Sorge, Volker (ed.) 2 2015 Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène 1 2015 Learning to parse on aligned corpora (rough diamond). Zbl 06481866Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2015 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 22 2014 Matching concepts across HOL libraries. Zbl 1304.68154Gauthier, Thibault; Kaliszyk, Cezary 7 2014 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 3 2014 Towards knowledge management for HOL Light. Zbl 1304.68158Kaliszyk, Cezary; Rabe, Florian 2 2014 Scalable LCF-style proof translation. Zbl 1317.68214Kaliszyk, Cezary; Krauss, Alexander 11 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 11 2013 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271Kaliszyk, Cezary; Urban, Josef 7 2013 Lemma mining over HOL Light. Zbl 1407.68437Kaliszyk, Cezary; Urban, Josef 4 2013 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 4 2013 Automated reasoning service for HOL Light. Zbl 1390.68576Kaliszyk, Cezary; Urban, Josef 3 2013 Algebraic analysis of Huzita’s origami operations and their extensions. Zbl 1306.52008Ghourabi, Fadoua; Kasem, Asem; Kaliszyk, Cezary 2 2013 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283Urban, Christian; Kaliszyk, Cezary 10 2012 General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265Urban, Christian; Kaliszyk, Cezary 5 2011 Merging procedural and declarative proof. Zbl 1246.68198Kaliszyk, Cezary; Wiedijk, Freek 1 2009 Computing with classical real numbers. Zbl 1194.68097Kaliszyk, Cezary; O’Connor, Russell 3 2008 Certified computer algebra on top of an interactive theorem prover. Zbl 1202.68382Kaliszyk, Cezary; Wiedijk, Freek 7 2007 Web interfaces for proof assistants. Zbl 1278.68266Kaliszyk, Cezary 4 2007 Cooperative repositories for formal proofs. A wiki-based solution. Zbl 1202.68377Corbineau, Pierre; Kaliszyk, Cezary 3 2007 all cited Publications top 5 cited Publications all top 5 Cited by 187 Authors 23 Kaliszyk, Cezary 12 Urban, Josef 5 Blanchette, Jasmin Christian 5 Naumowicz, Adam 5 Pąk, Karol 4 Tahar, Sofiène 3 Benzmüller, Christoph Ewald 3 Gauthier, Thibault 3 Janičić, Predrag 3 Khan Afshar, Sanaz 3 Nipkow, Tobias 3 Paulson, Lawrence Charles 3 Rabe, Florian 3 Siddique, Umair 3 Vyskočil, Jiří 2 Bancerek, Grzegorz 2 Byliński, Czesław 2 Cheney, James 2 Czajka, Łukasz 2 Dunchev, Cvetan 2 Färber, Michael 2 Geuvers, Jan Herman 2 Grabowski, Adam 2 Guidi, Ferruccio 2 Heras, Jónathan 2 Ida, Tetsuo 2 Jakubův, Jan 2 Korniłowicz, Artur 2 Kutz, Yunus D. K. 2 Matuszewski, Roman 2 Momigliano, Alberto 2 Narboux, Julien 2 Popescu, Andrei 2 Sacerdoti Coen, Claudio 2 Schmidt-Schauß, Manfred 2 Seddiki, Ons 2 Stojanović Đurđević, Sana 2 Urban, Christian 2 Wenzel, Makarius 1 Abel, Andreas M. 1 Adams, Mark 1 Adams, Mark F. 1 Allais, Guillaume 1 Alt, Helmut 1 Aransay, Jesús 1 Aravantinos, Vincent 1 Aspinall, David 1 Autexier, Serge 1 Azevedo de Amorim, Arthur 1 Barendregt, Hendrik Pieter 1 Bauer, Gertrud 1 Beeson, Michael J. 1 Bengtson, Jesper 1 Bentkamp, Alexander 1 Bezem, Marc 1 Bogoşel, Beniamin 1 Böhme, Sascha 1 Boldo, Sylvie 1 Breitner, Joachim 1 Brown, Chad Edward 1 Buchin, Kevin 1 Bucur, Dorin 1 Chaplick, Steven 1 Chen, Shuwei 1 Cheong, Otfried 1 Chojecki, Przemyslaw 1 Claessen, Koen 1 Corneli, Joseph 1 Dang, Tat Dat 1 Divasón, Jose 1 Echenim, Mnacho 1 Fleury, Mathias 1 Fragalà, Ilaria 1 Fuchs, Laurent 1 Furbach, Ulrich 1 Gammie, Peter 1 Ganesalingam, Mohan 1 Gheri, Lorenzo 1 Ghourabi, Fadoua 1 Gowers, William Timothy 1 Gransden, Thomas 1 Grayson, Daniel Richard 1 Greenaway, David 1 Guan, Yong 1 Guiol, Hervé 1 Gunther, Emmanuel 1 Hales, Thomas Callister 1 Hameer, Aliya 1 Harrison, John 1 Hasan, Osman 1 Haslbeck, Maximilian P. L. 1 He, Xingxing 1 Hoang, Le Truong 1 Holmes, Kathryn 1 Hutter, Dieter 1 Johansson, Moa 1 Julien, Nicolas 1 Kaufmann, Matt 1 Kfoury, Assaf J. 1 Kindermann, Philipp ...and 87 more Authors all top 5 Cited in 22 Serials 21 Journal of Automated Reasoning 5 Mathematics in Computer Science 4 Journal of Symbolic Computation 3 Annals of Mathematics and Artificial Intelligence 2 Theoretical Computer Science 2 Formal Aspects of Computing 2 Journal of Functional Programming 1 Artificial Intelligence 1 Mathematics Magazine 1 Applied Mathematics and Optimization 1 Information Sciences 1 MSCS. Mathematical Structures in Computer Science 1 Bulletin of the American Mathematical Society. New Series 1 Applicable Algebra in Engineering, Communication and Computing 1 Advances in Applied Clifford Algebras 1 Journal of Inequalities and Applications 1 Theory and Practice of Logic Programming 1 Sādhanā 1 Logica Universalis 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning 1 Forum of Mathematics, Pi all top 5 Cited in 20 Fields 90 Computer science (68-XX) 23 Mathematical logic and foundations (03-XX) 4 Geometry (51-XX) 3 Optics, electromagnetic theory (78-XX) 2 Linear and multilinear algebra; matrix theory (15-XX) 2 Real functions (26-XX) 2 Convex and discrete geometry (52-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Field theory and polynomials (12-XX) 1 Algebraic geometry (14-XX) 1 Category theory; homological algebra (18-XX) 1 Approximations and expansions (41-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Manifolds and cell complexes (57-XX) 1 Numerical analysis (65-XX) 1 Quantum theory (81-XX) 1 Operations research, mathematical programming (90-XX) 1 Mathematics education (97-XX) Citations by Year