ask others

Cezary Kaliszyk

> Home > Persons

Person information

affiliation: University of Innsbruck, Austria

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

showing all ?? records

2010 – today

see FAQ

What is the meaning of the colors in the publication lists?

2018
[j15]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/aicom/FontaineKSU18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/aicom/FontaineKSU18
Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban:
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31(3): 235-236 (2018)
[j14]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/CzajkaK18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/CzajkaK18
Lukasz Czajka, Cezary Kaliszyk:
Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reasoning 61(1-4): 423-453 (2018)
[c59]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/KaliszykP18
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KaliszykP18
Cezary Kaliszyk, Julian Parsert:
Formal microeconomic foundations and the first welfare theorem. CPP 2018: 91-101
[i24]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1804-00595
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1804-00595
Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
Learning to Reason with HOL4 tactics. CoRR abs/1804.00595 (2018)
[i23]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1804-00596
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1804-00596
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
Learning to Prove with Tactics. CoRR abs/1804.00596 (2018)
[i22]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1805-03107
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1805-03107
Michael Färber, Cezary Kaliszyk, Josef Urban:
Machine Learning Guidance and Proof Certification for Connection Tableaux. CoRR abs/1805.03107 (2018)
[i21]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1805-06502
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1805-06502
Qingxiang Wang, Cezary Kaliszyk, Josef Urban:
First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR abs/1805.06502 (2018)
[i20]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1805-07563
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1805-07563
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák:
Reinforcement Learning of Theorem Proving. CoRR abs/1805.07563 (2018)
2017
[j13]
- view
  - electronic edition @ isa-afp.org
- export record
  dblp key:
  - journals/afp/ParsertK17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/afp/ParsertK17
Julian Parsert, Cezary Kaliszyk:
Microeconomics and the First Welfare Theorem. Archive of Formal Proofs 2017 (2017)
[c58]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cade/FarberKU17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/FarberKU17
Michael Färber, Cezary Kaliszyk, Josef Urban:
Monte Carlo Tableau Proof Search. CADE 2017: 563-579
[c57]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/fedcsis/KaliszykP17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/fedcsis/KaliszykP17
Cezary Kaliszyk, Karol Pak:
Progress in the Independent Certification of Mizar Mathematical Library in Isabelle. FedCSIS 2017: 227-236
[c56]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/KaliszykUV17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/KaliszykUV17
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017: 12-27
[c55]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/lpar/LoosISK17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/LoosISK17
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk:
Deep Network Guided Proof Search. LPAR 2017: 85-105
[c54]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/lpar/GauthierKU17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/GauthierKU17
Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
TacticToe: Learning to Reason with HOL4 Tactics. LPAR 2017: 125-143
[c53]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/macis/KaliszykP17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/macis/KaliszykP17
Cezary Kaliszyk, Karol Pak:
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions. MACIS 2017: 163-178
[c52]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/MullerGKKR17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/MullerGKKR17
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe:
Classification of Alignments Between Concepts of Formal Mathematical Systems. CICM 2017: 83-98
[c51]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykP17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykP17
Cezary Kaliszyk, Karol Pak:
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. CICM 2017: 193-207
[i19]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/LoosISK17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/LoosISK17
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk:
Deep Network Guided Proof Search. CoRR abs/1701.06972 (2017)
[i18]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykCS17
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykCS17
Cezary Kaliszyk, François Chollet, Christian Szegedy:
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. CoRR abs/1703.00426 (2017)
2016
[j12]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/BlanchetteGKKU16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/BlanchetteGKKU16
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban:
A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reasoning 57(3): 219-244 (2016)
[j11]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jfrea/BlanchetteKPU16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jfrea/BlanchetteKPU16
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formalized Reasoning 9(1): 101-148 (2016)
[c50]
- view
  - electronic edition @ ceur-ws.org
- export record
  dblp key:
  - conf/cade/FarberK16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/FarberK16
Michael Färber, Cezary Kaliszyk:
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. PAAR@IJCAR 2016: 24-31
[c49]
- view
  - electronic edition @ ceur-ws.org
- export record
  dblp key:
  - conf/cade/KaliszykSR16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykSR16
Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe:
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. PAAR@IJCAR 2016: 41-55
[c48]
- view
  - electronic edition @ ceur-ws.org
- export record
  dblp key:
  - conf/cikm/GauthierKU16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cikm/GauthierKU16
Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
Initial Experiments with Statistical Conjecturing over Large Formal Corpora. FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016: 219-228
[c47]
- view
  - electronic edition @ ceur-ws.org
- export record
  dblp key:
  - conf/cikm/KaliszykKMR16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cikm/KaliszykKMR16
Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe:
A Standard for Aligning Mathematical Concepts. FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016: 229-244
[c46]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/KaliszykPU16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KaliszykPU16
Cezary Kaliszyk, Karol Pak, Josef Urban:
Towards a mizar environment for isabelle: foundations and language. CPP 2016: 58-65
[c45]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/fase/0001K16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/fase/0001K16
David Aspinall, Cezary Kaliszyk:
Towards Formal Proof Metrics. FASE 2016: 325-341
[c44]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/0001K16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/0001K16
David Aspinall, Cezary Kaliszyk:
What's in a Theorem Name? ITP 2016: 459-465
[c43]
- view
  - electronic edition via DOI
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/CzajkaK16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/CzajkaK16
Lukasz Czajka, Cezary Kaliszyk:
Goal Translation for a Hammer for Coq (Extended Abstract). HaTT@IJCAR 2016: 13-20
[e4]
- view
- export record
  dblp key:
  - journals/corr/BlanchetteK16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/BlanchetteK16
Jasmin Christian Blanchette, Cezary Kaliszyk:
Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016. EPTCS 210, 2016 [contents]
[i17]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/FarberKU16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/FarberKU16
Michael Färber, Cezary Kaliszyk, Josef Urban:
Monte Carlo Connection Prover. CoRR abs/1611.05990 (2016)
[i16]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykUV16
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykUV16
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving. CoRR abs/1611.09703 (2016)
2015
[j10]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/KaliszykU15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/KaliszykU15
Cezary Kaliszyk, Josef Urban:
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 54(1): 99 (2015)
[j9]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/KaliszykU15a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/KaliszykU15a
Cezary Kaliszyk, Josef Urban:
MizAR 40 for Mizar 40. J. Autom. Reasoning 55(3): 245-256 (2015)
[j8]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jsc/KaliszykU15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jsc/KaliszykU15
Cezary Kaliszyk, Josef Urban:
Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015)
[j7]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/mics/KaliszykU15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/mics/KaliszykU15
Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. Mathematics in Computer Science 9(1): 5-22 (2015)
[c42]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cade/KaliszykSUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykSUV15
Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil:
System Description: E.T. 0.1. CADE 2015: 389-398
[c41]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/GauthierK15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/GauthierK15
Thibault Gauthier, Cezary Kaliszyk:
Premise Selection and External Provers for HOL4. CPP 2015: 49-57
[c40]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/cpp/KaliszykUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KaliszykUV15
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP 2015: 59-66
[c39]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/frocos/FarberK15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/frocos/FarberK15
Michael Färber, Cezary Kaliszyk:
Random Forests for Premise Selection. FroCos 2015: 325-340
[c38]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/frocos/KaliszykUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/frocos/KaliszykUV15
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Lemmatization for Stronger Reasoning in Large Theories. FroCos 2015: 341-356
[c37]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/gcai/FarberK15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/gcai/FarberK15
Michael Färber, Cezary Kaliszyk:
Metis-based Paramodulation Tactic for HOL Light. GCAI 2015: 127-136
[c36]
- view
  - electronic edition @ ijcai.org
- export record
  dblp key:
  - conf/ijcai/KaliszykUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/ijcai/KaliszykUV15
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI 2015: 3084-3090
[c35]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/KaliszykUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/KaliszykUV15
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Learning to Parse on Aligned Corpora (Rough Diamond). ITP 2015: 227-233
[c34]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/lpar/KaliszykUV15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/KaliszykUV15
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Improving Statistical Linguistic Algorithms for Parsing Mathematics. IWIL@LPAR 2015: 27-36
[c33]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lpar/KaliszykU15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/KaliszykU15
Cezary Kaliszyk, Josef Urban:
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. LPAR 2015: 88-96
[c32]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lpar/GauthierK15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/GauthierK15
Thibault Gauthier, Cezary Kaliszyk:
Sharing HOL4 and HOL Light Proof Knowledge. LPAR 2015: 372-386
[c31]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykUSADT15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykUSADT15
Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar:
Formalizing Physics: Automation, Presentation and Foundation Issues. CICM 2015: 288-295
[c30]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/tableaux/Kaliszyk15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/tableaux/Kaliszyk15
Cezary Kaliszyk:
Efficient Low-Level Connection Tableaux. TABLEAUX 2015: 102-111
[e3]
- view
  - table of contents in dblp
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/2015
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/2015
Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge:
Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings. Lecture Notes in Computer Science 9150, Springer 2015, ISBN 978-3-319-20614-1 [contents]
[e2]
- view
- export record
  dblp key:
  - journals/corr/KaliszykP15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykP15
Cezary Kaliszyk, Andrei Paskevich:
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. EPTCS 186, 2015 [contents]
[i15]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/HalesABDHHKMMNNNOPRSTTTUVZ15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/HalesABDHHKMMNNNOPRSTTTUVZ15
Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller:
A formal proof of the Kepler conjecture. CoRR abs/1501.02155 (2015)
[i14]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/GauthierK15
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/GauthierK15
Thibault Gauthier, Cezary Kaliszyk:
Sharing HOL4 and HOL Light proof knowledge. CoRR abs/1509.03527 (2015)
[i13]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/GauthierK15a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/GauthierK15a
Thibault Gauthier, Cezary Kaliszyk:
Premise Selection and External Provers for HOL4. CoRR abs/1509.03534 (2015)
2014
[j6]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jar/KaliszykU14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jar/KaliszykU14
Cezary Kaliszyk, Josef Urban:
Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53(2): 173-213 (2014)
[c29]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/cade/GauthierKKN14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/GauthierKKN14
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish:
Beagle as a HOL4 external ATP method. PAAR@IJCAR 2014: 50-59
[c28]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/cade/KaliszykUV14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykUV14
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. PAAR@IJCAR 2014: 60-66
[c27]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/GauthierK14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/GauthierK14
Thibault Gauthier, Cezary Kaliszyk:
Matching Concepts across HOL Libraries. CICM 2014: 267-281
[c26]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykR14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykR14
Cezary Kaliszyk, Florian Rabe:
Towards Knowledge Management for HOL Light. CICM 2014: 357-372
[c25]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykUVG14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykUVG14
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM 2014: 435-439
[c24]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/semweb/KaliszykU14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/semweb/KaliszykU14
Cezary Kaliszyk, Josef Urban:
Wikis and Collaborative Systems for Large Formal Mathematics. SWCS (LNCS Volume) 2014: 35-52
[c23]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/sycss/KaliszykMU14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/sycss/KaliszykMU14
Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. SCSS 2014: 27-34
[c22]
- view
  - electronic edition via DOI
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/JoostenKU14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/JoostenKU14
Sebastiaan Joosten, Cezary Kaliszyk, Josef Urban:
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. ACL2 2014: 77-85
[i12]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykUV14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykUV14
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. CoRR abs/1402.2359 (2014)
[i11]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykU14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykU14
Cezary Kaliszyk, Josef Urban:
Learning-assisted Theorem Proving with Millions of Lemmas. CoRR abs/1402.3578 (2014)
[i10]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykUVG14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykUVG14
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. CoRR abs/1405.3451 (2014)
[i9]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/GauthierK14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/GauthierK14
Thibault Gauthier, Cezary Kaliszyk:
Matching concepts across HOL libraries. CoRR abs/1405.3906 (2014)
[i8]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykMU14
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykMU14
Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. CoRR abs/1410.5467 (2014)
[i7]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykUV14a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykUV14a
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CoRR abs/1410.5476 (2014)
2013
[c21]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/cade/KaliszykS13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykS13
Cezary Kaliszyk, Thomas Sternagel:
Initial Experiments on Deriving a Complete HOL Simplification Set. PxTP@CADE 2013: 77-86
[c20]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/cade/KaliszykU13a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykU13a
Cezary Kaliszyk, Josef Urban:
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE 2013: 87-95
[c19]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cade/KaliszykU13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykU13
Cezary Kaliszyk, Josef Urban:
PRocH: Proof Reconstruction for HOL Light. CADE 2013: 267-274
[c18]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/KuhlweinBKU13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/KuhlweinBKU13
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban:
MaSh: Machine Learning for Sledgehammer. ITP 2013: 35-50
[c17]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/KaliszykK13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/KaliszykK13
Cezary Kaliszyk, Alexander Krauss:
Scalable LCF-Style Proof Translation. ITP 2013: 51-66
[c16]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/itp/TankinkKUG13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/itp/TankinkKUG13
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456
[c15]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/lpar/KaliszykU13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/lpar/KaliszykU13
Cezary Kaliszyk, Josef Urban:
Lemma Mining over HOL Light. LPAR 2013: 503-517
[c14]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykU13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykU13
Cezary Kaliszyk, Josef Urban:
Automated Reasoning Service for HOL Light. MKM/Calculemus/DML 2013: 120-135
[c13]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/TankinkKUG13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/TankinkKUG13
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML 2013: 152-167
[e1]
- view
- export record
  dblp key:
  - journals/corr/KaliszykL13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykL13
Cezary Kaliszyk, Christoph Lüth:
Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012. EPTCS 118, 2013 [contents]
[i6]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1305-5710
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1305-5710
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. CoRR abs/1305.5710 (2013)
[i5]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykU13
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykU13
Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. CoRR abs/1309.4962 (2013)
[i4]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykU13a
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykU13a
Cezary Kaliszyk, Josef Urban:
Lemma Mining over HOL Light. CoRR abs/1310.2797 (2013)
[i3]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/KaliszykU13b
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/KaliszykU13b
Cezary Kaliszyk, Josef Urban:
MizAR 40 for Mizar 40. CoRR abs/1310.2805 (2013)
2012
[j5]
- view
  - electronic edition via DOI
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1206-0136
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1206-0136
Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science 8(2) (2012)
[c12]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/adg/GhourabiKK12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/adg/GhourabiKK12
Fadoua Ghourabi, Asem Kasem, Cezary Kaliszyk:
Algebraic Analysis of Huzita's Origami Operations and Their Extensions. Automated Deduction in Geometry 2012: 143-160
[c11]
- view
  - electronic edition @ easychair.org
- export record
  dblp key:
  - conf/cade/KaliszykU12
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cade/KaliszykU12
Cezary Kaliszyk, Josef Urban:
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. PAAR@IJCAR 2012: 72-81
[i2]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-1211-7012
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-1211-7012
Cezary Kaliszyk, Josef Urban:
Learning-assisted Automated Reasoning with Flyspeck. CoRR abs/1211.7012 (2012)
2011
[c10]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/cpp/KaliszykB11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/cpp/KaliszykB11
Cezary Kaliszyk, Henk Barendregt:
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. CPP 2011: 87-102
[c9]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/esop/UrbanK11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/esop/UrbanK11
Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP 2011: 480-500
[c8]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykI11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykI11
Cezary Kaliszyk, Tetsuo Ida:
Proof Assistant Decision Procedures for Formalizing Origami. Calculemus/MKM 2011: 45-57
[c7]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - conf/sac/KaliszykU11
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/sac/KaliszykU11
Cezary Kaliszyk, Christian Urban:
Quotients revisited for Isabelle/HOL. SAC 2011: 1639-1644
2010
[j4]
- view
  - electronic edition @ acm.org
- export record
  dblp key:
  - journals/cca/HaftmannKN10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/cca/HaftmannKN10
Florian Haftmann, Cezary Kaliszyk, Walther Neuper:
CTP-based programming languages?: considerations about an experimental design. ACM Comm. Computer Algebra 44(1/2): 27-41 (2010)
[j3]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/fm/Kaliszyk10
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/fm/Kaliszyk10
Cezary Kaliszyk:
Counting Derangements, Non Bijective Functions and the Birthday Problem. Formalized Mathematics 18(1-4): 197-200 (2010)

2000 – 2009

see FAQ

What is the meaning of the colors in the publication lists?

2009
[j2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/jfrea/KaliszykO09
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/jfrea/KaliszykO09
Cezary Kaliszyk, Russell O'Connor:
Computing with Classical Real Numbers. J. Formalized Reasoning 2(1): 27-39 (2009)
2008
[c6]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/aisc/Kaliszyk08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/aisc/Kaliszyk08
Cezary Kaliszyk:
Automating Side Conditions in Formalized Partial Functions. AISC/MKM/Calculemus 2008: 300-314
[c5]
- view
  - electronic edition @ ceur-ws.org
- export record
  dblp key:
  - conf/semwiki/KaliszykCWMG08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/semwiki/KaliszykCWMG08
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008
[c4]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/types/KaliszykW08
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/types/KaliszykW08
Cezary Kaliszyk, Freek Wiedijk:
Merging Procedural and Declarative Proof. TYPES 2008: 203-219
[i1]
- view
  - electronic edition @ arxiv.org
- export record
  dblp key:
  - journals/corr/abs-0809-1644
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/corr/abs-0809-1644
Cezary Kaliszyk, Russell O'Connor:
Computing with Classical Real Numbers. CoRR abs/0809.1644 (2008)
2007
[j1]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - journals/entcs/Kaliszyk07
- ask others
- share record
  short URL:
  - https://dblp.org/rec/journals/entcs/Kaliszyk07
Cezary Kaliszyk:
Web Interfaces for Proof Assistants. Electr. Notes Theor. Comput. Sci. 174(2): 49-61 (2007)
[c3]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/KaliszykW07
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/KaliszykW07
Cezary Kaliszyk, Freek Wiedijk:
Certified Computer Algebra on Top of an Interactive Theorem Prover. Calculemus/MKM 2007: 94-105
[c2]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/mkm/CorbineauK07
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/mkm/CorbineauK07
Pierre Corbineau, Cezary Kaliszyk:
Cooperative Repositories for Formal Proofs. Calculemus/MKM 2007: 221-234
2004
[c1]
- view
  - electronic edition via DOI
- export record
  dblp key:
  - conf/icwe/AndruszkiewiczCGKS04
- ask others
- share record
  short URL:
  - https://dblp.org/rec/conf/icwe/AndruszkiewiczCGKS04
Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, Mateusz Srebrny:
SIE - Intelligent Web Proxy Framework. ICWE 2004: 373-385

Coauthor Index

see FAQ

maintained by

at