×

zbMATH — the first resource for mathematics

Kaliszyk, Cezary

Compute Distance To:
Author ID: kaliszyk.cezary Recent zbMATH articles by "Kaliszyk, Cezary"
Published as: Kaliszyk, Cezary
Documents Indexed: 60 Publications since 2007, including 2 Books

Publications by Year

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.68283
Kaliszyk, Cezary; Urban, Josef
22
2014
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
19
2015
HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177
Kaliszyk, Cezary; Urban, Josef
13
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
11
2017
Scalable LCF-style proof translation. Zbl 1317.68214
Kaliszyk, Cezary; Krauss, Alexander
11
2013
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
11
2013
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283
Urban, Christian; Kaliszyk, Cezary
10
2012
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
7
2016
Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220
Kaliszyk, Cezary; Urban, Josef
7
2015
Matching concepts across HOL libraries. Zbl 1304.68154
Gauthier, Thibault; Kaliszyk, Cezary
7
2014
PRocH: proof reconstruction for HOL Light. Zbl 1381.68271
Kaliszyk, Cezary; Urban, Josef
7
2013
Certified computer algebra on top of an interactive theorem prover. Zbl 1202.68382
Kaliszyk, Cezary; Wiedijk, Freek
7
2007
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
5
2011
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
4
2018
FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 06528775
Kaliszyk, Cezary; Urban, Josef
4
2015
Lemma mining over HOL Light. Zbl 1407.68437
Kaliszyk, Cezary; Urban, Josef
4
2013
Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
4
2013
Web interfaces for proof assistants. Zbl 1278.68266
Kaliszyk, Cezary
4
2007
System description: E.T. 0.1. Zbl 06515521
Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří
3
2015
Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman
3
2014
Automated reasoning service for HOL Light. Zbl 1390.68576
Kaliszyk, Cezary; Urban, Josef
3
2013
Computing with classical real numbers. Zbl 1194.68097
Kaliszyk, Cezary; O’Connor, Russell
3
2008
Cooperative repositories for formal proofs. A wiki-based solution. Zbl 1202.68377
Corbineau, Pierre; Kaliszyk, Cezary
3
2007
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
2
2017
Hammering towards QED. Zbl 07106506
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
2
2016
Lemmatization for stronger reasoning in large theories. Zbl 06688824
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
2
2015
Random forests for premise selection. Zbl 06688823
Färber, Michael; Kaliszyk, Cezary
2
2015
Sharing HOL4 and HOL light proof knowledge. Zbl 06528794
Gauthier, Thibault; Kaliszyk, Cezary
2
2015
Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015
Kerber, Manfred (ed.); Carette, Jacques (ed.); Kaliszyk, Cezary (ed.); Rabe, Florian (ed.); Sorge, Volker (ed.)
2
2015
Towards knowledge management for HOL Light. Zbl 1304.68158
Kaliszyk, Cezary; Rabe, Florian
2
2014
Algebraic analysis of Huzita’s origami operations and their extensions. Zbl 1306.52008
Ghourabi, Fadoua; Kasem, Asem; Kaliszyk, Cezary
2
2013
Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
2
2013
GRUNGE: a grand unified ATP challenge. Zbl 07178973
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef
1
2019
Aligning concepts across proof assistant libraries. Zbl 1395.68247
Gauthier, Thibault; Kaliszyk, Cezary
1
2019
Towards formal foundations for game theory. Zbl 06946998
Parsert, Julian; Kaliszyk, Cezary
1
2018
Towards a unified ordering for superposition-based automated reasoning. Zbl 1395.68248
Jakubuv, Jan; Kaliszyk, Cezary
1
2018
Isabelle formalization of set theoretic structures and set comprehensions. Zbl 07036050
Kaliszyk, Cezary; Pąk, Karol
1
2017
Automating formalization by statistical and semantic parsing of mathematics. Zbl 06821841
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2017
Presentation and manipulation of Mizar properties in an Isabelle object logic. Zbl 1367.68250
Kaliszyk, Cezary; Pąk, Karol
1
2017
What’s in a theorem name? Zbl 06644760
Aspinall, David; Kaliszyk, Cezary
1
2016
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 to parse on aligned corpora (rough diamond). Zbl 06481866
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2015
Merging procedural and declarative proof. Zbl 1246.68198
Kaliszyk, Cezary; Wiedijk, Freek
1
2009
GRUNGE: a grand unified ATP challenge. Zbl 07178973
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef
1
2019
Aligning concepts across proof assistant libraries. Zbl 1395.68247
Gauthier, Thibault; Kaliszyk, Cezary
1
2019
Hammer for Coq: automation for dependent type theory. Zbl 1448.68458
Czajka, Łukasz; Kaliszyk, Cezary
4
2018
Towards formal foundations for game theory. Zbl 06946998
Parsert, Julian; Kaliszyk, Cezary
1
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
11
2017
Classification of alignments between concepts of formal mathematical systems. Zbl 1367.68309
Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian
2
2017
Isabelle formalization of set theoretic structures and set comprehensions. Zbl 07036050
Kaliszyk, Cezary; Pąk, Karol
1
2017
Automating formalization by statistical and semantic parsing of mathematics. Zbl 06821841
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2017
Presentation and manipulation of Mizar properties in an Isabelle object logic. Zbl 1367.68250
Kaliszyk, Cezary; Pąk, Karol
1
2017
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
7
2016
Hammering towards QED. Zbl 07106506
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
2
2016
What’s in a theorem name? Zbl 06644760
Aspinall, David; Kaliszyk, Cezary
1
2016
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
19
2015
HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177
Kaliszyk, Cezary; Urban, Josef
13
2015
Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220
Kaliszyk, Cezary; Urban, Josef
7
2015
FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 06528775
Kaliszyk, Cezary; Urban, Josef
4
2015
System description: E.T. 0.1. Zbl 06515521
Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří
3
2015
Lemmatization for stronger reasoning in large theories. Zbl 06688824
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
2
2015
Random forests for premise selection. Zbl 06688823
Färber, Michael; Kaliszyk, Cezary
2
2015
Sharing HOL4 and HOL light proof knowledge. Zbl 06528794
Gauthier, Thibault; Kaliszyk, Cezary
2
2015
Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Zbl 1316.68015
Kerber, 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.68186
Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène
1
2015
Learning to parse on aligned corpora (rough diamond). Zbl 06481866
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2015
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
22
2014
Matching concepts across HOL libraries. Zbl 1304.68154
Gauthier, Thibault; Kaliszyk, Cezary
7
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
3
2014
Towards knowledge management for HOL Light. Zbl 1304.68158
Kaliszyk, Cezary; Rabe, Florian
2
2014
Scalable LCF-style proof translation. Zbl 1317.68214
Kaliszyk, Cezary; Krauss, Alexander
11
2013
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
11
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
4
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
Algebraic analysis of Huzita’s origami operations and their extensions. Zbl 1306.52008
Ghourabi, Fadoua; Kasem, Asem; Kaliszyk, Cezary
2
2013
Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
2
2013
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1242.68283
Urban, Christian; Kaliszyk, Cezary
10
2012
General bindings and alpha-equivalence in Nominal Isabelle. Zbl 1326.68265
Urban, Christian; Kaliszyk, Cezary
5
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
3
2008
Certified computer algebra on top of an interactive theorem prover. Zbl 1202.68382
Kaliszyk, Cezary; Wiedijk, Freek
7
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 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

Citations by Year