Cezary Kaliszyk

191 papers A* 5A 7B 34C 17Misc 3Journal 77Unranked 42
YearRankTypeTitle / Venue / Authors
2026 J jnl
Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents.
CoRR
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 A* conf
Automated Strategy Invention for Confluence of Term Rewrite Systems.
IJCAI
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk
2025 C conf
Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
CICM
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 J jnl
Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
CoRR
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 C conf
Hammering Higher Order Set Theory.
CICM
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025 J jnl
Hammering Higher Order Set Theory.
CoRR
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025 — conf
Payment Channels with Proofs.
BCCA
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 J jnl
Payment Channels with Proofs.
CoRR
Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025 — conf
The Dependently Typed Higher-Order Form for the TPTP World.
FroCoS
Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe
2025 J jnl
The Dependently Typed Higher-Order Form for the TPTP World.
CoRR
Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe
2024 J jnl
Automated Strategy Invention for Confluence of Term Rewrite Systems.
CoRR
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk
2024 B conf
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers.
ITP
Karol Pak, Cezary Kaliszyk
2024 J jnl
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers.
CoRR
Karol Pak, Cezary Kaliszyk
2024 — conf
Differentiable Inductive Logic Programming in High-Dimensional Space.
IJCLR
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
2024 B conf
Experiments with Choice in Dependently-Typed Higher-Order Logic.
LPAR
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
2024 J jnl
Experiments with Choice in Dependently-Typed Higher-Order Logic.
CoRR
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
2024 — conf
Learning Guided Automated Reasoning: A Brief Survey.
Logics and Type Systems in Theory and Practice
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
2024 J jnl
Learning Guided Automated Reasoning: A Brief Survey.
CoRR
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
2024 — conf
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction.
IJCLR
Liao Zhang, David M. Cerna, Cezary Kaliszyk
2024 J jnl
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction.
CoRR
Liao Zhang, David M. Cerna, Cezary Kaliszyk
2024 B conf
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery.
LPAR
Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk
2024 J jnl
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version).
CoRR
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
2024 — conf
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic.
IJCAR (1)
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
2023 J jnl
Combining Higher-Order Logic with Set Theory Formalizations.
J. Autom. Reason.
Cezary Kaliszyk, Karol Pak
2023 B conf
Experiments on Infinite Model Finding in SMT Solving.
LPAR
Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
2023 B conf
Improved Assistance for Interactive Proof (Keynote).
CPP
Cezary Kaliszyk
2023 — conf
Learning Proof Transformations and Its Applications in Interactive Theorem Proving.
FroCoS
Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
2023 B conf
MizAR 60 for Mizar 50.
ITP
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2023 J jnl
MizAR 60 for Mizar 50.
CoRR
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2023 C conf
VizAR: Visualization of Automated Reasoning Proofs (System Description).
CICM
Jan Jakubuv, Cezary Kaliszyk
2022 — conf
Abstract: Challenges and Solutions for Higher-Order SMT Proofs.
SMT
Chad E. Brown, Mikolás Janota, Cezary Kaliszyk
2022 Misc conf
Adversarial Learning to Reason in an Arbitrary Logic.
FLAIRS
Stanislaw J. Purgal, Cezary Kaliszyk
2022 J jnl
Adversarial Learning to Reason in an Arbitrary Logic.
CoRR
Stanislaw J. Purgal, Cezary Kaliszyk
2022 J jnl
Differentiable Inductive Logic Programming in High-Dimensional Space.
CoRR
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
2022 B conf
Formalizing a Diophantine Representation of the Set of Prime Numbers.
ITP
Karol Pak, Cezary Kaliszyk
2022 J jnl
Formalizing a Diophantine Representation of the Set of Prime Numbers.
CoRR
Karol Pak, Cezary Kaliszyk
2022 A conf
Lash 1.0 (System Description).
IJCAR
Chad E. Brown, Cezary Kaliszyk
2022 J jnl
Lash 1.0 (System Description).
CoRR
Chad E. Brown, Cezary Kaliszyk
2022 — conf
Lazy Paramodulation in Practice.
PAAR@IJCAR
Grzegorz Prusak, Cezary Kaliszyk
2022 A* conf
Learning Higher-Order Logic Programs From Failures.
IJCAI
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
2022 — conf
Proofgold: Blockchain for Formal Methods.
FMBC@CAV
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
2022 B conf
The Isabelle ENIGMA.
ITP
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
2022 J jnl
The Isabelle ENIGMA.
CoRR
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
2021 B ed.
12th International Conference on Interactive Theorem Proving, ITP 2021, Rome, Italy (Virtual Conference), June 29 - July 1, 2021
ITP
Liron Cohen, Cezary Kaliszyk
2021 J jnl
A Study of Continuous Vector Representationsfor Theorem Proving.
CoRR
Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk
2021 J jnl
A study of continuous vector representations for theorem proving.
J. Log. Comput.
Stanislaw J. Purgal, Julian Parsert, Cezary Kaliszyk
2021 A* conf
Disambiguating Symbolic Expressions in Informal Documents.
ICLR
Dennis Müller, Cezary Kaliszyk
2021 J jnl
Disambiguating Symbolic Expressions in Informal Documents.
CoRR
Dennis Müller, Cezary Kaliszyk
2021 — conf
JEFL: Joint Embedding of Formal Proof Libraries.
FroCoS
Qingxiang Wang, Cezary Kaliszyk
2021 J jnl
JEFL: Joint Embedding of Formal Proof Libraries.
CoRR
Qingxiang Wang, Cezary Kaliszyk
2021 J jnl
Learning Higher-Order Programs without Meta-Interpretive Learning.
CoRR
Stanislaw J. Purgal, David M. Cerna, Cezary Kaliszyk
2021 J jnl
Machine Learning Guidance for Connection Tableaux.
J. Autom. Reason.
Michael Färber, Cezary Kaliszyk, Josef Urban
2021 C conf
Online Machine Learning Techniques for Coq: A Comparison.
CICM
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
2021 J jnl
Online Machine Learning Techniques for Coq: A Comparison.
CoRR
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
2021 J jnl
TacticToe: Learning to Prove with Tactics.
J. Autom. Reason.
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
2021 B conf
Towards Finding Longer Proofs.
TABLEAUX
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
2020 C conf
A Survey of Languages for Formalizing Mathematics.
CICM
Cezary Kaliszyk, Florian Rabe
2020 J jnl
A Survey of Languages for Formalizing Mathematics.
CoRR
Cezary Kaliszyk, Florian Rabe
2020 B conf
Exploration of neural machine translation in autoformalization of mathematics in Mizar.
CPP
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
2020 — ed.
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.
CICM Workshops
Edwin C. Brady, James H. Davenport, William M. Farmer, Cezary Kaliszyk, Andrea Kohlhase, Michael Kohlhase, Dennis Müller, Karol Pak, Claudio Sacerdoti Coen
2020 J jnl
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq.
Math. Comput. Sci.
Burak Ekici, Cezary Kaliszyk
2020 A conf
Property Invariant Embedding for Automated Reasoning.
ECAI
Miroslav Olsák, Cezary Kaliszyk, Josef Urban
2020 — conf
Property Preserving Embedding of First-order Logic.
GCAI
Julian Parsert, Stephanie Autherith, Cezary Kaliszyk
2020 J jnl
Relaxed Weighted Path Order in Theorem Proving.
Math. Comput. Sci.
Jan Jakubuv, Cezary Kaliszyk
2019 J jnl
Aligning concepts across proof assistant libraries.
J. Symb. Comput.
Thibault Gauthier, Cezary Kaliszyk
2019 J jnl
Can Neural Networks Learn Symbolic Rewriting?
CoRR
Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
2019 B conf
Certification of Nonclausal Connection Tableaux Proofs.
TABLEAUX
Michael Färber, Cezary Kaliszyk
2019 B conf
Declarative Proof Translation (Short Paper).
ITP
Cezary Kaliszyk, Karol Pak
2019 J jnl
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar.
CoRR
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
2019 A conf
GRUNGE: A Grand Unified ATP Challenge.
CADE
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
2019 J jnl
GRUNGE: A Grand Unified ATP Challenge.
CoRR
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
2019 B conf
Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
ITP
Chad E. Brown, Cezary Kaliszyk, Karol Pak
2019 C ed.
Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings
CICM
Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, Claudio Sacerdoti Coen
2019 — ed.
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.
CICM Workshops
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
2019 J jnl
Linear Programming.
Arch. Formal Proofs
Julian Parsert, Cezary Kaliszyk
2019 J jnl
Property Invariant Embedding for Automated Reasoning.
CoRR
Miroslav Olsák, Cezary Kaliszyk, Josef Urban
2019 J jnl
Semantics of Mizar as an Isabelle Object Logic.
J. Autom. Reason.
Cezary Kaliszyk, Karol Pak
2019 J jnl
Towards Finding Longer Proofs.
CoRR
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
2018 C conf
Concrete Semantics with Coq and CoqHammer.
CICM
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
2018 J jnl
Concrete Semantics with Coq and CoqHammer.
CoRR
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
2018 C conf
First Experiments with Neural Translation of Informal to Formal Mathematics.
CICM
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
2018 J jnl
First Experiments with Neural Translation of Informal to Formal Mathematics.
CoRR
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
2018 J jnl
Foreword to the Special Issue on Automated Reasoning.
AI Commun.
Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
2018 B conf
Formal microeconomic foundations and the first welfare theorem.
CPP
Cezary Kaliszyk, Julian Parsert
2018 J jnl
Hammer for Coq: Automation for Dependent Type Theory.
J. Autom. Reason.
Lukasz Czajka, Cezary Kaliszyk
2018 C conf
Isabelle Import Infrastructure for the Mizar Mathematical Library.
CICM
Cezary Kaliszyk, Karol Pak
2018 J jnl
Learning to Prove with Tactics.
CoRR
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
2018 J jnl
Learning to Reason with HOL4 tactics.
CoRR
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
2018 J jnl
Machine Learning Guidance and Proof Certification for Connection Tableaux.
CoRR
Michael Färber, Cezary Kaliszyk, Josef Urban
2018 A* conf
Reinforcement Learning of Theorem Proving.
NeurIPS
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák
2018 J jnl
Reinforcement Learning of Theorem Proving.
CoRR
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
2018 B conf
Towards Formal Foundations for Game Theory.
ITP
Julian Parsert, Cezary Kaliszyk
2018 — conf
Towards a Unified Ordering for Superposition-Based Automated Reasoning.
ICMS
Jan Jakubuv, Cezary Kaliszyk
2018 J jnl
Von-Neumann-Morgenstern Utility Theorem.
Arch. Formal Proofs
Julian Parsert, Cezary Kaliszyk
2017 B conf
Automating Formalization by Statistical and Semantic Parsing of Mathematics.
ITP
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2017 C conf
Classification of Alignments Between Concepts of Formal Mathematical Systems.
CICM
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
2017 B conf
Deep Network Guided Proof Search.
LPAR
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk
2017 J jnl
Deep Network Guided Proof Search.
CoRR
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk
2017 — conf
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving.
ICLR (Poster)
Cezary Kaliszyk, François Chollet, Christian Szegedy
2017 J jnl
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving.
CoRR
Cezary Kaliszyk, François Chollet, Christian Szegedy
2017 — conf
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions.
MACIS
Cezary Kaliszyk, Karol Pak
2017 J jnl
Microeconomics and the First Welfare Theorem.
Arch. Formal Proofs
Julian Parsert, Cezary Kaliszyk
2017 A conf
Monte Carlo Tableau Proof Search.
CADE
Michael Färber, Cezary Kaliszyk, Josef Urban
2017 C conf
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic.
CICM
Cezary Kaliszyk, Karol Pak
2017 C conf
Progress in the Independent Certification of Mizar Mathematical Library in Isabelle.
FedCSIS
Cezary Kaliszyk, Karol Pak
2017 Misc conf
System Description: Statistical Parsing of Informalized Mizar Formulas.
SYNASC
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2017 B conf
TacticToe: Learning to Reason with HOL4 Tactics.
LPAR
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
2016 J jnl
A Learning-Based Fact Selector for Isabelle/HOL.
J. Autom. Reason.
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
2016 — conf
A Standard for Aligning Mathematical Concepts.
FM4M/MathUI/ThEdu/DP/WIP@CIKM
Cezary Kaliszyk, Michael Kohlhase, Dennis Müller, Florian Rabe
2016 — conf
Goal Translation for a Hammer for Coq (Extended Abstract).
HaTT@IJCAR
Lukasz Czajka, Cezary Kaliszyk
2016 J jnl
Hammering towards QED.
J. Formaliz. Reason.
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
2016 — conf
Initial Experiments with Statistical Conjecturing over Large Formal Corpora.
FM4M/MathUI/ThEdu/DP/WIP@CIKM
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
2016 J jnl
Monte Carlo Connection Prover.
CoRR
Michael Färber, Cezary Kaliszyk, Josef Urban
2016 — conf
No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions.
PAAR@IJCAR
Michael Färber, Cezary Kaliszyk
2016 — ed.
Proceedings First International Workshop on Hammers for Type Theories, HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016.
HaTT@IJCAR
Jasmin Christian Blanchette, Cezary Kaliszyk
2016 J jnl
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving.
CoRR
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2016 — conf
TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism.
PAAR@IJCAR
Cezary Kaliszyk, Geoff Sutcliffe, Florian Rabe
2016 B conf
Towards Formal Proof Metrics.
FASE
David Aspinall, Cezary Kaliszyk
2016 B conf
Towards a mizar environment for isabelle: foundations and language.
CPP
Cezary Kaliszyk, Karol Pak, Josef Urban
2016 B conf
What's in a Theorem Name?
ITP
David Aspinall, Cezary Kaliszyk
2015 J jnl
A formal proof of the Kepler conjecture.
CoRR
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
2015 — ed.
CICM 2015 - Informal Work in Progress Proceedings, Washington, DC, USA, July 13-17, 2015
CICM (Work in Progress)
Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
2015 B conf
Certified Connection Tableaux Proofs for HOL Light and TPTP.
CPP
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015 B conf
Efficient Low-Level Connection Tableaux.
TABLEAUX
Cezary Kaliszyk
2015 A* conf
Efficient Semantic Features for Automated Reasoning over Large Theories.
IJCAI
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015 J jnl
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck.
J. Autom. Reason.
Cezary Kaliszyk, Josef Urban
2015 B conf
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover.
LPAR
Cezary Kaliszyk, Josef Urban
2015 C conf
Formalizing Physics: Automation, Presentation and Foundation Issues.
CICM
Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar
2015 J jnl
HOL(y)Hammer: Online ATP Service for HOL Light.
Math. Comput. Sci.
Cezary Kaliszyk, Josef Urban
2015 — conf
Improving Statistical Linguistic Algorithms for Parsing Mathematics.
IWIL@LPAR
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015 C ed.
Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings
CICM
Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
2015 B conf
Learning to Parse on Aligned Corpora (Rough Diamond).
ITP
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015 J jnl
Learning-assisted theorem proving with millions of lemmas.
J. Symb. Comput.
Cezary Kaliszyk, Josef Urban
2015 — conf
Lemmatization for Stronger Reasoning in Large Theories.
FroCos
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015 — conf
Metis-based Paramodulation Tactic for HOL Light.
GCAI
Michael Färber, Cezary Kaliszyk
2015 J jnl
MizAR 40 for Mizar 40.
J. Autom. Reason.
Cezary Kaliszyk, Josef Urban
2015 B conf
Premise Selection and External Provers for HOL4.
CPP
Thibault Gauthier, Cezary Kaliszyk
2015 J jnl
Premise Selection and External Provers for HOL4.
CoRR
Thibault Gauthier, Cezary Kaliszyk
2015 — ed.
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015.
PxTP@CADE
Cezary Kaliszyk, Andrei Paskevich
2015 — conf
Random Forests for Premise Selection.
FroCos
Michael Färber, Cezary Kaliszyk
2015 B conf
Sharing HOL4 and HOL Light Proof Knowledge.
LPAR
Thibault Gauthier, Cezary Kaliszyk
2015 J jnl
Sharing HOL4 and HOL Light proof knowledge.
CoRR
Thibault Gauthier, Cezary Kaliszyk
2015 A conf
System Description: E.T. 0.1.
CADE
Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil
2014 — conf
Beagle as a HOL4 external ATP method.
PAAR@IJCAR
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish
2014 J jnl
Certified Connection Tableaux Proofs for HOL Light and TPTP.
CoRR
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2014 C conf
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description.
CICM
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
2014 J jnl
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description.
CoRR
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
2014 — conf
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems.
ACL2
Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban
2014 J jnl
Learning-Assisted Automated Reasoning with Flyspeck.
J. Autom. Reason.
Cezary Kaliszyk, Josef Urban
2014 J jnl
Learning-assisted Theorem Proving with Millions of Lemmas.
CoRR
Cezary Kaliszyk, Josef Urban
2014 — conf
Machine Learner for Automated Reasoning 0.4 and 0.5.
PAAR@IJCAR
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2014 J jnl
Machine Learner for Automated Reasoning 0.4 and 0.5.
CoRR
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2014 — conf
Machine Learning of Coq Proof Guidance: First Experiments.
SCSS
Cezary Kaliszyk, Lionel Mamane, Josef Urban
2014 J jnl
Machine Learning of Coq Proof Guidance: First Experiments.
CoRR
Cezary Kaliszyk, Lionel Mamane, Josef Urban
2014 C conf
Matching Concepts across HOL Libraries.
CICM
Thibault Gauthier, Cezary Kaliszyk
2014 J jnl
Matching concepts across HOL libraries.
CoRR
Thibault Gauthier, Cezary Kaliszyk
2014 C conf
Towards Knowledge Management for HOL Light.
CICM
Cezary Kaliszyk, Florian Rabe
2014 — conf
Wikis and Collaborative Systems for Large Formal Mathematics.
SWCS (LNCS Volume)
Cezary Kaliszyk, Josef Urban
2013 — conf
Automated Reasoning Service for HOL Light.
MKM/Calculemus/DML
Cezary Kaliszyk, Josef Urban
2013 B conf
Communicating Formal Proofs: The Case of Flyspeck.
ITP
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013 J jnl
Formal Mathematics on Display: A Wiki for Flyspeck
CoRR
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013 — conf
Formal Mathematics on Display: A Wiki for Flyspeck.
MKM/Calculemus/DML
Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013 J jnl
HOL(y)Hammer: Online ATP Service for HOL Light.
CoRR
Cezary Kaliszyk, Josef Urban
2013 — conf
Initial Experiments on Deriving a Complete HOL Simplification Set.
PxTP@CADE
Cezary Kaliszyk, Thomas Sternagel
2013 B conf
Lemma Mining over HOL Light.
LPAR
Cezary Kaliszyk, Josef Urban
2013 J jnl
Lemma Mining over HOL Light.
CoRR
Cezary Kaliszyk, Josef Urban
2013 B conf
MaSh: Machine Learning for Sledgehammer.
ITP
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban
2013 J jnl
MizAR 40 for Mizar 40.
CoRR
Cezary Kaliszyk, Josef Urban
2013 A conf
PRocH: Proof Reconstruction for HOL Light.
CADE
Cezary Kaliszyk, Josef Urban
2013 — ed.
Proceedings 10th International Workshop On User Interfaces for Theorem Provers, UITP 2012, Bremen, Germany, July 11th, 2012.
UITP
Cezary Kaliszyk, Christoph Lüth
2013 B conf
Scalable LCF-Style Proof Translation.
ITP
Cezary Kaliszyk, Alexander Krauss
2013 — conf
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution.
PxTP@CADE
Cezary Kaliszyk, Josef Urban
2012 — conf
Algebraic Analysis of Huzita's Origami Operations and Their Extensions.
Automated Deduction in Geometry
Fadoua Ghourabi, Asem Kasem, Cezary Kaliszyk
2012 J jnl
General Bindings and Alpha-Equivalence in Nominal Isabelle
Log. Methods Comput. Sci.
Christian Urban, Cezary Kaliszyk
2012 — conf
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora.
PAAR@IJCAR
Cezary Kaliszyk, Josef Urban
2012 J jnl
Learning-assisted Automated Reasoning with Flyspeck
CoRR
Cezary Kaliszyk, Josef Urban
2011 A conf
General Bindings and Alpha-Equivalence in Nominal Isabelle.
ESOP
Christian Urban, Cezary Kaliszyk
2011 — conf
Proof Assistant Decision Procedures for Formalizing Origami.
Calculemus/MKM
Cezary Kaliszyk, Tetsuo Ida
2011 Misc conf
Quotients revisited for Isabelle/HOL.
SAC
Cezary Kaliszyk, Christian Urban
2011 B conf
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem.
CPP
Cezary Kaliszyk, Henk Barendregt
2010 J jnl
CTP-based programming languages?: considerations about an experimental design.
ACM Commun. Comput. Algebra
Florian Haftmann, Cezary Kaliszyk, Walther Neuper
2010 J jnl
Counting Derangements, Non Bijective Functions and the Birthday Problem.
Formaliz. Math.
Cezary Kaliszyk
2009 J jnl
Computing with Classical Real Numbers.
J. Formaliz. Reason.
Cezary Kaliszyk, Russell O'Connor
2008 — conf
A Real Semantic Web for Mathematics Deserves a Real Semantics.
SemWiki
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
2008 — conf
Automating Side Conditions in Formalized Partial Functions.
AISC/MKM/Calculemus
Cezary Kaliszyk
2008 J jnl
Computing with Classical Real Numbers
CoRR
Cezary Kaliszyk, Russell O'Connor
2008 — conf
Merging Procedural and Declarative Proof.
TYPES
Cezary Kaliszyk, Freek Wiedijk
2007 — conf
Certified Computer Algebra on Top of an Interactive Theorem Prover.
Calculemus/MKM
Cezary Kaliszyk, Freek Wiedijk
2007 — conf
Cooperative Repositories for Formal Proofs.
Calculemus/MKM
Pierre Corbineau, Cezary Kaliszyk
2006 — conf
Web Interfaces for Proof Assistants.
UITP@FLoC
Cezary Kaliszyk
2004 B conf
SIE - Intelligent Web Proxy Framework.
ICWE
Grzegorz Andruszkiewicz, Krzysztof Ciebiera, Marcin Gozdalik, Cezary Kaliszyk, Mateusz Srebrny