Home Summary Team Publications

Publications

2022

Learning Higher-Order Programs without Meta-Interpretive Learning
Stanisław Purgał and David Cerna and Cezary Kaliszyk
Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022
BibTeX Publisher arXiv preprint
Lash 1.0 (System Description)
Chad E. Brown and Cezary Kaliszyk
Automated Reasoning - 11th International Joint Conference, IJCAR 2022
BibTeX Publisher arXiv preprint
Adversarial Learning to Reason in an Arbitrary Logic
Stanisław Purgał and Cezary Kaliszyk
Proceedings of the Thirty-Fifth International Florida Artificial Intelligence Research Society Conference, FLAIRS 2022
BibTeX Publisher arXiv preprint
Formalizing a diophantine description of the set of primes (short paper)
Karol Pąk and Cezary Kaliszyk
13th International Conference on Interactive Theorem Proving, ITP 2022
BibTeX Publisher arXiv preprint
The Isabelle Enigma
Zar Goerzel and Jan Jakubuv and Cezary Kaliszyk and Mirek Olsak and Jelle Piepenbroek and Josef Urban
13th International Conference on Interactive Theorem Proving, ITP 2022
BibTeX Publisher preprint
Lazy Paramodulation in Practice
Grzegorz Prusak and Cezary Kaliszyk
Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022
BibTeX Publisher arXiv preprint
Proofgold: Blockchain for Formal Methods
Chad E. Brown and Cezary Kaliszyk and Thibault Gauthier and Josef Urban
4th International Workshop on Formal Methods for Blockchains, FMBC 2022
BibTeX Publisher preprint
Separability and randomness in free groups
Michal Buran
J. Algebra, 2022
BibTeX Publisher arXiv preprint

2021

Disambiguating Symbolic Expressions in Informal Documents
Dennis Müller and Cezary Kaliszyk
9th International Conference on Learning Representations, ICLR 2021
BibTeX Publisher arXiv preprint
JEFL: Joint Embedding of Formal Proof Libraries
Qingxiang Wang and Cezary Kaliszyk
Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint
Homotopy Type Theory in Isabelle
Joshua Chen
12th International Conference on Interactive Theorem Proving, ITP 2021
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint
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)
BibTeX Publisher preprint
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
BibTeX Publisher arXiv preprint
A study of continuous vector representations for theorem proving
Stanisław Purgał and Julian Parsert and Cezary Kaliszyk
Journal of Logic and Computation, 2021
BibTeX Publisher arXiv preprint
TacticToe: Learning to Prove with Tactics
Thibault Gauthier and Cezary Kaliszyk and Josef Urban and Ramana Kumar and Michael Norrish
J. Autom. Reason., 2021
BibTeX Publisher arXiv preprint
Machine Learning Guidance for Connection Tableaux
Michael Färber and Cezary Kaliszyk and Josef Urban
J. Autom. Reason., 2021
BibTeX Publisher arXiv preprint
Faster Smarter Proof by Induction in Isabelle/HOL
Yutaka Nagashima
International Joint Conference on Artificial Intelligence, IJCAI 2021
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint

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
BibTeX Publisher arXiv preprint
Property Invariant Embedding for Automated Reasoning
Miroslav Olsák and Cezary Kaliszyk and Josef Urban
24th European Conference on Artificial Intelligence, ECAI 2020
BibTeX Publisher arXiv preprint
Relaxed Weighted Path Order in Theorem Proving
Jan Jakubuv and Cezary Kaliszyk
Math. Comput. Sci., 2020
BibTeX Publisher preprint
GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry
Miroslav Olsák
7th International Conference on Mathematical Software - ICMS 2020
BibTeX Publisher arXiv preprint
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq
Burak Ekici and Cezary Kaliszyk
Math. Comput. Sci., 2020
BibTeX Publisher preprint
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
BibTeX Publisher arXiv preprint
A Survey of Languages for Formalizing Mathematics
Cezary Kaliszyk and Florian Rabe
Intelligent Computer Mathematics (CICM 2020)
BibTeX Publisher arXiv preprint
Property Preserving Embedding of First-order Logic
Julian Parsert and Stephanie Autherith and Cezary Kaliszyk
6th Global Conference on Artificial Intelligence (GCAI 2020)
BibTeX Publisher preprint
Improving Expressivity of Graph Neural Networks
Stanislaw Purgal
2020 International Joint Conference on Neural Networks, IJCNN 2020
BibTeX Publisher preprint

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)
BibTeX Publisher preprint
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)
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint
Linear Programming
Julian Parsert and Cezary Kaliszyk
Arch. Formal Proofs, 2019
BibTeX Publisher preprint
Aligning Concepts across Proof Assistant Libraries
Thibault Gauthier and Cezary Kaliszyk
J. Symbolic Computation, 2019
BibTeX Publisher preprint
Declarative Proof Translation (short paper)
Cezary Kaliszyk and Karol Pąk
10th International Conference on Interactive Theorem Proving (ITP 2019)
BibTeX Publisher preprint
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)
BibTeX Publisher preprint
Semantics of Mizar as an Isabelle Object Logic
Cezary Kaliszyk and Karol Pąk
J. Autom. Reasoning, 2019
BibTeX Publisher preprint
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
BibTeX Publisher preprint

2018

Hammer for Coq: Automation for Dependent Type Theory
Łukasz Czajka and Cezary Kaliszyk
J. Autom. Reasoning, 2018
BibTeX Publisher preprint
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
BibTeX Publisher arXiv preprint
CoqHammer: Strong Automation for Program Verification
Łukasz Czajka and Cezary Kaliszyk
Fourth International Workshop on Coq for Programming Languages, CoqPL 2018
BibTeX Publisher preprint
Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq
Burak Ekici
FMM 2018 - Third workshop on Formal Mathematics for Mathematicians
BibTeX Publisher preprint
IMP with exceptions over decorated logic
Burak Ekici
Discret. Math. Theor. Comput. Sci., 2018
BibTeX Publisher arXiv preprint
Goal-Oriented Conjecturing for Isabelle/HOL
Yutaka Nagashima and Julian Parsert
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
BibTeX Publisher arXiv preprint
Von-Neumann-Morgenstern Utility Theorem
Julian Parsert and Cezary Kaliszyk
Arch. Formal Proofs, 2018
BibTeX Publisher preprint
Towards a Unified Ordering for Superposition-Based Automated Reasoning
Jan Jakubuv and Cezary Kaliszyk
6th International Conference on Mathematical Software (ICMS 2018)
BibTeX Publisher preprint
Concrete Semantics with Coq and CoqHammer
Łukasz Czajka and Burak Ekici and Cezary Kaliszyk
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
BibTeX Publisher arXiv preprint
Isabelle Import Infrastructure for the Mizar Mathematical Library
Cezary Kaliszyk and Karol Pąk
11th International Conference on Intelligent Computer Mathematics (CICM 2018)
BibTeX Publisher preprint
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)
BibTeX Publisher arXiv preprint
Towards Formal Foundations for Game Theory
Julian Parsert and Cezary Kaliszyk
Interactive Theorem Proving - 9th International Conference, ITP 2018
BibTeX Publisher preprint
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)
BibTeX Publisher preprint

2017

Monte Carlo Tableau Proof Search
Michael Färber and Cezary Kaliszyk and Josef Urban
26th International Conference on Automated Deduction (CADE 2017)
BibTeX Publisher arXiv preprint
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)
BibTeX Publisher preprint
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
BibTeX preprint
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)
BibTeX Publisher preprint
Microeconomics and the First Welfare Theorem
Julian Parsert and Cezary Kaliszyk
Arch. Formal Proofs, 2017
BibTeX Publisher preprint
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
BibTeX Publisher arXiv preprint
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
BibTeX Publisher arXiv preprint
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
BibTeX Publisher preprint
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
BibTeX Publisher preprint
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
BibTeX Publisher preprint
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
BibTeX Publisher arXiv preprint