On the independence of axioms in BL and MTL. - Karel Chvalovský (Fuzzy Sets Syst., 2012)

Note on Deduction Theorems in contraction-free logics. - Karel Chvalovský; Petr Cintula (Math. Log. Q., 2012)

Undecidability of Consequence Relation in Full non-Associative Lambek Calculus. - Karel Chvalovský (J. Symb. Log., 2015)

Full Lambek Calculus with Contraction is Undecidable. - Karel Chvalovský; Rostislav Horcík (J. Symb. Log., 2016)

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. - Karel Chvalovský; Jan Jakubuv; Martin Suda 001; Josef Urban (CADE, 2019)

Top-Down Neural Model For Formulae. - Karel Chvalovský (ICLR (Poster), 2019)

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). - Jan Jakubuv; Karel Chvalovský; Miroslav Olsák; Bartosz Piotrowski; Martin Suda 001; Josef Urban (IJCAR (2), 2020)

Fast and Slow Enigmas and Parental Guidance. - Zarathustra Amadeus Goertzel; Karel Chvalovský; Jan Jakubuv; Miroslav Olsák; Josef Urban (FroCoS, 2021)

Learning Theorem Proving Components. - Karel Chvalovský; Jan Jakubuv; Miroslav Olsák; Josef Urban (TABLEAUX, 2021)

MizAR 60 for Mizar 50. - Jan Jakubuv; Karel Chvalovský; Zarathustra Amadeus Goertzel; Cezary Kaliszyk; Mirek Olsák; Bartosz Piotrowski; Stephan Schulz 001; Martin Suda 001; Josef Urban (ITP, 2023)

Guiding an Instantiation Prover with Graph Neural Networks. - Karel Chvalovský; Konstantin Korovin; Jelle Piepenbrock; Josef Urban (LPAR, 2023)

Towards Learning Infinite SMT Models (Work in Progress). - Mikolás Janota; Bartosz Piotrowski; Karel Chvalovský (SYNASC, 2023)

Regularization in Spider-Style Strategy Discovery and Schedule Construction. - Filip Bártek; Karel Chvalovský; Martin Suda 001 (IJCAR (1), 2024)

Cautious Specialization of Strategy Schedules (Extended Abstract). - Filip Bártek; Karel Chvalovský; Martin Suda 001 (PAAR+SC²@IJCAR, 2024)

SMT and Functional Equation Solving over the Reals: Challenges from the IMO. - Chad E. Brown; Karel Chvalovský; Mikolás Janota; Mirek Olsák; Stefan Ratschan (CADE, 2025)