×
Compute Distance To:
Author ID: kaliszyk.cezary Recent zbMATH articles by "Kaliszyk, Cezary"
Published as: Kaliszyk, Cezary
all top 5

Co-Authors

3 single-authored
31 Urban, Josef
7 Gauthier, Thibault
6 Pąk, Karol
5 Vyskočil, Jiří
4 Färber, Michael
4 Rabe, Florian
3 Blanchette, Jasmin Christian
3 Brown, Chad Edward
3 Geuvers, Jan Herman
2 Czajka, Łukasz
2 Ekici, Burak
2 Jakubův, Jan
2 Kühlwein, Daniel
2 Parsert, Julian
2 Schulz, Stephan
2 Tankink, Carst
2 Urban, Christian
2 Wang, Qingxiang
2 Wiedijk, Freek
1 Adams, Mark
1 Aspinall, David
1 Barendregt, Hendrik Pieter
1 Bauer, Gertrud
1 Blaauwbroek, Lasse
1 Brady, Edwin C.
1 Carette, Jacques
1 Černỳ, Prokop
1 Cohen, Liron
1 Corbineau, Pierre
1 Csiszárik, Adrián
1 Dang, Tat Dat
1 Dunchev, Cvetan
1 Fontaine, Pascal
1 Ghourabi, Fadoua
1 Greenaway, David
1 Hales, Thomas Callister
1 Hoàng Lê Trường
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 Kumar, Ramana
1 Loos, Sarah M.
1 Magron, Victor
1 McLaughlin, Sean
1 Michalewski, Henryk
1 Müller, Dennis
1 Nguyen, Quang Truong
1 Nguyen, Tat Thang
1 Nipkow, Tobias
1 Norrish, Michael
1 Obua, Steven
1 O’Connor, Russell
1 Olšák, Miroslav
1 Paskevich, Andrei
1 Paulson, Lawrence Charles
1 Piotrowski, Bartosz
1 Pleso, Joseph
1 PurgaŁ, StanisŁaw
1 Rute, Jason
1 Sacerdoti Coen, Claudio
1 Siddique, Umair
1 Solovyev, Alexey
1 Sorge, Volker
1 Sutcliffe, Geoff
1 Szegedy, Christian
1 Tạ Thị Hoài An
1 Tahar, Sofiène
1 Tran, Nam Trung
1 Trieu, Thi Diep
1 Zhang, Liao
1 Zombori, Zsolt
1 Zumkeller, Roland

Publications by Year

Citations contained in zbMATH Open

55 Publications have been cited 406 times in 184 Documents Cited by Year
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
35
2014
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
33
2015
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, 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
31
2017
HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177
Kaliszyk, Cezary; Urban, Josef
26
2015
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
22
2016
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
18
2018
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283
Urban, Christian; Kaliszyk, Cezary
15
2012
FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312
Kaliszyk, Cezary; Urban, Josef
14
2015
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
14
2013
Scalable LCF-style proof translation. Zbl 1317.68214
Kaliszyk, Cezary; Krauss, Alexander
14
2013
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
13
2016
Deep network guided proof search. Zbl 1403.68197
Loos, Sarah; Irving, Geoffrey; Szegedy, Christian; Kaliszyk, Cezary
11
2017
Certified computer algebra on top of an interactive theorem prover. Zbl 1202.68382
Kaliszyk, Cezary; Wiedijk, Freek
9
2007
Matching concepts across HOL libraries. Zbl 1304.68154
Gauthier, Thibault; Kaliszyk, Cezary
8
2014
Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220
Kaliszyk, Cezary; Urban, Josef
7
2015
TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef
7
2017
PRocH: proof reconstruction for HOL Light. Zbl 1381.68271
Kaliszyk, Cezary; Urban, Josef
7
2013
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
7
2011
GRUNGE: a grand unified ATP challenge. Zbl 07178973
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef
6
2019
TacticToe: learning to prove with tactics. Zbl 07356973
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael
6
2021
Random forests for premise selection. Zbl 1471.68307
Färber, Michael; Kaliszyk, Cezary
5
2015
Sharing HOL4 and HOL Light proof knowledge. Zbl 1471.68309
Gauthier, Thibault; Kaliszyk, Cezary
5
2015
Property invariant embedding for automated reasoning. Zbl 1464.68317
Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef
5
2020
Monte Carlo tableau proof search. Zbl 1494.68286
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
5
2017
Lemma mining over HOL Light. Zbl 1407.68437
Kaliszyk, Cezary; Urban, Josef
5
2013
Aligning concepts across proof assistant libraries. Zbl 1395.68247
Gauthier, Thibault; Kaliszyk, Cezary
5
2019
Computing with classical real numbers. Zbl 1194.68097
Kaliszyk, Cezary; O’Connor, Russell
4
2008
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
4
2017
A survey of languages for formalizing mathematics. Zbl 1455.68257
Kaliszyk, Cezary; Rabe, Florian
4
2020
Towards knowledge management for HOL Light. Zbl 1304.68158
Kaliszyk, Cezary; Rabe, Florian
4
2014
Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman
4
2014
System description: E.T. 0.1. Zbl 1465.68286
Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří
4
2015
Web interfaces for proof assistants. Zbl 1278.68266
Kaliszyk, Cezary
4
2007
Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
4
2013
Semantics of Mizar as an Isabelle object logic. Zbl 1468.68290
Kaliszyk, Cezary; Pąk, Karol
4
2019
Lemmatization for stronger reasoning in large theories. Zbl 1471.68313
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
3
2015
Efficient low-level connection tableaux. Zbl 1471.68311
Kaliszyk, Cezary
3
2015
Cooperative repositories for formal proofs. A wiki-based solution. Zbl 1202.68377
Corbineau, Pierre; Kaliszyk, Cezary
3
2007
Automated reasoning service for HOL Light. Zbl 1390.68576
Kaliszyk, Cezary; Urban, Josef
3
2013
Machine learning guidance for connection tableaux. Zbl 07356974
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
3
2021
Isabelle formalization of set theoretic structures and set comprehensions. Zbl 1497.68547
Kaliszyk, Cezary; Pąk, Karol
2
2017
Towards formal foundations for game theory. Zbl 06946998
Parsert, Julian; Kaliszyk, Cezary
2
2018
Isabelle import infrastructure for the Mizar Mathematical Library. Zbl 1417.68185
Kaliszyk, Cezary; Pąk, Karol
2
2018
Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015
2
2015
Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
2
2013
Algebraic analysis of Huzita’s origami operations and their extensions. Zbl 1306.52008
Ghourabi, Fadoua; Kasem, Asem; Kaliszyk, Cezary
2
2013
What’s in a theorem name? Zbl 1478.68434
Aspinall, David; Kaliszyk, Cezary
2
2016
Presentation and manipulation of Mizar properties in an Isabelle object logic. Zbl 1367.68250
Kaliszyk, Cezary; Pąk, Karol
1
2017
Certification of nonclausal connection tableaux proofs. Zbl 1435.03033
Färber, Michael; Kaliszyk, Cezary
1
2019
Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2015
Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186
Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène
1
2015
Towards a unified ordering for superposition-based automated reasoning. Zbl 1395.68248
Jakubuv, Jan; Kaliszyk, Cezary
1
2018
Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2017
Merging procedural and declarative proof. Zbl 1246.68198
Kaliszyk, Cezary; Wiedijk, Freek
1
2009
Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Zbl 1428.68028
1
2019
TacticToe: learning to prove with tactics. Zbl 07356973
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael
6
2021
Machine learning guidance for connection tableaux. Zbl 07356974
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
3
2021
Property invariant embedding for automated reasoning. Zbl 1464.68317
Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef
5
2020
A survey of languages for formalizing mathematics. Zbl 1455.68257
Kaliszyk, Cezary; Rabe, Florian
4
2020
GRUNGE: a grand unified ATP challenge. Zbl 07178973
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef
6
2019
Aligning concepts across proof assistant libraries. Zbl 1395.68247
Gauthier, Thibault; Kaliszyk, Cezary
5
2019
Semantics of Mizar as an Isabelle object logic. Zbl 1468.68290
Kaliszyk, Cezary; Pąk, Karol
4
2019
Certification of nonclausal connection tableaux proofs. Zbl 1435.03033
Färber, Michael; Kaliszyk, Cezary
1
2019
Intelligent computer mathematics. 12th international conference, CICM 2019, Prague, Czech Republic, July 8–12, 2019. Proceedings. Zbl 1428.68028
1
2019
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
18
2018
Towards formal foundations for game theory. Zbl 06946998
Parsert, Julian; Kaliszyk, Cezary
2
2018
Isabelle import infrastructure for the Mizar Mathematical Library. Zbl 1417.68185
Kaliszyk, Cezary; Pąk, Karol
2
2018
Towards a unified ordering for superposition-based automated reasoning. Zbl 1395.68248
Jakubuv, Jan; Kaliszyk, Cezary
1
2018
A formal proof of the Kepler conjecture. Zbl 1379.52018
Hales, 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
31
2017
Deep network guided proof search. Zbl 1403.68197
Loos, Sarah; Irving, Geoffrey; Szegedy, Christian; Kaliszyk, Cezary
11
2017
TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef
7
2017
Monte Carlo tableau proof search. Zbl 1494.68286
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
5
2017
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
4
2017
Isabelle formalization of set theoretic structures and set comprehensions. Zbl 1497.68547
Kaliszyk, Cezary; Pąk, Karol
2
2017
Presentation and manipulation of Mizar properties in an Isabelle object logic. Zbl 1367.68250
Kaliszyk, Cezary; Pąk, Karol
1
2017
Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2017
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
22
2016
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
13
2016
What’s in a theorem name? Zbl 1478.68434
Aspinall, David; Kaliszyk, Cezary
2
2016
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
33
2015
HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177
Kaliszyk, Cezary; Urban, Josef
26
2015
FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312
Kaliszyk, Cezary; Urban, Josef
14
2015
Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220
Kaliszyk, Cezary; Urban, Josef
7
2015
Random forests for premise selection. Zbl 1471.68307
Färber, Michael; Kaliszyk, Cezary
5
2015
Sharing HOL4 and HOL Light proof knowledge. Zbl 1471.68309
Gauthier, Thibault; Kaliszyk, Cezary
5
2015
System description: E.T. 0.1. Zbl 1465.68286
Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří
4
2015
Lemmatization for stronger reasoning in large theories. Zbl 1471.68313
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
3
2015
Efficient low-level connection tableaux. Zbl 1471.68311
Kaliszyk, Cezary
3
2015
Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015
2
2015
Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2015
Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186
Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène
1
2015
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
35
2014
Matching concepts across HOL libraries. Zbl 1304.68154
Gauthier, Thibault; Kaliszyk, Cezary
8
2014
Towards knowledge management for HOL Light. Zbl 1304.68158
Kaliszyk, Cezary; Rabe, Florian
4
2014
Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman
4
2014
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
14
2013
Scalable LCF-style proof translation. Zbl 1317.68214
Kaliszyk, Cezary; Krauss, Alexander
14
2013
PRocH: proof reconstruction for HOL Light. Zbl 1381.68271
Kaliszyk, Cezary; Urban, Josef
7
2013
Lemma mining over HOL Light. Zbl 1407.68437
Kaliszyk, Cezary; Urban, Josef
5
2013
Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
4
2013
Automated reasoning service for HOL Light. Zbl 1390.68576
Kaliszyk, Cezary; Urban, Josef
3
2013
Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
2
2013
Algebraic analysis of Huzita’s origami operations and their extensions. Zbl 1306.52008
Ghourabi, Fadoua; Kasem, Asem; Kaliszyk, Cezary
2
2013
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283
Urban, Christian; Kaliszyk, Cezary
15
2012
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
7
2011
Merging procedural and declarative proof. Zbl 1246.68198
Kaliszyk, Cezary; Wiedijk, Freek
1
2009
Computing with classical real numbers. Zbl 1194.68097
Kaliszyk, Cezary; O’Connor, Russell
4
2008
Certified computer algebra on top of an interactive theorem prover. Zbl 1202.68382
Kaliszyk, Cezary; Wiedijk, Freek
9
2007
Web interfaces for proof assistants. Zbl 1278.68266
Kaliszyk, Cezary
4
2007
Cooperative repositories for formal proofs. A wiki-based solution. Zbl 1202.68377
Corbineau, Pierre; Kaliszyk, Cezary
3
2007
all top 5

Cited by 308 Authors

31 Kaliszyk, Cezary
27 Urban, Josef
10 Blanchette, Jasmin Christian
8 Jakubův, Jan
7 Pąk, Karol
7 Rabe, Florian
6 Bentkamp, Alexander
6 Paulson, Lawrence Charles
6 Reger, Giles
5 Gauthier, Thibault
5 Naumowicz, Adam
5 Olšák, Miroslav
5 Sutcliffe, Geoff
5 Traytel, Dmitry
5 Vukmirović, Petar
5 Wenzel, Makarius
4 Benzmüller, Christoph Ewald
4 Bhayat, Ahmed
4 Brown, Chad Edward
4 Chvalovský, Karel
4 Cruanes, Simon
4 Czajka, Łukasz
4 Janičić, Predrag
4 Kutz, Yunus D. K.
4 Nipkow, Tobias
4 Schmidt-Schauß, Manfred
4 Suda, Martin
4 Tahar, Sofiène
4 Tourret, Sophie
4 Waldmann, Uwe
3 Färber, Michael
3 Khan Afshar, Sanaz
3 Kohlhase, Michael
3 Korniłowicz, Artur
3 Koutsoukou-Argyraki, Angeliki
3 Narboux, Julien
3 Popescu, Andrei
3 Siddique, Umair
3 Vyskočil, Jiří
3 Zombori, Zsolt
2 Bancerek, Grzegorz
2 Byliński, Czesław
2 Cheney, James
2 Cohn, Henry Lee
2 Dubut, Jérémy
2 Dunchev, Cvetan
2 Fleury, Mathias
2 Geuvers, Jan Herman
2 Goertzel, Zarathustra Amadeus
2 Grabowski, Adam
2 Guidi, Ferruccio
2 He, Xingxing
2 Heras, Jónathan
2 Ida, Tetsuo
2 Lewis, Robert Y.
2 Liu, Jun
2 Matuszewski, Roman
2 Momigliano, Alberto
2 Nummelin, Visa
2 Otten, Jens
2 Parrow, Joachim
2 Piotrowski, Bartosz
2 Rawson, Michael
2 Sacerdoti Coen, Claudio
2 Schulz, Stephan
2 Seddiki, Ons
2 Stojanović Đurđević, Sana
2 Théry, Laurent
2 Urban, Christian
2 Weber, Tjark
2 Wernhard, Christoph
2 Xu, Yang
2 Yamada, Akihisa
1 Abel, Andreas M.
1 Adams, Mark
1 Afkhami-Jeddi, Nima
1 Allais, Guillaume
1 Alt, Helmut
1 Aransay, Jesús
1 Aravantinos, Vincent
1 Aspinall, David
1 Autexier, Serge
1 Avigad, Jeremy
1 Azevedo de Amorim, Arthur
1 Barbosa, Haniel
1 Barendregt, Hendrik Pieter
1 Barrett, Clark W.
1 Bauer, Gertrud
1 Beeson, Michael J.
1 Bengtson, Jesper
1 Bertholon, Guillaume
1 Bezem, Marc
1 Bibel, Wolfgang
1 Blaauwbroek, Lasse
1 Bogoşel, Beniamin
1 Böhme, Sascha
1 Boldo, Sylvie
1 Borgström, Johannes
1 Breitner, Joachim
1 Brun, Matthias
...and 208 more Authors

Citations by Year