default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDCezary Kaliszyk
Person information
- affiliation: University of Innsbruck, Austria
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c98]Lasse Blaauwbroek, David M. Cerna
, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban:
Learning Guided Automated Reasoning: A Brief Survey. Logics and Type Systems in Theory and Practice 2024: 54-83- [c97]Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk:
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. IJCAR (1) 2024: 86-104 - [c96]Karol Pak, Cezary Kaliszyk:
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. ITP 2024: 29:1-29:18 - [c95]Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk:
Experiments with Choice in Dependently-Typed Higher-Order Logic. LPAR 2024: 311-320 - [c94]Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk:
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery. LPAR 2024: 360-369 - [i44]Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban:
Learning Guided Automated Reasoning: A Brief Survey. CoRR abs/2403.04017 (2024) - [i43]Karol Pak, Cezary Kaliszyk:
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. CoRR abs/2410.00065 (2024) - 2023
- [j24]Cezary Kaliszyk, Karol Pak:
Combining Higher-Order Logic with Set Theory Formalizations. J. Autom. Reason. 67(2): 20 (2023) - [c93]Cezary Kaliszyk:
Improved Assistance for Interactive Proof (Keynote). CPP 2023: 2 - [c92]Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban:
Learning Proof Transformations and Its Applications in Interactive Theorem Proving. FroCoS 2023: 236-254 - [c91]Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban:
MizAR 60 for Mizar 50. ITP 2023: 19:1-19:22 - [c90]Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk:
Experiments on Infinite Model Finding in SMT Solving. LPAR 2023: 317-328 - [c89]Jan Jakubuv, Cezary Kaliszyk:
VizAR: Visualization of Automated Reasoning Proofs (System Description). CICM 2023: 303-308 - [i42]Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban:
MizAR 60 for Mizar 50. CoRR abs/2303.06686 (2023) - 2022
- [c88]Chad E. Brown, Cezary Kaliszyk:
Lash 1.0 (System Description). IJCAR 2022: 350-358 - [c87]Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban:
Proofgold: Blockchain for Formal Methods. FMBC@CAV 2022: 4:1-4:15 - [c86]Stanislaw J. Purgal, Cezary Kaliszyk:
Adversarial Learning to Reason in an Arbitrary Logic. FLAIRS 2022 - [c85]Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk:
Learning Higher-Order Logic Programs From Failures. IJCAI 2022: 2726-2733 - [c84]Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban:
The Isabelle ENIGMA. ITP 2022: 16:1-16:21 - [c83]Karol Pak, Cezary Kaliszyk:
Formalizing a Diophantine Representation of the Set of Prime Numbers. ITP 2022: 26:1-26:8 - [c82]Grzegorz Prusak, Cezary Kaliszyk:
Lazy Paramodulation in Practice. PAAR@IJCAR 2022 - [c81]Chad E. Brown, Mikolás Janota, Cezary Kaliszyk:
Abstract: Challenges and Solutions for Higher-Order SMT Proofs. SMT 2022: 128 - [i41]Stanislaw J. Purgal, Cezary Kaliszyk:
Adversarial Learning to Reason in an Arbitrary Logic. CoRR abs/2204.02737 (2022) - [i40]Karol Pak, Cezary Kaliszyk:
Formalizing a Diophantine Representation of the Set of Prime Numbers. CoRR abs/2204.12311 (2022) - [i39]Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban:
The Isabelle ENIGMA. CoRR abs/2205.01981 (2022) - [i38]Chad E. Brown, Cezary Kaliszyk:
Lash 1.0 (System Description). CoRR abs/2205.06640 (2022) - [i37]Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk:
Differentiable Inductive Logic Programming in High-Dimensional Space. CoRR abs/2208.06652 (2022) - 2021
- [j23]Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65(2): 257-286 (2021) - [j22]Michael Färber, Cezary Kaliszyk, Josef Urban:
Machine Learning Guidance for Connection Tableaux. J. Autom. Reason. 65(2): 287-320 (2021) - [j21]Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk:
A study of continuous vector representations for theorem proving. J. Log. Comput. 31(8): 2057-2083 (2021) - [c80]Qingxiang Wang, Cezary Kaliszyk:
JEFL: Joint Embedding of Formal Proof Libraries. FroCoS 2021: 154-170 - [c79]Dennis Müller, Cezary Kaliszyk:
Disambiguating Symbolic Expressions in Informal Documents. ICLR 2021 - [c78]Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban:
Online Machine Learning Techniques for Coq: A Comparison. CICM 2021: 67-83 - [c77]Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:
Towards Finding Longer Proofs. TABLEAUX 2021: 167-186 - [e9]Liron Cohen, Cezary Kaliszyk:
12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). LIPIcs 193, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021, ISBN 978-3-95977-188-7 [contents] - [i36]Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk:
A Study of Continuous Vector Representationsfor Theorem Proving. CoRR abs/2101.09142 (2021) - [i35]Dennis Müller, Cezary Kaliszyk:
Disambiguating Symbolic Expressions in Informal Documents. CoRR abs/2101.11716 (2021) - [i34]Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban:
Online Machine Learning Techniques for Coq: A Comparison. CoRR abs/2104.05207 (2021) - [i33]Qingxiang Wang, Cezary Kaliszyk:
JEFL: Joint Embedding of Formal Proof Libraries. CoRR abs/2107.10188 (2021) - [i32]Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk:
Learning Higher-Order Programs without Meta-Interpretive Learning. CoRR abs/2112.14603 (2021) - 2020
- [j20]Burak Ekici, Cezary Kaliszyk:
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq. Math. Comput. Sci. 14(3): 533-549 (2020) - [j19]Jan Jakubuv, Cezary Kaliszyk:
Relaxed Weighted Path Order in Theorem Proving. Math. Comput. Sci. 14(3): 657-670 (2020) - [c76]Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban:
Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP 2020: 85-98 - [c75]Miroslav Olsák, Cezary Kaliszyk, Josef Urban:
Property Invariant Embedding for Automated Reasoning. ECAI 2020: 1395-1402 - [c74]Julian Parsert, Stephanie Autherith, Cezary Kaliszyk:
Property Preserving Embedding of First-order Logic. GCAI 2020: 70-82 - [c73]Cezary Kaliszyk, Florian Rabe:
A Survey of Languages for Formalizing Mathematics. CICM 2020: 138-156 - [e8]Edwin C. Brady, James H. Davenport, William M. Farmer, Cezary Kaliszyk, Andrea Kohlhase, Michael Kohlhase, Dennis Müller, Karol Pak, Claudio Sacerdoti Coen:
Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague, Czech Republic, July 8-12, 2019. CEUR Workshop Proceedings 2634, CEUR-WS.org 2020 [contents] - [i31]Cezary Kaliszyk, Florian Rabe:
A Survey of Languages for Formalizing Mathematics. CoRR abs/2005.12876 (2020)
2010 – 2019
- 2019
- [j18]Julian Parsert, Cezary Kaliszyk:
Linear Programming. Arch. Formal Proofs 2019 (2019) - [j17]Cezary Kaliszyk, Karol Pak:
Semantics of Mizar as an Isabelle Object Logic. J. Autom. Reason. 63(3): 557-595 (2019) - [j16]Thibault Gauthier, Cezary Kaliszyk:
Aligning concepts across proof assistant libraries. J. Symb. Comput. 90: 89-123 (2019) - [c72]Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban:
GRUNGE: A Grand Unified ATP Challenge. CADE 2019: 123-141 - [c71]Chad E. Brown, Cezary Kaliszyk, Karol Pak:
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ITP 2019: 9:1-9:16 - [c70]Cezary Kaliszyk, Karol Pak:
Declarative Proof Translation (Short Paper). ITP 2019: 35:1-35:7 - [c69]Michael Färber, Cezary Kaliszyk:
Certification of Nonclausal Connection Tableaux Proofs. TABLEAUX 2019: 21-38 - [e7]Osman Hasan, Abdou Youssef, Adam Naumowicz, William M. Farmer, Cezary Kaliszyk, Diane Gallois-Wong, Florian Rabe, Gabriel Dos Reis, Grant O. Passmore, James H. Davenport, Markus Pfeiffer, Michael Kohlhase, Serge Autexier, Sofiène Tahar, Thomas Koprucki, Umair Siddique, Walther Neuper, Wolfgang Windsteiger, Wolfgang Schreiner, Wolfram Sperber, Zoltán Kovács:
Joint Proceedings of the CME-EI, FMM, CAAT, FVPS, M3SRD, OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2018 co-located with the 11th Conference on Intelligent Computer Mathematics (CICM 2018), Hagenberg, Austria, August 13-17, 2018. CEUR Workshop Proceedings 2307, CEUR-WS.org 2019 [contents] - [e6]Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, Claudio Sacerdoti Coen:
Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings. Lecture Notes in Computer Science 11617, Springer 2019, ISBN 978-3-030-23249-8 [contents] - [i30]Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban:
GRUNGE: A Grand Unified ATP Challenge. CoRR abs/1903.02539 (2019) - [i29]Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:
Towards Finding Longer Proofs. CoRR abs/1905.13100 (2019) - [i28]Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk:
Can Neural Networks Learn Symbolic Rewriting? CoRR abs/1911.04873 (2019) - [i27]Miroslav Olsák, Cezary Kaliszyk, Josef Urban:
Property Invariant Embedding for Automated Reasoning. CoRR abs/1911.12073 (2019) - [i26]Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban:
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CoRR abs/1912.02636 (2019) - 2018
- [j15]Julian Parsert, Cezary Kaliszyk:
Von-Neumann-Morgenstern Utility Theorem. Arch. Formal Proofs 2018 (2018) - [j14]Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban:
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31(3): 235-236 (2018) - [j13]Lukasz Czajka, Cezary Kaliszyk:
Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason. 61(1-4): 423-453 (2018) - [c68]Cezary Kaliszyk, Julian Parsert:
Formal microeconomic foundations and the first welfare theorem. CPP 2018: 91-101 - [c67]Jan Jakubuv, Cezary Kaliszyk:
Towards a Unified Ordering for Superposition-Based Automated Reasoning. ICMS 2018: 245-254 - [c66]Julian Parsert, Cezary Kaliszyk:
Towards Formal Foundations for Game Theory. ITP 2018: 495-503 - [c65]Lukasz Czajka, Burak Ekici, Cezary Kaliszyk:
Concrete Semantics with Coq and CoqHammer. CICM 2018: 53-59 - [c64]Cezary Kaliszyk, Karol Pak:
Isabelle Import Infrastructure for the Mizar Mathematical Library. CICM 2018: 131-146 - [c63]Qingxiang Wang, Cezary Kaliszyk, Josef Urban:
First Experiments with Neural Translation of Informal to Formal Mathematics. CICM 2018: 255-270 - [c62]Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák:
Reinforcement Learning of Theorem Proving. NeurIPS 2018: 8836-8847 - [i25]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
Learning to Reason with HOL4 tactics. CoRR abs/1804.00595 (2018) - [i24]Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
Learning to Prove with Tactics. CoRR abs/1804.00596 (2018) - [i23]Michael Färber, Cezary Kaliszyk, Josef Urban:
Machine Learning Guidance and Proof Certification for Connection Tableaux. CoRR abs/1805.03107 (2018) - [i22]Qingxiang Wang, Cezary Kaliszyk, Josef Urban:
First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR abs/1805.06502 (2018) - [i21]Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák:
Reinforcement Learning of Theorem Proving. CoRR abs/1805.07563 (2018) - [i20]Lukasz Czajka, Burak Ekici, Cezary Kaliszyk:
Concrete Semantics with Coq and CoqHammer. CoRR abs/1808.06413 (2018) - 2017
- [j12]Julian Parsert, Cezary Kaliszyk:
Microeconomics and the First Welfare Theorem. Arch. Formal Proofs 2017 (2017) - [c61]Michael Färber, Cezary Kaliszyk, Josef Urban:
Monte Carlo Tableau Proof Search. CADE 2017: 563-579 - [c60]Cezary Kaliszyk, Karol Pak:
Progress in the Independent Certification of Mizar Mathematical Library in Isabelle. FedCSIS 2017: 227-236 - [c59]Cezary Kaliszyk, François Chollet, Christian Szegedy:
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. ICLR (Poster) 2017 - [c58]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017: 12-27 - [c57]Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk:
Deep Network Guided Proof Search. LPAR 2017: 85-105 - [c56]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
TacticToe: Learning to Reason with HOL4 Tactics. LPAR 2017: 125-143 - [c55]Cezary Kaliszyk, Karol Pak:
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions. MACIS 2017: 163-178 - [c54]Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe:
Classification of Alignments Between Concepts of Formal Mathematical Systems. CICM 2017: 83-98 - [c53]Cezary Kaliszyk, Karol Pak:
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. CICM 2017: 193-207 - [c52]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
System Description: Statistical Parsing of Informalized Mizar Formulas. SYNASC 2017: 169-172 - [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
- [j11]Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban:
A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reason. 57(3): 219-244 (2016) - [j10]Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formaliz. Reason. 9(1): 101-148 (2016) - [c51]Michael Färber, Cezary Kaliszyk:
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. PAAR@IJCAR 2016: 24-31 - [c50]Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe:
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. PAAR@IJCAR 2016: 41-55 - [c49]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
Initial Experiments with Statistical Conjecturing over Large Formal Corpora. FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016: 219-228 - [c48]Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe:
A Standard for Aligning Mathematical Concepts. FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016: 229-244 - [c47]Cezary Kaliszyk, Karol Pak, Josef Urban:
Towards a mizar environment for isabelle: foundations and language. CPP 2016: 58-65 - [c46]David Aspinall, Cezary Kaliszyk:
Towards Formal Proof Metrics. FASE 2016: 325-341 - [c45]David Aspinall, Cezary Kaliszyk:
What's in a Theorem Name? ITP 2016: 459-465 - [c44]Lukasz Czajka, Cezary Kaliszyk:
Goal Translation for a Hammer for Coq (Extended Abstract). HaTT@IJCAR 2016: 13-20 - [e5]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
- [j9]Cezary Kaliszyk, Josef Urban:
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reason. 54(1): 99 (2015) - [j8]Cezary Kaliszyk, Josef Urban:
MizAR 40 for Mizar 40. J. Autom. Reason. 55(3): 245-256 (2015) - [j7]Cezary Kaliszyk, Josef Urban:
Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015) - [j6]Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. Math. Comput. Sci. 9(1): 5-22 (2015) - [c43]Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil:
System Description: E.T. 0.1. CADE 2015: 389-398 - [c42]Thibault Gauthier, Cezary Kaliszyk:
Premise Selection and External Provers for HOL4. CPP 2015: 49-57 - [c41]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP 2015: 59-66 - [c40]Michael Färber, Cezary Kaliszyk:
Random Forests for Premise Selection. FroCos 2015: 325-340 - [c39]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Lemmatization for Stronger Reasoning in Large Theories. FroCos 2015: 341-356 - [c38]Michael Färber, Cezary Kaliszyk:
Metis-based Paramodulation Tactic for HOL Light. GCAI 2015: 127-136 - [c37]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI 2015: 3084-3090 - [c36]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Learning to Parse on Aligned Corpora (Rough Diamond). ITP 2015: 227-233 - [c35]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Improving Statistical Linguistic Algorithms for Parsing Mathematics. IWIL@LPAR 2015: 27-36 - [c34]Cezary Kaliszyk, Josef Urban:
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. LPAR 2015: 88-96 - [c33]Thibault Gauthier, Cezary Kaliszyk:
Sharing HOL4 and HOL Light Proof Knowledge. LPAR 2015: 372-386 - [c32]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 - [c31]Cezary Kaliszyk:
Efficient Low-Level Connection Tableaux. TABLEAUX 2015: 102-111 - [e4]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] - [e3]Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge:
CICM 2015 - Informal Work in Progress Proceedings, Washington, DC, USA, July 13-17, 2015. 2015 [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 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]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
- [j5]Cezary Kaliszyk, Josef Urban:
Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reason. 53(2): 173-213 (2014) - [c30]Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish:
Beagle as a HOL4 external ATP method. PAAR@IJCAR 2014: 50-59 - [c29]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. PAAR@IJCAR 2014: 60-66 - [c28]Thibault Gauthier, Cezary Kaliszyk:
Matching Concepts across HOL Libraries. CICM 2014: 267-281 - [c27]Cezary Kaliszyk, Florian Rabe:
Towards Knowledge Management for HOL Light. CICM 2014: 357-372 - [c26]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM 2014: 435-439 - [c25]Cezary Kaliszyk, Josef Urban:
Wikis and Collaborative Systems for Large Formal Mathematics. SWCS (LNCS Volume) 2014: 35-52 - [c24]Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. SCSS 2014: 27-34 - [c23]Sebastiaan J. C. 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
- [c22]Cezary Kaliszyk, Thomas Sternagel:
Initial Experiments on Deriving a Complete HOL Simplification Set. PxTP@CADE 2013: 77-86 - [c21]Cezary Kaliszyk, Josef Urban:
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE 2013: 87-95 - [c20]Cezary Kaliszyk, Josef Urban:
PRocH: Proof Reconstruction for HOL Light. CADE 2013: 267-274 - [c19]Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban:
MaSh: Machine Learning for Sledgehammer. ITP 2013: 35-50 - [c18]Cezary Kaliszyk, Alexander Krauss:
Scalable LCF-Style Proof Translation. ITP 2013: 51-66 - [c17]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456 - [c16]Cezary Kaliszyk, Josef Urban:
Lemma Mining over HOL Light. LPAR 2013: 503-517 - [c15]Cezary Kaliszyk, Josef Urban:
Automated Reasoning Service for HOL Light. MKM/Calculemus/DML 2013: 120-135 - [c14]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]Cezary Kaliszyk, Josef Urban:
Lemma Mining over HOL Light. CoRR abs/1310.2797 (2013) - [i3]Cezary Kaliszyk, Josef Urban:
MizAR 40 for Mizar 40. CoRR abs/1310.2805 (2013) - 2012
- [j4]Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. Log. Methods Comput. Sci. 8(2) (2012) - [c13]Fadoua Ghourabi, Asem Kasem, Cezary Kaliszyk:
Algebraic Analysis of Huzita's Origami Operations and Their Extensions. Automated Deduction in Geometry 2012: 143-160 - [c12]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
- [c11]Cezary Kaliszyk, Henk Barendregt:
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. CPP 2011: 87-102 - [c10]Christian Urban, Cezary Kaliszyk:
General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP 2011: 480-500 - [c9]Cezary Kaliszyk, Tetsuo Ida:
Proof Assistant Decision Procedures for Formalizing Origami. Calculemus/MKM 2011: 45-57 - [c8]Cezary Kaliszyk, Christian Urban:
Quotients revisited for Isabelle/HOL. SAC 2011: 1639-1644 - 2010
- [j3]Florian Haftmann, Cezary Kaliszyk, Walther Neuper:
CTP-based programming languages?: considerations about an experimental design. ACM Commun. Comput. Algebra 44(1/2): 27-41 (2010) - [j2]Cezary Kaliszyk:
Counting Derangements, Non Bijective Functions and the Birthday Problem. Formaliz. Math. 18(1-4): 197-200 (2010)
2000 – 2009
- 2009
- [j1]Cezary Kaliszyk, Russell O'Connor:
Computing with Classical Real Numbers. J. Formaliz. Reason. 2(1): 27-39 (2009) - 2008
- [c7]Cezary Kaliszyk:
Automating Side Conditions in Formalized Partial Functions. AISC/MKM/Calculemus 2008: 300-314 - [c6]Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers:
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki 2008 - [c5]Cezary Kaliszyk, Freek Wiedijk:
Merging Procedural and Declarative Proof. TYPES 2008: 203-219 - [i1]Cezary Kaliszyk, Russell O'Connor:
Computing with Classical Real Numbers. CoRR abs/0809.1644 (2008) - 2007
- [c4]Cezary Kaliszyk, Freek Wiedijk:
Certified Computer Algebra on Top of an Interactive Theorem Prover. Calculemus/MKM 2007: 94-105 - [c3]Pierre Corbineau, Cezary Kaliszyk:
Cooperative Repositories for Formal Proofs. Calculemus/MKM 2007: 221-234 - 2006
- [c2]Cezary Kaliszyk:
Web Interfaces for Proof Assistants. UITP@FLoC 2006: 49-61 - 2004
- [c1]Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, Mateusz Srebrny:
SIE - Intelligent Web Proxy Framework. ICWE 2004: 373-385
Coauthor Index
[c98] [i44] [c92] [c91] [i42] [c87] [c84] [i39] [j23] [j22] [c78] [c77] [i34] [c76] [c75] [c72] [i30] [i29] [i28] [i27] [i26] [j14] [c63] [c62] [i25] [i24] [i23] [i22] [i21] [c61] [c58] [c56] [c52] [j11] [j10] [c49] [c47] [i17] [i16] [j9] [j8] [j7] [j6] [c43] [c41] [c39] [c37] [c36] [c35] [c34] [c32] [i15] [j5] [c29] [c26] [c25] [c24] [c23] [i12] [i11] [i10] [i8] [i7] [c21] [c20] [c19] [c17] [c16] [c15] [c14] [i6] [i5] [i4] [i3] [c12] [i2]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-06 20:30 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
