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 - [i48]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) - [i47]Karol Pak, Cezary Kaliszyk:
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. CoRR abs/2410.00065 (2024) - [i46]Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk:
Experiments with Choice in Dependently-Typed Higher-Order Logic. CoRR abs/2410.08874 (2024) - [i45]Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk:
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version). CoRR abs/2410.14232 (2024) - [i44]Liao Zhang, David M. Cerna, Cezary Kaliszyk:
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction. CoRR abs/2411.01188 (2024) - [i43]Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk:
Automated Strategy Invention for Confluence of Term Rewrite Systems. CoRR abs/2411.06409 (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