Skip to content

Martin Suda

Publication record assembled from the DBLP archive of ranked conferences.

Papers indexed

42

Venues

13

Active years

2009–2025

Best venue rank

A*

Where they publish

Papers

42 indexed papers, newest first.

YearVenueTitleAuthors
2025CADEEfficient Neural Clause-Selection Reinforcement.Martin Suda
2025CAVThe Vampire Diary.Filip Brtek, Ahmed Bhayat, Robin Coutelier, Mrton Hajd, Matthias Hetzenberger, Petra Hozzov, Laura Kovcs, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2025IJCAIUsing Planning for Automated Testing of Video Games.Toms Balyo, Roman Bartk, Luks Chrpa, Michal Cervenka, Filip Dvork, Stephan Gocht, Luks Lipck, Viktor Macek, Dominik Rohcek, Josef Ryz, Martin Suda, Dominik Safrnek, Slavomr Svancr, G. Michael Youngblood
2024IJCARRegularization in Spider-Style Strategy Discovery and Schedule Construction.Filip Brtek, Karel Chvalovsk, Martin Suda
2024IJCARA Higher-Order Vampire (Short Paper).Ahmed Bhayat, Martin Suda
2024IJCARLemma Discovery and Strategies for Automated Induction.Slrn Halla Einarsdttir, Mrton Hajd, Moa Johansson, Nicholas Smallbone, Martin Suda
2024KRPlanning Domain Model Acquisition from State Traces without Action Parameters.Toms Balyo, Martin Suda, Luks Chrpa, Dominik Safrnek, Stephan Gocht, Filip Dvork, Roman Bartk, G. Michael Youngblood
2023ITPMizAR 60 for Mizar 50.Jan Jakubuv, Karel Chvalovsk, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsk, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2023LPARHow Much Should This Symbol Weigh? A GNN-Advised Clause Selection.Filip Brtek, Martin Suda
2022CADEVampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description).Martin Suda
2021CADEImproving ENIGMA-style Clause Selection while Learning From History.Martin Suda
2021CADENeural Precedence Recommender.Filip Brtek, Martin Suda
2020CADELearning Precedences from Simple Symbol Features.Filip Brtek, Martin Suda
2020CADELayered Clause Selection for Theory Reasoning - (Short Paper).Bernhard Gleiss, Martin Suda
2020CADELayered Clause Selection for Saturation-Based Theorem Proving.Bernhard Gleiss, Martin Suda
2020CADEENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).Jan Jakubuv, Karel Chvalovsk, Miroslav Olsk, Bartosz Piotrowski, Martin Suda, Josef Urban
2019CADEENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.Karel Chvalovsk, Jan Jakubuv, Martin Suda, Josef Urban
2019SYNASCSuperposition Reasoning about Quantified Bitvector Formulas.David Damestani, Laura Kovcs, Martin Suda
2019TACASTOOLympics 2019: An Overview of Competitions in Formal Methods.Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada
2018LPARTowards Smarter MACE-style Model Finders.Mikolas Janota, Martin Suda
2018LPARA Theory of Satisfiability-Preserving Proofs in SAT Solving.Adrin Rebola-Pardo, Martin Suda
2018SATLocal Soundness for QBF Calculi.Martin Suda, Bernhard Gleiss
2018TACASUnification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.Giles Reger, Martin Suda, Andrei Voronkov
2017CADESplitting Proofs for Interpolation.Bernhard Gleiss, Laura Kovcs, Martin Suda
2017CADEA Unifying Principle for Clause Elimination in First-Order Logic.Benjamin Kiesl, Martin Suda
2017CADECheckable Proofs for First-Order Theorem Proving.Giles Reger, Martin Suda
2017LPARBlocked Clauses in First-Order Logic.Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
2017LPARSet of Support for Theory Reasoning.Giles Reger, Martin Suda
2017TAPTesting a Saturation-Based Theorem Prover: Experiences and Challenges.Giles Reger, Martin Suda, Andrei Voronkov
2016CADESelecting the Selection.Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
2016CADEGlobal Subsumption Revisited (Briefly).Giles Reger, Martin Suda
2016SATLifting QBF Resolution Calculi to DQBF.Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
2016SATFinding Finite Models in Multi-sorted First-Order Logic.Giles Reger, Martin Suda, Andrei Voronkov
2015CADEThe Uses of SAT Solvers in Vampire.Giles Reger, Martin Suda
2015CADEPlaying with AVATAR.Giles Reger, Martin Suda, Andrei Voronkov
2014CADEThe Challenges of Evaluating a New Feature in Vampire.Giles Reger, Martin Suda, Andrei Voronkov
2012CADEA PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.Martin Suda, Christoph Weidenbach
2012LPARLabelled Superposition for PLTL.Martin Suda, Christoph Weidenbach
2010CADEOn the Saturation of YAGO.Martin Suda, Christoph Weidenbach, Patrick Wischnewski
2010FlAIRSProgress Towards Effective Automated Reasoning with World Knowledge.Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, Gerard de Melo
2009CADESPASS Version 3.5.Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski
2009KIExternal Sources of Axioms in Automated Theorem Proving.Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo