Publications

2021

Disambiguating Symbolic Expressions in Informal Documents
Dennis Müller and Cezary Kaliszyk
9th International Conference on Learning Representations, ICLR 2021
JEFL: Joint Embedding of Formal Proof Libraries
Qingxiang Wang and Cezary Kaliszyk
Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021
Fast and Slow Enigmas and Parental Guidance
Zarathustra Amadeus Goertzel and Karel Chvalovský and Jan Jakubův and Miroslav Olšák and Josef Urban
Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021
Learning Theorem Proving Components
Karel Chvalovský and Jan Jakubův and Miroslav Olšák and Josef Urban
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021
Towards Finding Longer Proofs
Zsolt Zombori and Adrián Csiszárik and Henryk Michalewski and Cezary Kaliszyk and Josef Urban
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021
Homotopy Type Theory in Isabelle
Joshua Chen
12th International Conference on Interactive Theorem Proving, ITP 2021
Learning to Solve Geometric Construction Problems from Images
Jaroslav Macke and Jirí Sedlár and Miroslav Olsák and Josef Urban and Josef Sivic
Intelligent Computer Mathematics - 14th International Conference, CICM 2021
Characteristic Subsets of SMT-LIB Benchmarks
Jan Jakubuv and Mikolás Janota and Andrew Reynolds
Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification (CAV 2021)
Online Machine Learning Techniques for Coq: A Comparison
Liao Zhang and Lasse Blaauwbroek and Bartosz Piotrowski and Prokop Cerný and Cezary Kaliszyk and Josef Urban
Intelligent Computer Mathematics - 14th International Conference, CICM 2021
A study of continuous vector representations for theorem proving
Stanisław Purgał and Julian Parsert and Cezary Kaliszyk
Journal of Logic and Computation, 2021
TacticToe: Learning to Prove with Tactics
Thibault Gauthier and Cezary Kaliszyk and Josef Urban and Ramana Kumar and Michael Norrish
J. Autom. Reason., 2021
Machine Learning Guidance for Connection Tableaux
Michael Färber and Cezary Kaliszyk and Josef Urban
J. Autom. Reason., 2021
Faster Smarter Proof by Induction in Isabelle/HOL
Yutaka Nagashima
International Joint Conference on Artificial Intelligence, IJCAI 2021
The Role of Entropy in Guiding a Connection Prover
Zsolt Zombori and Josef Urban and Miroslav Olsák
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021

2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Jan Jakubuv and Karel Chvalovský and Miroslav Olsák and Bartosz Piotrowski and Martin Suda and Josef Urban
Automated Reasoning - 10th International Joint Conference, IJCAR 2020
Property Invariant Embedding for Automated Reasoning
Miroslav Olsák and Cezary Kaliszyk and Josef Urban
24th European Conference on Artificial Intelligence, ECAI 2020
Relaxed Weighted Path Order in Theorem Proving
Jan Jakubuv and Cezary Kaliszyk
Math. Comput. Sci., 2020
GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry
Miroslav Olsák
7th International Conference on Mathematical Software - ICMS 2020
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq
Burak Ekici and Cezary Kaliszyk
Math. Comput. Sci., 2020
Exploration of neural machine translation in autoformalization of mathematics in Mizar
Qingxiang Wang and Chad E. Brown and Cezary Kaliszyk and Josef Urban
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020
A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk and Florian Rabe
Intelligent Computer Mathematics (CICM 2020)
Property Preserving Embedding of First-order Logic
Julian Parsert and Stephanie Autherith and Cezary Kaliszyk
6th Global Conference on Artificial Intelligence (GCAI 2020)

2019

Certification of Nonclausal Connection Tableaux Proofs
Michael Färber and Cezary Kaliszyk
28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2019)
GRUNGE: A Grand Unified ATP Challenge
Chad Brown and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban
The 27th International Conference on Automated Deduction (CADE 2019)
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici and Arjun Viswanathan and Yoni Zohar and Clark W. Barrett and Cesare Tinelli
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019
Linear Programming
Julian Parsert and Cezary Kaliszyk
Arch. Formal Proofs, 2019
Aligning Concepts across Proof Assistant Libraries
Thibault Gauthier and Cezary Kaliszyk
J. Symbolic Computation, 2019
Declarative Proof Translation (short paper)
Cezary Kaliszyk and Karol Pąk
10th International Conference on Interactive Theorem Proving (ITP 2019)
Higher-order Tarski Grothendieck as a Foundation for Formal Proof
Chad Brown and Cezary Kaliszyk and Karol Pąk
10th International Conference on Interactive Theorem Proving (ITP 2019)
Semantics of Mizar as an Isabelle Object Logic
Cezary Kaliszyk and Karol Pąk
J. Autom. Reasoning, 2019
Can Neural Networks Learn Symbolic Rewriting?
Bartosz Piotrowski and Josef Urban and Chad Brown and Cezary Kaliszyk
Learning and Reasoning with Graph-Structured Representations -- ICML 2019 Workshop

2018

Hammer for Coq: Automation for Dependent Type Theory
Łukasz Czajka and Cezary Kaliszyk
J. Autom. Reasoning, 2018
Reinforcement Learning of Theorem Proving
Kaliszyk, Cezary and Urban, Josef and Michalewski, Henryk and Olšák, Miroslav
Advances in Neural Information Processing Systems 31, 2018
CoqHammer: Strong Automation for Program Verification
Łukasz Czajka and Cezary Kaliszyk
Fourth International Workshop on Coq for Programming Languages, CoqPL 2018
Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq
Burak Ekici
FMM 2018 - Third workshop on Formal Mathematics for Mathematicians
IMP with exceptions over decorated logic
Burak Ekici
Discret. Math. Theor. Comput. Sci., 2018
Goal-Oriented Conjecturing for Isabelle/HOL
Yutaka Nagashima and Julian Parsert
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
Von-Neumann-Morgenstern Utility Theorem
Julian Parsert and Cezary Kaliszyk
Arch. Formal Proofs, 2018
Towards a Unified Ordering for Superposition-Based Automated Reasoning
Jan Jakubuv and Cezary Kaliszyk
6th International Conference on Mathematical Software (ICMS 2018)
Concrete Semantics with Coq and CoqHammer
Łukasz Czajka and Burak Ekici and Cezary Kaliszyk
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
Isabelle Import Infrastructure for the Mizar Mathematical Library
Cezary Kaliszyk and Karol Pąk
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
First Experiments with Neural Translation of Informal to Formal Mathematics
Qingxiang Wang and Cezary Kaliszyk and Josef Urban
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
Towards Formal Foundations for Game Theory
Julian Parsert and Cezary Kaliszyk
Interactive Theorem Proving - 9th International Conference, ITP 2018
Formal Microeconomic Foundations and the First Welfare Theorem
Julian Parsert and Cezary Kaliszyk
Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018)

2017

Monte Carlo Tableau Proof Search
Michael Färber and Cezary Kaliszyk and Josef Urban
26th International Conference on Automated Deduction (CADE 2017)
Isabelle Formalization of Set Theoretic Structures and Set Comprehensions
Cezary Kaliszyk and Karol Pak
International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS 2017)
System Description: Statistical Parsing of Informalized Mizar Formulas
Cezary Kaliszyk and Josef Urban and Jiří Vyskočil
19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017
Automating Formalization by Statistical and Semantic Parsing of Mathematics
Cezary Kaliszyk and Josef Urban and Jiří Vyskočil
8th International Conference on Interactive Theorem Proving (ITP 2017)
Microeconomics and the First Welfare Theorem
Julian Parsert and Cezary Kaliszyk
Arch. Formal Proofs, 2017
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Cezary Kaliszyk and François Chollet and Christian Szegedy
5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings
Deep Network Guided Proof Search
Sarah Loos and Geoffrey Irving and Christian Szegedy and Cezary Kaliszyk
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017
Progress in the Independent Certification of Mizar Mathematical Library in Isabelle
Cezary Kaliszyk and Karol Pąk
Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017
Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic
Cezary Kaliszyk and Karol Pak
10th International Conference on Intelligent Computer Mathematics (CICM'17), 2017
Classification of Alignments Between Concepts of Formal Mathematical Systems
Dennis Müller and Thibault Gauthier and Cezary Kaliszyk and Michael Kohlhase and Florian Rabe
10th International Conference on Intelligent Computer Mathematics (CICM'17), 2017
TacticToe: Learning to Reason with HOL4 Tactics
Thibault Gauthier and Cezary Kaliszyk and Josef Urban
LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017