Author:Martin Suda

Publications
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, Clausification, EPR, finite model finder, first-order logic⁷, first-order theorem proving, FOOL, inprocessing techniques, Interference, Interpolants, IRM-calc, local proofs, long-distance resolution, machine learning, Parameters Learning, partial strategy, Preprocessing, proof checking, proving strategy, QBF, QBF calculi, Resolution Calculi, SAT², SAT solving, Satisfiability Modulo Theories², Saturation Algorithms², semantics², SMT, SMT solving², strategies, strategy invention, superposition calculus, theorem proving⁸, theory reasoning, translation, Vampire⁶, winning strategy, Z3.