Karel Chvalovský

24 papers A 2B 3Misc 1Journal 12Unranked 6
YearRankTypeTitle / Venue / Authors
2025 A conf
SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
CADE
Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
2025 J jnl
SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
CoRR
Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
2025 J jnl
Towards Learning Infinite SMT Models (Work in Progress).
CoRR
Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
2024 — conf
Cautious Specialization of Strategy Schedules (Extended Abstract).
PAAR+SC²@IJCAR
Filip Bártek, Karel Chvalovský, Martin Suda
2024 — conf
Regularization in Spider-Style Strategy Discovery and Schedule Construction.
IJCAR (1)
Filip Bártek, Karel Chvalovský, Martin Suda
2024 J jnl
Regularization in Spider-Style Strategy Discovery and Schedule Construction.
CoRR
Filip Bártek, Karel Chvalovský, Martin Suda
2023 B conf
Guiding an Instantiation Prover with Graph Neural Networks.
LPAR
Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, 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 Misc conf
Towards Learning Infinite SMT Models (Work in Progress).
SYNASC
Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
2021 — conf
Fast and Slow Enigmas and Parental Guidance.
FroCoS
Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021 J jnl
Fast and Slow Enigmas and Parental Guidance.
CoRR
Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021 B conf
Learning Theorem Proving Components.
TABLEAUX
Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021 J jnl
Learning Theorem Proving Components.
CoRR
Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2020 — conf
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).
IJCAR (2)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020 J jnl
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description).
CoRR
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2019 A conf
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
CADE
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
2019 J jnl
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
CoRR
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
2019 — conf
Top-Down Neural Model For Formulae.
ICLR (Poster)
Karel Chvalovský
2016 J jnl
Full Lambek Calculus with Contraction is Undecidable.
J. Symb. Log.
Karel Chvalovský, Rostislav Horcík
2015 J jnl
Undecidability of Consequence Relation in Full non-Associative Lambek Calculus.
J. Symb. Log.
Karel Chvalovský
2012 J jnl
Note on Deduction Theorems in contraction-free logics.
Math. Log. Q.
Karel Chvalovský, Petr Cintula
2012 J jnl
On the independence of axioms in BL and MTL.
Fuzzy Sets Syst.
Karel Chvalovský
2010 — conf
Note on Deduction Theorems in Contraction-Free Logics.
LPAR short papers(Yogyakarta)
Karel Chvalovský, Petr Cintula