Author:Martin Suda

Publications
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection Filip Bártek and Martin Suda In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) Martin Suda EasyChair Preprint no. 7719
Aiming for the Goal with SInE Martin Suda In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
LPAR-22 Workshop and Short Paper Proceedings Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe and Margus Veanes (editors) Kalpa Publications in Computing, volume 9
Towards Smarter MACE-style Model Finders Mikolas Janota and Martin Suda In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Theory of Satisfiability-Preserving Proofs in SAT Solving Adrián Rebola-Pardo and Martin Suda In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Local Soundness for QBF Calculi Martin Suda and Bernhard Gleiss EasyChair Preprint no. 362
Towards the Semantics of QBF Clauses Martin Suda EasyChair Preprint no. 361
Local proofs and AVATAR Giles Reger and Martin Suda In:Vampire 2017. Proceedings of the 4th Vampire Workshop
Incremental Solving with Vampire Giles Reger and Martin Suda In:Vampire 2017. Proceedings of the 4th Vampire Workshop
Checkable Proofs for First-Order Theorem Proving Giles Reger and Martin Suda In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Automated Invention of Strategies and Term Orderings for Vampire Jan Jakubuv, Martin Suda and Josef Urban In:GCAI 2017. 3rd Global Conference on Artificial Intelligence
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning Giles Reger, Martin Suda and Andrei Voronkov EasyChair Preprint no. 1
Set of Support for Theory Reasoning Giles Reger and Martin Suda In:IWIL Workshop and LPAR Short Presentations
Blocked Clauses in First-Order Logic Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits and Armin Biere In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Global Subsumption Revisited (Briefly) Giles Reger and Martin Suda In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
New Techniques in Clausal Form Generation Giles Reger, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
AVATAR Modulo Theories Giles Reger, Nikolaj Bjorner, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
A Clausal Normal Form Translation for FOOL Evgenii Kotelnikov, Laura Kovács, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
The Challenges of Evaluating a New Feature in Vampire Giles Reger, Martin Suda and Andrei Voronkov In:Proceedings of the 1st and 2nd Vampire Workshops
The Uses of SAT Solvers in Vampire Giles Reger and Martin Suda In:Proceedings of the 1st and 2nd Vampire Workshops

Keyphrases

automated reasoning⁴, automated theorem proving³, Avatar⁴, AVATAR architecture, blocked clauses, CEGAR, Clausal Normal Form, clause elimination, clause normal form, Clause selection, Clausification, EPR, evaluation, finite model finder, first-order logic⁷, first-order theorem proving², FOOL, Graph Neural Network, inprocessing techniques, Interference, Interpolants, IRM-calc, large theory problems, local proofs, long-distance resolution, machine learning², Parameters Learning, partial strategy, premise selection, Preprocessing, proof checking, proving strategy, QBF, QBF calculi, randomization, Resolution Calculi, SAT², SAT solving, Satisfiability Modulo Theories², Saturation Algorithms², saturation-based theorem proving², semantics², sine, SMT, SMT solving², strategies, strategy invention, superposition calculus, theorem proving⁸, theory reasoning, translation, Vampire⁷, winning strategy, Z3.