Cezary Kaliszyk

ORCID

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 97

Top Venues

Publications

Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic. IJCAR (1) (2024)
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
Experiments with Choice in Dependently-Typed Higher-Order Logic. LPAR (2024)
Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery. LPAR (2024)
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)
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
Learning Guided Automated Reasoning: A Brief Survey. CoRR (2024)
Cezary Kaliszyk
Improved Assistance for Interactive Proof (Keynote). CPP (2023)
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 (2023)
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)
Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
Experiments on Infinite Model Finding in SMT Solving. LPAR (2023)
Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
Learning Proof Transformations and Its Applications in Interactive Theorem Proving. FroCoS (2023)
Jan Jakubuv, Cezary Kaliszyk
VizAR: Visualization of Automated Reasoning Proofs (System Description). CICM (2023)
Cezary Kaliszyk, Karol Pak
Combining Higher-Order Logic with Set Theory Formalizations. J. Autom. Reason. 67 (2) (2023)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
The Isabelle ENIGMA. ITP (2022)
Grzegorz Prusak, Cezary Kaliszyk
Lazy Paramodulation in Practice. PAAR@IJCAR (2022)
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
Learning Higher-Order Logic Programs From Failures. IJCAI (2022)
Karol Pak, Cezary Kaliszyk
Formalizing a Diophantine Representation of the Set of Prime Numbers. ITP (2022)
Stanislaw J. Purgal, Cezary Kaliszyk
Adversarial Learning to Reason in an Arbitrary Logic. FLAIRS (2022)
Chad E. Brown, Mikolás Janota, Cezary Kaliszyk
Abstract: Challenges and Solutions for Higher-Order SMT Proofs. SMT (2022)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
The Isabelle ENIGMA. CoRR (2022)
Chad E. Brown, Cezary Kaliszyk
Lash 1.0 (System Description). CoRR (2022)
Chad E. Brown, Cezary Kaliszyk
Lash 1.0 (System Description). IJCAR (2022)
Karol Pak, Cezary Kaliszyk
Formalizing a Diophantine Representation of the Set of Prime Numbers. CoRR (2022)
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
Differentiable Inductive Logic Programming in High-Dimensional Space. CoRR (2022)
Stanislaw J. Purgal, Cezary Kaliszyk
Adversarial Learning to Reason in an Arbitrary Logic. CoRR (2022)
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
Proofgold: Blockchain for Formal Methods. FMBC@CAV (2022)
Qingxiang Wang, Cezary Kaliszyk
JEFL: Joint Embedding of Formal Proof Libraries. CoRR (2021)
Michael Färber, Cezary Kaliszyk, Josef Urban
Machine Learning Guidance for Connection Tableaux. J. Autom. Reason. 65 (2) (2021)
Dennis Müller, Cezary Kaliszyk
Disambiguating Symbolic Expressions in Informal Documents. ICLR (2021)
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
Learning Higher-Order Programs without Meta-Interpretive Learning. CoRR (2021)
Qingxiang Wang, Cezary Kaliszyk
JEFL: Joint Embedding of Formal Proof Libraries. FroCoS (2021)
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Online Machine Learning Techniques for Coq: A Comparison. CoRR (2021)
Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk
A Study of Continuous Vector Representationsfor Theorem Proving. CoRR (2021)
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Online Machine Learning Techniques for Coq: A Comparison. CICM (2021)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65 (2) (2021)
Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk
A study of continuous vector representations for theorem proving. J. Log. Comput. 31 (8) (2021)
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
Towards Finding Longer Proofs. TABLEAUX (2021)
Dennis Müller, Cezary Kaliszyk
Disambiguating Symbolic Expressions in Informal Documents. CoRR (2021)
Cezary Kaliszyk, Florian Rabe
A Survey of Languages for Formalizing Mathematics. CICM (2020)
Jan Jakubuv, Cezary Kaliszyk
Relaxed Weighted Path Order in Theorem Proving. Math. Comput. Sci. 14 (3) (2020)
Burak Ekici, Cezary Kaliszyk
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq. Math. Comput. Sci. 14 (3) (2020)
Cezary Kaliszyk, Florian Rabe
A Survey of Languages for Formalizing Mathematics. CoRR (2020)
Julian Parsert, Stephanie Autherith, Cezary Kaliszyk
Property Preserving Embedding of First-order Logic. GCAI (2020)
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP (2020)
Miroslav Olsák, Cezary Kaliszyk, Josef Urban
Property Invariant Embedding for Automated Reasoning. ECAI (2020)
Thibault Gauthier, Cezary Kaliszyk
Aligning concepts across proof assistant libraries. J. Symb. Comput. 90 (2019)
Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
Can Neural Networks Learn Symbolic Rewriting? CoRR (2019)
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
Towards Finding Longer Proofs. CoRR (2019)
Julian Parsert, Cezary Kaliszyk
Linear Programming. Arch. Formal Proofs 2019 (2019)
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CoRR (2019)
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
GRUNGE: A Grand Unified ATP Challenge. CoRR (2019)
Cezary Kaliszyk, Karol Pak
Semantics of Mizar as an Isabelle Object Logic. J. Autom. Reason. 63 (3) (2019)
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
GRUNGE: A Grand Unified ATP Challenge. CADE (2019)
Miroslav Olsák, Cezary Kaliszyk, Josef Urban
Property Invariant Embedding for Automated Reasoning. CoRR (2019)
Michael Färber, Cezary Kaliszyk
Certification of Nonclausal Connection Tableaux Proofs. TABLEAUX (2019)
Chad E. Brown, Cezary Kaliszyk, Karol Pak
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ITP (2019)
Cezary Kaliszyk, Karol Pak
Declarative Proof Translation (Short Paper). ITP (2019)
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák
Reinforcement Learning of Theorem Proving. NeurIPS (2018)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
Learning to Prove with Tactics. CoRR (2018)
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR (2018)
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
Concrete Semantics with Coq and CoqHammer. CICM (2018)
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
Concrete Semantics with Coq and CoqHammer. CoRR (2018)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Learning to Reason with HOL4 tactics. CoRR (2018)
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
First Experiments with Neural Translation of Informal to Formal Mathematics. CICM (2018)
Jan Jakubuv, Cezary Kaliszyk
Towards a Unified Ordering for Superposition-Based Automated Reasoning. ICMS (2018)
Cezary Kaliszyk, Karol Pak
Isabelle Import Infrastructure for the Mizar Mathematical Library. CICM (2018)
Julian Parsert, Cezary Kaliszyk
Von-Neumann-Morgenstern Utility Theorem. Arch. Formal Proofs 2018 (2018)
Cezary Kaliszyk, Julian Parsert
Formal microeconomic foundations and the first welfare theorem. CPP (2018)
Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31 (3) (2018)
Michael Färber, Cezary Kaliszyk, Josef Urban
Machine Learning Guidance and Proof Certification for Connection Tableaux. CoRR (2018)
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
Reinforcement Learning of Theorem Proving. CoRR (2018)
Julian Parsert, Cezary Kaliszyk
Towards Formal Foundations for Game Theory. ITP (2018)
Lukasz Czajka, Cezary Kaliszyk
Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason. 61 (1-4) (2018)
Cezary Kaliszyk, François Chollet, Christian Szegedy
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. ICLR (Poster) (2017)
Cezary Kaliszyk, Karol Pak
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions. MACIS (2017)
Michael Färber, Cezary Kaliszyk, Josef Urban
Monte Carlo Tableau Proof Search. CADE (2017)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP (2017)
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk
Deep Network Guided Proof Search. CoRR (2017)
Cezary Kaliszyk, Karol Pak
Progress in the Independent Certification of Mizar Mathematical Library in Isabelle. FedCSIS (2017)
Cezary Kaliszyk, François Chollet, Christian Szegedy
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. CoRR (2017)
Cezary Kaliszyk, Karol Pak
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. CICM (2017)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
TacticToe: Learning to Reason with HOL4 Tactics. LPAR (2017)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
System Description: Statistical Parsing of Informalized Mizar Formulas. SYNASC (2017)
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk
Deep Network Guided Proof Search. LPAR (2017)
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
Classification of Alignments Between Concepts of Formal Mathematical Systems. CICM (2017)
Julian Parsert, Cezary Kaliszyk
Microeconomics and the First Welfare Theorem. Arch. Formal Proofs 2017 (2017)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Initial Experiments with Statistical Conjecturing over Large Formal Corpora. FM4M/MathUI/ThEdu/DP/WIP@CIKM (2016)
Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe
A Standard for Aligning Mathematical Concepts. FM4M/MathUI/ThEdu/DP/WIP@CIKM (2016)
David Aspinall, Cezary Kaliszyk
What's in a Theorem Name? ITP (2016)
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) (2016)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving. CoRR (2016)
David Aspinall, Cezary Kaliszyk
Towards Formal Proof Metrics. FASE (2016)
Michael Färber, Cezary Kaliszyk
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. PAAR@IJCAR (2016)
Michael Färber, Cezary Kaliszyk, Josef Urban
Monte Carlo Connection Prover. CoRR (2016)
Lukasz Czajka, Cezary Kaliszyk
Goal Translation for a Hammer for Coq (Extended Abstract). HaTT@IJCAR (2016)
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
Hammering towards QED. J. Formaliz. Reason. 9 (1) (2016)
Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. PAAR@IJCAR (2016)
Cezary Kaliszyk, Karol Pak, Josef Urban
Towards a mizar environment for isabelle: foundations and language. CPP (2016)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
Learning to Parse on Aligned Corpora (Rough Diamond). ITP (2015)
Cezary Kaliszyk, Josef Urban
MizAR 40 for Mizar 40. J. Autom. Reason. 55 (3) (2015)
Thibault Gauthier, Cezary Kaliszyk
Premise Selection and External Provers for HOL4. CPP (2015)

Cezary Kaliszyk.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Cezary Kaliszyk