Martin Suda

93 papers A* 3A 15B 6C 1Misc 3Journal 30Unranked 28
YearRankTypeTitle / Venue / Authors
2026 J jnl
Reintroducing the Second Player in EPR.
CoRR
Leroy Chew, Mikolás Janota, Miroslav Olsák, Martin Suda
2025 — conf
Boosting Vampire with Neural Networks.
SC-Square@CADE
Martin Suda, Filip Bártek
2025 J jnl
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo.
CoRR
Anja Petkovic Komel, Michael Rawson, Martin Suda
2025 A conf
Efficient Neural Clause-Selection Reinforcement.
CADE
Martin Suda
2025 J jnl
Efficient Neural Clause-Selection Reinforcement.
CoRR
Martin Suda
2025 C conf
Hammering Higher Order Set Theory.
CICM
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025 J jnl
Hammering Higher Order Set Theory.
CoRR
Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025 — conf
The Vampire Diary.
CAV (3)
Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2025 J jnl
The Vampire Diary.
CoRR
Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2025 A* conf
Using Planning for Automated Testing of Video Games.
IJCAI
Tomás Balyo, Roman Barták, Lukás Chrpa, Michal Cervenka, Filip Dvorák, Stephan Gocht, Lukás Lipcák, Viktor Macek, Dominik Rohácek, Josef Ryzí, Martin Suda, Dominik Safránek, Slavomír Svancár, G. Michael Youngblood
2024 — conf
A Higher-Order Vampire (Short Paper).
IJCAR (1)
Ahmed Bhayat, Martin Suda
2024 J jnl
A Higher-Order Vampire (Short Paper).
CoRR
Ahmed Bhayat, Martin Suda
2024 — conf
Cautious Specialization of Strategy Schedules (Extended Abstract).
PAAR+SC²@IJCAR
Filip Bártek, Karel Chvalovský, Martin Suda
2024 — ed.
Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024 co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2, 2024.
PAAR+SC²@IJCAR
Christopher W. Brown, Daniela Kaufmann, Cláudia Nalon, Alexander Steen, Martin Suda
2024 — conf
Learning Guided Automated Reasoning: A Brief Survey.
Logics and Type Systems in Theory and Practice
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
2024 J jnl
Learning Guided Automated Reasoning: A Brief Survey.
CoRR
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
2024 J jnl
Learning Planning Action Models from State Traces.
CoRR
Tomás Balyo, Martin Suda, Lukás Chrpa, Dominik Safránek, Filip Dvorák, Roman Barták, G. Michael Youngblood
2024 — conf
Lemma Discovery and Strategies for Automated Induction.
IJCAR (1)
Sólrún Halla Einarsdóttir, Márton Hajdú, Moa Johansson, Nicholas Smallbone, Martin Suda
2024 A* conf
Planning Domain Model Acquisition from State Traces without Action Parameters.
KR
Tomás Balyo, Martin Suda, Lukás Chrpa, Dominik Safránek, Stephan Gocht, Filip Dvorák, Roman Barták, G. Michael Youngblood
2024 — conf
Regularization in Spider-Style Strategy Discovery and Schedule Construction.
IJCAR (1)
Filip Bártek, Karel Chvalovský, Martin Suda
2024 J jnl
Regularization in Spider-Style Strategy Discovery and Schedule Construction.
CoRR
Filip Bártek, Karel Chvalovský, Martin Suda
2023 — ed.
Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings
FroCoS
Uli Sattler, Martin Suda
2023 B conf
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection.
LPAR
Filip Bártek, Martin Suda
2023 B conf
MizAR 60 for Mizar 50.
ITP
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2023 J jnl
MizAR 60 for Mizar 50.
CoRR
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2022 — conf
Reuse of Introduced Symbols in Automatic Theorem Provers (short paper).
PAAR@IJCAR
Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger
2022 A conf
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description).
IJCAR
Martin Suda
2021 A conf
Improving ENIGMA-style Clause Selection while Learning From History.
CADE
Martin Suda
2021 A conf
Neural Precedence Recommender.
CADE
Filip Bártek, Martin Suda
2021 J jnl
New Techniques that Improve ENIGMA-style Clause Selection Guidance.
CoRR
Martin Suda
2021 — ed.
Proceedings of the Third International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2021, Virtual Event, July 16, 2021.
ARCADE@CADE
Martin Suda, Sarah Winkler
2021 J jnl
SAT Competition 2020.
Artif. Intell.
Nils Froleyks, Marijn Heule, Ashlin Iser, Matti Järvisalo, Martin Suda
2021 J jnl
Vampire With a Brain Is a Good ITP Hammer.
CoRR
Martin Suda
2021 — conf
Vampire with a Brain Is a Good ITP Hammer.
FroCoS
Martin Suda
2020 — conf
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).
IJCAR (2)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020 J jnl
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description).
CoRR
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020 — conf
Layered Clause Selection for Saturation-Based Theorem Proving.
PAAR+SC²@IJCAR
Bernhard Gleiss, Martin Suda
2020 — conf
Layered Clause Selection for Theory Reasoning - (Short Paper).
IJCAR (1)
Bernhard Gleiss, Martin Suda
2020 J jnl
Layered Clause Selection for Theory Reasoning.
CoRR
Bernhard Gleiss, Martin Suda
2020 — conf
Learning Precedences from Simple Symbol Features.
PAAR+SC²@IJCAR
Filip Bártek, Martin Suda
2019 — conf
Aiming for the Goal with SInE.
Vampire
Martin Suda
2019 A conf
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
CADE
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
2019 J jnl
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
CoRR
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
2019 — ed.
Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2019, Natal, Brazil, August 26, 2019.
ARCADE@CADE
Martin Suda, Sarah Winkler
2019 J jnl
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.
J. Autom. Reason.
Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda
2019 J jnl
SAT Competition 2018.
J. Satisf. Boolean Model. Comput.
Marijn J. H. Heule, Matti Järvisalo, Martin Suda
2019 Misc conf
Superposition Reasoning about Quantified Bitvector Formulas.
SYNASC
David Damestani, Laura Kovács, Martin Suda
2019 — conf
Symmetry Avoidance in MACE-Style Finite Model Finding.
FroCos
Giles Reger, Martin Riener, Martin Suda
2019 — conf
TOOLympics 2019: An Overview of Competitions in Formal Methods.
TACAS (3)
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
2018 B conf
A Theory of Satisfiability-Preserving Proofs in SAT Solving.
LPAR
Adrián Rebola-Pardo, Martin Suda
2018 — ed.
LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018
LPAR (Workshop and Short Papers)
Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes
2018 A conf
Local Soundness for QBF Calculi.
SAT
Martin Suda, Bernhard Gleiss
2018 B conf
Towards Smarter MACE-style Model Finders.
LPAR
Mikolas Janota, Martin Suda
2018 — conf
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.
TACAS (1)
Giles Reger, Martin Suda, Andrei Voronkov
2017 A conf
A Unifying Principle for Clause Elimination in First-Order Logic.
CADE
Benjamin Kiesl, Martin Suda
2017 — conf
Automated Invention of Strategies and Term Orderings for Vampire.
GCAI
Jan Jakubuv, Martin Suda, Josef Urban
2017 B conf
Blocked Clauses in First-Order Logic.
LPAR
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
2017 J jnl
Blocked Clauses in First-Order Logic.
CoRR
Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
2017 — conf
Checkable Proofs for First-Order Theorem Proving.
ARCADE@CADE
Giles Reger, Martin Suda
2017 — conf
Instantiation and Pretending to be an SMT Solver with Vampire.
SMT
Giles Reger, Martin Suda, Andrei Voronkov
2017 — ed.
Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016.
FM4M/MathUI/ThEdu/DP/WIP@CIKM
Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, Martin Suda
2017 — conf
Set of Support for Theory Reasoning.
IWIL@LPAR
Giles Reger, Martin Suda
2017 A conf
Splitting Proofs for Interpolation.
CADE
Bernhard Gleiss, Laura Kovács, Martin Suda
2017 J jnl
Splitting Proofs for Interpolation.
CoRR
Bernhard Gleiss, Laura Kovács, Martin Suda
2017 J jnl
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).
CoRR
Giles Reger, Martin Suda, Andrei Voronkov
2017 — conf
Testing a Saturation-Based Theorem Prover: Experiences and Challenges.
TAP@STAF
Giles Reger, Martin Suda, Andrei Voronkov
2016 — conf
A Clausal Normal Form Translation for FOOL.
GCAI
Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
2016 — conf
AVATAR Modulo Theories.
GCAI
Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov
2016 J jnl
Finding Finite Models in Multi-Sorted First Order Logic.
CoRR
Giles Reger, Martin Suda, Andrei Voronkov
2016 A conf
Finding Finite Models in Multi-sorted First-Order Logic.
SAT
Giles Reger, Martin Suda, Andrei Voronkov
2016 — conf
Global Subsumption Revisited (Briefly).
Vampire@IJCAR
Giles Reger, Martin Suda
2016 A conf
Lifting QBF Resolution Calculi to DQBF.
SAT
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
2016 J jnl
Lifting QBF Resolution Calculi to DQBF.
CoRR
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
2016 J jnl
Lifting QBF Resolution Calculi to DQBF.
Electron. Colloquium Comput. Complex.
Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
2016 — conf
New Techniques in Clausal Form Generation.
GCAI
Giles Reger, Martin Suda, Andrei Voronkov
2016 A conf
Selecting the Selection.
IJCAR
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
2016 J jnl
Selecting the Selection.
CoRR
Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder
2015 A conf
Playing with AVATAR.
CADE
Giles Reger, Martin Suda, Andrei Voronkov
2015 — —
Resolution-based methods for linear temporal reasoning.
Martin Suda
2015 — conf
The Uses of SAT Solvers in Vampire.
Vampire Workshop
Giles Reger, Martin Suda
2015 J jnl
Variable and Clause Elimination for LTL Satisfiability Checking.
Math. Comput. Sci.
Martin Suda
2014 A* conf
Property Directed Reachability for Automated Planning.
ICAPS
Martin Suda
2014 J jnl
Property Directed Reachability for Automated Planning.
J. Artif. Intell. Res.
Martin Suda
2014 — conf
The Challenges of Evaluating a New Feature in Vampire.
Vampire Workshop
Giles Reger, Martin Suda, Andrei Voronkov
2013 J jnl
Duality in STRIPS planning
CoRR
Martin Suda
2013 J jnl
Triggered Clause Pushing for IC3.
CoRR
Martin Suda
2013 J jnl
Variable and clause elimination for LTL satisfiability checking.
CoRR
Martin Suda
2012 A conf
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.
IJCAR
Martin Suda, Christoph Weidenbach
2012 B conf
Labelled Superposition for PLTL.
LPAR
Martin Suda, Christoph Weidenbach
2010 A conf
On the Saturation of YAGO.
IJCAR
Martin Suda, Christoph Weidenbach, Patrick Wischnewski
2010 Misc conf
Progress Towards Effective Automated Reasoning with World Knowledge.
FLAIRS
Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, Gerard de Melo
2009 Misc conf
External Sources of Axioms in Automated Theorem Proving.
KI
Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo
2009 A conf
SPASS Version 3.5.
CADE
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski