default search action
Martin Suda 0001
Person information
- affiliation: Czech Technical University in Prague, Czech Republic
- affiliation (former): TU Wien, Vienna, Austria
- affiliation (former): University of Manchester, UK
- affiliation (former): Max Planck Institute for Informatics, Saarbrücken, Germany
Other persons with the same name
- Martin Suda 0002 — Austrian Institute of Technology, Safety & Security Department (and 1 more)
- Martin Suda 0003 — Filuta AI, Inc., New York, NY, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [c50]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: 54-83 - [c49]Ahmed Bhayat
A Higher-Order Vampire (Short Paper). IJCAR (1) 2024: 75-85 - [c48]Filip Bártek
Regularization in Spider-Style Strategy Discovery and Schedule Construction. IJCAR (1) 2024: 194-213 - [c47]Sólrún Halla Einarsdóttir
Lemma Discovery and Strategies for Automated Induction. IJCAR (1) 2024: 214-232 - [c46]Filip Bártek, Karel Chvalovský, Martin Suda:
Cautious Specialization of Strategy Schedules (Extended Abstract). PAAR+SC²@IJCAR 2024: 28-36 - [e6]Christopher W. Brown, Daniela Kaufmann, Cláudia Nalon, Alexander Steen, Martin Suda:
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. CEUR Workshop Proceedings 3717, CEUR-WS.org 2024 [contents] - [i19]Lasse Blaauwbroek, David M. Cerna
Learning Guided Automated Reasoning: A Brief Survey. CoRR abs/2403.04017 (2024) - [i18]Filip Bártek, Karel Chvalovský, Martin Suda:
Regularization in Spider-Style Strategy Discovery and Schedule Construction. CoRR abs/2403.12869 (2024) - [i17]Ahmed Bhayat, Martin Suda:
A Higher-Order Vampire (Short Paper). CoRR abs/2407.05208 (2024) - 2023
- [c45]Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk
MizAR 60 for Mizar 50. ITP 2023: 19:1-19:22 - [c44]Filip Bártek
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection. LPAR 2023: 96-111 - [e5]Uli Sattler, Martin Suda:
Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings. Lecture Notes in Computer Science 14279, Springer 2023, ISBN 978-3-031-43368-9 [contents] - [i16]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 abs/2303.06686 (2023) - 2022
- [c43]Martin Suda
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description). IJCAR 2022: 659-667 - [c42]Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger:
Reuse of Introduced Symbols in Automatic Theorem Provers (short paper). PAAR@IJCAR 2022 - 2021
- [j5]Nils Froleyks
SAT Competition 2020. Artif. Intell. 301: 103572 (2021) - [c41]Filip Bártek
Neural Precedence Recommender. CADE 2021: 525-542 - [c40]Martin Suda
Improving ENIGMA-style Clause Selection while Learning From History. CADE 2021: 543-561 - [c39]Martin Suda
Vampire with a Brain Is a Good ITP Hammer. FroCoS 2021: 192-209 - [e4]Martin Suda, Sarah Winkler
Proceedings of the Third International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2021, Virtual Event, July 16, 2021. 2021 [contents] - [i15]Martin Suda:
Vampire With a Brain Is a Good ITP Hammer. CoRR abs/2102.03529 (2021) - [i14]Martin Suda:
New Techniques that Improve ENIGMA-style Clause Selection Guidance. CoRR abs/2102.13564 (2021) - 2020
- [c38]Filip Bártek, Martin Suda:
Learning Precedences from Simple Symbol Features. PAAR+SC²@IJCAR 2020: 21-33 - [c37]Bernhard Gleiss, Martin Suda:
Layered Clause Selection for Saturation-Based Theorem Proving. PAAR+SC²@IJCAR 2020: 34-52 - [c36]Bernhard Gleiss, Martin Suda:
Layered Clause Selection for Theory Reasoning - (Short Paper). IJCAR (1) 2020: 402-409 - [c35]Jan Jakubuv, Karel Chvalovský
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) 2020: 448-463 - [i13]Bernhard Gleiss, Martin Suda:
Layered Clause Selection for Theory Reasoning. CoRR abs/2001.09705 (2020) - [i12]Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban:
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). CoRR abs/2002.05406 (2020)
2010 – 2019
- 2019
- [j4]Olaf Beyersdorff
Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF. J. Autom. Reason. 63(3): 597-623 (2019) - [j3]Marijn J. H. Heule, Matti Järvisalo, Martin Suda:
SAT Competition 2018. J. Satisf. Boolean Model. Comput. 11(1): 133-154 (2019) - [c34]Karel Chvalovský
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE 2019: 197-215 - [c33]Giles Reger
Symmetry Avoidance in MACE-Style Finite Model Finding. FroCos 2019: 3-21 - [c32]David Damestani, Laura Kovács
Superposition Reasoning about Quantified Bitvector Formulas. SYNASC 2019: 95-99 - [c31]Ezio Bartocci
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) 2019: 3-24 - [c30]Martin Suda:
Aiming for the Goal with SInE. Vampire 2019: 38-44 - [e3]Martin Suda, Sarah Winkler
Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2019, Natal, Brazil, August 26, 2019. EPTCS 311, 2019 [contents] - [i11]Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban:
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CoRR abs/1903.03182 (2019) - 2018
- [c29]Mikolas Janota
Towards Smarter MACE-style Model Finders. LPAR 2018: 454-470 - [c28]Adrián Rebola-Pardo, Martin Suda:
A Theory of Satisfiability-Preserving Proofs in SAT Solving. LPAR 2018: 583-603 - [c27]Martin Suda
Local Soundness for QBF Calculi. SAT 2018: 217-234 - [c26]Giles Reger
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS (1) 2018: 3-22 - [e2]Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes:
LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018. Kalpa Publications in Computing 9, EasyChair 2018 [contents] - 2017
- [c25]Giles Reger, Martin Suda:
Checkable Proofs for First-Order Theorem Proving. ARCADE@CADE 2017: 55-63 - [c24]Benjamin Kiesl, Martin Suda
A Unifying Principle for Clause Elimination in First-Order Logic. CADE 2017: 274-290 - [c23]Bernhard Gleiss, Laura Kovács
Splitting Proofs for Interpolation. CADE 2017: 291-309 - [c22]Jan Jakubuv, Martin Suda, Josef Urban:
Automated Invention of Strategies and Term Orderings for Vampire. GCAI 2017: 121-133 - [c21]Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere:
Blocked Clauses in First-Order Logic. LPAR 2017: 31-48 - [c20]Giles Reger
Set of Support for Theory Reasoning. IWIL@LPAR 2017: 124-134 - [c19]Giles Reger, Martin Suda, Andrei Voronkov:
Instantiation and Pretending to be an SMT Solver with Vampire. SMT 2017: 63-75 - [c18]Giles Reger
Testing a Saturation-Based Theorem Prover: Experiences and Challenges. TAP@STAF 2017: 152-161 - [e1]Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa
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. CEUR Workshop Proceedings 1785, CEUR-WS.org 2017 [contents] - [i10]Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere:
Blocked Clauses in First-Order Logic. CoRR abs/1702.00847 (2017) - [i9]Giles Reger, Martin Suda, Andrei Voronkov:
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). CoRR abs/1704.03391 (2017) - [i8]Bernhard Gleiss, Laura Kovács, Martin Suda:
Splitting Proofs for Interpolation. CoRR abs/1711.02503 (2017) - 2016
- [c17]Giles Reger, Martin Suda:
Global Subsumption Revisited (Briefly). Vampire@IJCAR 2016: 61-73 - [c16]Krystof Hoder, Giles Reger
Selecting the Selection. IJCAR 2016: 313-329 - [c15]Giles Reger
New Techniques in Clausal Form Generation. GCAI 2016: 11-23 - [c14]Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov:
AVATAR Modulo Theories. GCAI 2016: 39-52 - [c13]Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov:
A Clausal Normal Form Translation for FOOL. GCAI 2016: 53-71 - [c12]Giles Reger
Finding Finite Models in Multi-sorted First-Order Logic. SAT 2016: 323-341 - [c11]Olaf Beyersdorff
Lifting QBF Resolution Calculi to DQBF. SAT 2016: 490-499 - [i7]Giles Reger, Martin Suda, Andrei Voronkov:
Finding Finite Models in Multi-Sorted First Order Logic. CoRR abs/1604.08040 (2016) - [i6]Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder:
Selecting the Selection. CoRR abs/1604.08055 (2016) - [i5]Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda:
Lifting QBF Resolution Calculi to DQBF. CoRR abs/1604.08058 (2016) - [i4]Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda:
Lifting QBF Resolution Calculi to DQBF. Electron. Colloquium Comput. Complex. TR16 (2016) - 2015
- [b1]Martin Suda:
Resolution-based methods for linear temporal reasoning. Saarland University, 2015 - [j2]Martin Suda
Variable and Clause Elimination for LTL Satisfiability Checking. Math. Comput. Sci. 9(3): 327-344 (2015) - [c10]Giles Reger, Martin Suda:
The Uses of SAT Solvers in Vampire. Vampire Workshop 2015: 63-69 - [c9]Giles Reger
Playing with AVATAR. CADE 2015: 399-415 - 2014
- [j1]Martin Suda:
Property Directed Reachability for Automated Planning. J. Artif. Intell. Res. 50: 265-319 (2014) - [c8]Martin Suda:
Property Directed Reachability for Automated Planning. ICAPS 2014 - [c7]Giles Reger, Martin Suda, Andrei Voronkov:
The Challenges of Evaluating a New Feature in Vampire. Vampire Workshop 2014: 70-74 - 2013
- [i3]Martin Suda:
Duality in STRIPS planning. CoRR abs/1304.0897 (2013) - [i2]Martin Suda:
Variable and clause elimination for LTL satisfiability checking. CoRR abs/1306.5539 (2013) - [i1]Martin Suda:
Triggered Clause Pushing for IC3. CoRR abs/1307.4966 (2013) - 2012
- [c6]Martin Suda
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. IJCAR 2012: 537-543 - [c5]Martin Suda
Labelled Superposition for PLTL. LPAR 2012: 391-405 - 2010
- [c4]Martin Suda
On the Saturation of YAGO. IJCAR 2010: 441-456 - [c3]Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, Gerard de Melo:
Progress Towards Effective Automated Reasoning with World Knowledge. FLAIRS 2010
2000 – 2009
- 2009
- [c2]Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda
SPASS Version 3.5. CADE 2009: 140-145 - [c1]Martin Suda
External Sources of Axioms in Automated Theorem Proving. KI 2009: 281-288
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:23 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: