Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarCezary Kaliszyk
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
- 2017
[j13]Julian Parsert, Cezary Kaliszyk:
Microeconomics and the First Welfare Theorem. Archive of Formal Proofs 2017 (2017)- [c56]
- [c55]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017: 12-27 - [c54]Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk:
Deep Network Guided Proof Search. LPAR 2017: 85-105 - [c53]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
TacticToe: Learning to Reason with HOL4 Tactics. LPAR 2017: 125-143 - [c52]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]
- [i19]Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk:
Deep Network Guided Proof Search. CoRR abs/1701.06972 (2017) - [i18]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]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]Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formalized Reasoning 9(1): 101-148 (2016) - [c50]Michael Färber, Cezary Kaliszyk:
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. PAAR@IJCAR 2016: 24-31 - [c49]Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe:
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. PAAR@IJCAR 2016: 41-55 - [c48]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]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]Cezary Kaliszyk, Karol Pak, Josef Urban:
Towards a mizar environment for isabelle: foundations and language. CPP 2016: 58-65 - [c45]
- [c44]
- [c43]Lukasz Czajka, Cezary Kaliszyk:
Goal Translation for a Hammer for Coq (Extended Abstract). HaTT@IJCAR 2016: 13-20 - [e4]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]Michael Färber, Cezary Kaliszyk, Josef Urban:
Monte Carlo Connection Prover. CoRR abs/1611.05990 (2016) - [i16]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]Cezary Kaliszyk, Josef Urban:
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 54(1): 99 (2015) - [j9]
- [j8]Cezary Kaliszyk, Josef Urban:
Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015) - [j7]Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. Mathematics in Computer Science 9(1): 5-22 (2015) - [c42]Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil:
System Description: E.T. 0.1. CADE 2015: 389-398 - [c41]Thibault Gauthier, Cezary Kaliszyk:
Premise Selection and External Provers for HOL4. CPP 2015: 49-57 - [c40]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP 2015: 59-66 - [c39]
- [c38]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Lemmatization for Stronger Reasoning in Large Theories. FroCos 2015: 341-356 - [c37]Michael Färber, Cezary Kaliszyk:
Metis-based Paramodulation Tactic for HOL Light. GCAI 2015: 127-136 - [c36]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI 2015: 3084-3090 - [c35]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Learning to Parse on Aligned Corpora (Rough Diamond). ITP 2015: 227-233 - [c34]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Improving Statistical Linguistic Algorithms for Parsing Mathematics. IWIL@LPAR 2015: 27-36 - [c33]Cezary Kaliszyk, Josef Urban:
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. LPAR 2015: 88-96 - [c32]
- [c31]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]
- [e3]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]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]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 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]Thibault Gauthier, Cezary Kaliszyk:
Sharing HOL4 and HOL Light proof knowledge. CoRR abs/1509.03527 (2015) - [i13]Thibault Gauthier, Cezary Kaliszyk:
Premise Selection and External Provers for HOL4. CoRR abs/1509.03534 (2015) - 2014
- [j6]Cezary Kaliszyk, Josef Urban:
Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53(2): 173-213 (2014) - [c29]Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish:
Beagle as a HOL4 external ATP method. PAAR@IJCAR 2014: 50-59 - [c28]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. PAAR@IJCAR 2014: 60-66 - [c27]
- [c26]
- [c25]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]Cezary Kaliszyk, Josef Urban:
Wikis and Collaborative Systems for Large Formal Mathematics. SWCS (LNCS Volume) 2014: 35-52 - [c23]Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. SCSS 2014: 27-34 - [c22]Sebastiaan Joosten, Cezary Kaliszyk, Josef Urban:
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. ACL2 2014: 77-85 - [i12]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. CoRR abs/1402.2359 (2014) - [i11]Cezary Kaliszyk, Josef Urban:
Learning-assisted Theorem Proving with Millions of Lemmas. CoRR abs/1402.3578 (2014) - [i10]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]Thibault Gauthier, Cezary Kaliszyk:
Matching concepts across HOL libraries. CoRR abs/1405.3906 (2014) - [i8]Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. CoRR abs/1410.5467 (2014) - [i7]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CoRR abs/1410.5476 (2014) - 2013
- [c21]Cezary Kaliszyk, Thomas Sternagel:
Initial Experiments on Deriving a Complete HOL Simplification Set. PxTP@CADE 2013: 77-86 - [c20]Cezary Kaliszyk, Josef Urban:
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE 2013: 87-95 - [c19]
- [c18]Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban:
MaSh: Machine Learning for Sledgehammer. ITP 2013: 35-50 - [c17]
- [c16]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456 - [c15]
- [c14]Cezary Kaliszyk, Josef Urban:
Automated Reasoning Service for HOL Light. MKM/Calculemus/DML 2013: 120-135 - [c13]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML 2013: 152-167 - [e1]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]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. CoRR abs/1305.5710 (2013) - [i5]Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. CoRR abs/1309.4962 (2013) - [i4]
- [i3]
- 2012
- [j5]Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science 8(2) (2012) - [c12]Fadoua Ghourabi, Asem Kasem, Cezary Kaliszyk:
Algebraic Analysis of Huzita's Origami Operations and Their Extensions. Automated Deduction in Geometry 2012: 143-160 - [c11]Cezary Kaliszyk, Josef Urban:
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. PAAR@IJCAR 2012: 72-81 - [i2]Cezary Kaliszyk, Josef Urban:
Learning-assisted Automated Reasoning with Flyspeck. CoRR abs/1211.7012 (2012) - 2011
- [c10]Cezary Kaliszyk, Henk Barendregt:
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. CPP 2011: 87-102 - [c9]Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP 2011: 480-500 - [c8]Cezary Kaliszyk, Tetsuo Ida:
Proof Assistant Decision Procedures for Formalizing Origami. Calculemus/MKM 2011: 45-57 - [c7]
- 2010
- [j4]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]Cezary Kaliszyk:
Counting Derangements, Non Bijective Functions and the Birthday Problem. Formalized Mathematics 18(1-4): 197-200 (2010)
2000 – 2009
- 2009
- [j2]Cezary Kaliszyk, Russell O'Connor:
Computing with Classical Real Numbers. J. Formalized Reasoning 2(1): 27-39 (2009) - 2008
- [c6]Cezary Kaliszyk:
Automating Side Conditions in Formalized Partial Functions. AISC/MKM/Calculemus 2008: 300-314 - [c5]Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008 - [c4]
- [i1]
- 2007
- [j1]Cezary Kaliszyk:
Web Interfaces for Proof Assistants. Electr. Notes Theor. Comput. Sci. 174(2): 49-61 (2007) - [c3]Cezary Kaliszyk, Freek Wiedijk:
Certified Computer Algebra on Top of an Interactive Theorem Prover. Calculemus/MKM 2007: 94-105 - [c2]Pierre Corbineau, Cezary Kaliszyk:
Cooperative Repositories for Formal Proofs. Calculemus/MKM 2007: 221-234 - 2004
- [c1]Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, Mateusz Srebrny:
SIE - Intelligent Web Proxy Framework. ICWE 2004: 373-385
Coauthor Index
maintained by 
at 
at 
data released under the ODC-BY 1.0 license; see also our legal information page
last updated on 2017-09-21 00:11 CEST by the dblp team