Author:Karel Chvalovský

Publications
Neural Conjecturing for Saturation Theorem Provers Karel Chvalovský, Martin Suda and Josef Urban In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection Karel Chvalovský, Martin Suda and Josef Urban In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Guiding an Instantiation Prover with Graph Neural Networks Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock and Josef Urban In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Note on Deduction Theorems in Contraction-Free Logics Karel Chvalovský and Petr Cintula In:LPAR-17-short. short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning.

Keyphrases

BCI logic, Clause Evaluation, conjecturing, contraction-free logics, E prover, Graph Neural Networks, ITP hammers, lemma introduction, local deduction theorems, machine learning², Mizar, neural clause-selection guidance, proving strategies, saturation-based theorem proving, theorem proving, Vampire².