Martin Suda

ORCID

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 59

Top Venues

Saarland University (PHD)

Education History

Saarland University

PHD

Publications

Filip Bártek, Karel Chvalovský, Martin Suda
Cautious Specialization of Strategy Schedules (Extended Abstract). PAAR+SC²@IJCAR (2024)
Ahmed Bhayat, Martin Suda
A Higher-Order Vampire (Short Paper). IJCAR (1) (2024)
Filip Bártek, Karel Chvalovský, Martin Suda
Regularization in Spider-Style Strategy Discovery and Schedule Construction. CoRR (2024)
Filip Bártek, Karel Chvalovský, Martin Suda
Regularization in Spider-Style Strategy Discovery and Schedule Construction. IJCAR (1) (2024)
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
Learning Guided Automated Reasoning: A Brief Survey. Logics and Type Systems in Theory and Practice (2024)
Ahmed Bhayat, Martin Suda
A Higher-Order Vampire (Short Paper). CoRR (2024)
Sólrún Halla Einarsdóttir, Márton Hajdú, Moa Johansson, Nicholas Smallbone, Martin Suda
Lemma Discovery and Strategies for Automated Induction. IJCAR (1) (2024)
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
Learning Guided Automated Reasoning: A Brief Survey. CoRR (2024)
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
MizAR 60 for Mizar 50. CoRR (2023)
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
MizAR 60 for Mizar 50. ITP (2023)
Filip Bártek, Martin Suda
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection. LPAR (2023)
Martin Suda
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). IJCAR (2022)
Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger
Reuse of Introduced Symbols in Automatic Theorem Provers (short paper). PAAR@IJCAR (2022)
Filip Bártek, Martin Suda
Neural Precedence Recommender. CADE (2021)
Martin Suda
Vampire With a Brain Is a Good ITP Hammer. CoRR (2021)
Martin Suda
Vampire with a Brain Is a Good ITP Hammer. FroCoS (2021)
Martin Suda
New Techniques that Improve ENIGMA-style Clause Selection Guidance. CoRR (2021)
Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda
SAT Competition 2020. Artif. Intell. 301 (2021)
Martin Suda
Improving ENIGMA-style Clause Selection while Learning From History. CADE (2021)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). CoRR (2020)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) (2020)
Bernhard Gleiss, Martin Suda
Layered Clause Selection for Theory Reasoning - (Short Paper). IJCAR (1) (2020)
Bernhard Gleiss, Martin Suda
Layered Clause Selection for Saturation-Based Theorem Proving. PAAR+SC²@IJCAR (2020)
Bernhard Gleiss, Martin Suda
Layered Clause Selection for Theory Reasoning. CoRR (2020)
Filip Bártek, Martin Suda
Learning Precedences from Simple Symbol Features. PAAR+SC²@IJCAR (2020)
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CoRR (2019)
Giles Reger, Martin Riener, Martin Suda
Symmetry Avoidance in MACE-Style Finite Model Finding. FroCos (2019)
Martin Suda
Aiming for the Goal with SInE. Vampire (2019)
Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. J. Autom. Reason. 63 (3) (2019)
David Damestani, Laura Kovács, Martin Suda
Superposition Reasoning about Quantified Bitvector Formulas. SYNASC (2019)
Marijn J. H. Heule, Matti Järvisalo, Martin Suda
SAT Competition 2018. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE (2019)
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
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) (2019)
Mikolas Janota, Martin Suda
Towards Smarter MACE-style Model Finders. LPAR (2018)
Martin Suda, Bernhard Gleiss
Local Soundness for QBF Calculi. SAT (2018)
Adrián Rebola-Pardo, Martin Suda
A Theory of Satisfiability-Preserving Proofs in SAT Solving. LPAR (2018)
Giles Reger, Martin Suda, Andrei Voronkov
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS (1) (2018)
Giles Reger, Martin Suda, Andrei Voronkov
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). CoRR (2017)
Giles Reger, Martin Suda
Set of Support for Theory Reasoning. IWIL@LPAR (2017)
Giles Reger, Martin Suda
Checkable Proofs for First-Order Theorem Proving. ARCADE@CADE (2017)
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
Blocked Clauses in First-Order Logic. LPAR (2017)
Bernhard Gleiss, Laura Kovács, Martin Suda
Splitting Proofs for Interpolation. CADE (2017)
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
Blocked Clauses in First-Order Logic. CoRR (2017)
Bernhard Gleiss, Laura Kovács, Martin Suda
Splitting Proofs for Interpolation. CoRR (2017)
Jan Jakubuv, Martin Suda, Josef Urban
Automated Invention of Strategies and Term Orderings for Vampire. GCAI (2017)
Giles Reger, Martin Suda, Andrei Voronkov
Instantiation and Pretending to be an SMT Solver with Vampire. SMT (2017)
Benjamin Kiesl, Martin Suda
A Unifying Principle for Clause Elimination in First-Order Logic. CADE (2017)
Giles Reger, Martin Suda, Andrei Voronkov
Testing a Saturation-Based Theorem Prover: Experiences and Challenges. TAP@STAF (2017)
Giles Reger, Martin Suda, Andrei Voronkov
New Techniques in Clausal Form Generation. GCAI (2016)
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Lifting QBF Resolution Calculi to DQBF. SAT (2016)
Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder
Selecting the Selection. CoRR (2016)
Giles Reger, Martin Suda
Global Subsumption Revisited (Briefly). Vampire@IJCAR (2016)
Giles Reger, Nikolaj Bjørner, Martin Suda, Andrei Voronkov
AVATAR Modulo Theories. GCAI (2016)
Giles Reger, Martin Suda, Andrei Voronkov
Finding Finite Models in Multi-sorted First-Order Logic. SAT (2016)
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Lifting QBF Resolution Calculi to DQBF. CoRR (2016)
Giles Reger, Martin Suda, Andrei Voronkov
Finding Finite Models in Multi-Sorted First Order Logic. CoRR (2016)
Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
A Clausal Normal Form Translation for FOOL. GCAI (2016)
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
Lifting QBF Resolution Calculi to DQBF. Electron. Colloquium Comput. Complex. 23 (2016)
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
Selecting the Selection. IJCAR (2016)
Martin Suda
Variable and Clause Elimination for LTL Satisfiability Checking. Math. Comput. Sci. 9 (3) (2015)
Giles Reger, Martin Suda, Andrei Voronkov
Playing with AVATAR. CADE (2015)
Giles Reger, Martin Suda
The Uses of SAT Solvers in Vampire. Vampire Workshop (2015)
Giles Reger, Martin Suda, Andrei Voronkov
The Challenges of Evaluating a New Feature in Vampire. Vampire Workshop (2014)
Martin Suda
Property Directed Reachability for Automated Planning. ICAPS (2014)
Martin Suda
Property Directed Reachability for Automated Planning. J. Artif. Intell. Res. 50 (2014)
Martin Suda
Variable and clause elimination for LTL satisfiability checking. CoRR (2013)
Martin Suda
Duality in STRIPS planning CoRR (2013)
Martin Suda
Triggered Clause Pushing for IC3. CoRR (2013)
Martin Suda, Christoph Weidenbach
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. IJCAR (2012)
Martin Suda, Christoph Weidenbach
Labelled Superposition for PLTL. LPAR (2012)
Martin Suda, Christoph Weidenbach, Patrick Wischnewski
On the Saturation of YAGO. IJCAR (2010)
Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, Gerard de Melo
Progress Towards Effective Automated Reasoning with World Knowledge. FLAIRS Conference (2010)
Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo
External Sources of Axioms in Automated Theorem Proving. KI (2009)
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski
SPASS Version 3.5. CADE (2009)

Martin Suda.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Martin Suda