Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDMartin 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
Books and Theses
- 2015
[b1]Martin Suda:
Resolution-based methods for linear temporal reasoning. Saarland University, 2015
Journal Articles
- 2021
- [j5]Nils Froleyks
, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda:
SAT Competition 2020. Artif. Intell. 301: 103572 (2021) - 2019
- [j4]Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda:
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) - 2015
- [j2]Martin Suda:
Variable and Clause Elimination for LTL Satisfiability Checking. Math. Comput. Sci. 9(3): 327-344 (2015) - 2014
- [j1]Martin Suda:
Property Directed Reachability for Automated Planning. J. Artif. Intell. Res. 50: 265-319 (2014)
Conference and Workshop Papers
- 2023
- [c45]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: 19:1-19:22 - [c44]Filip Bártek, Martin Suda:
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection. LPAR 2023: 96-111 - 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
- [c41]Filip Bártek, Martin Suda:
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 - 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ý, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban:
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) 2020: 448-463 - 2019
- [c34]Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban:
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE 2019: 197-215 - [c33]Giles Reger, Martin Riener, Martin Suda:
Symmetry Avoidance in MACE-Style Finite Model Finding. FroCos 2019: 3-21 - [c32]David Damestani, Laura Kovács, Martin Suda:
Superposition Reasoning about Quantified Bitvector Formulas. SYNASC 2019: 95-99 - [c31]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: 3-24 - [c30]Martin Suda:
Aiming for the Goal with SInE. Vampire 2019: 38-44 - 2018
- [c29]Mikolas Janota, Martin Suda:
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, Bernhard Gleiss:
Local Soundness for QBF Calculi. SAT 2018: 217-234 - [c26]Giles Reger, Martin Suda, Andrei Voronkov:
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS (1) 2018: 3-22 - 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, Martin Suda:
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, Martin Suda:
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, Martin Suda, Andrei Voronkov:
Testing a Saturation-Based Theorem Prover: Experiences and Challenges. TAP@STAF 2017: 152-161 - 2016
- [c17]Giles Reger, Martin Suda:
Global Subsumption Revisited (Briefly). Vampire@IJCAR 2016: 61-73 - [c16]Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov:
Selecting the Selection. IJCAR 2016: 313-329 - [c15]Giles Reger, Martin Suda, Andrei Voronkov:
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, Martin Suda, Andrei Voronkov:
Finding Finite Models in Multi-sorted First-Order Logic. SAT 2016: 323-341 - [c11]Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda:
Lifting QBF Resolution Calculi to DQBF. SAT 2016: 490-499 - 2015
- [c10]Giles Reger, Martin Suda:
The Uses of SAT Solvers in Vampire. Vampire Workshop 2015: 63-69 - [c9]Giles Reger, Martin Suda, Andrei Voronkov:
Playing with AVATAR. CADE 2015: 399-415 - 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 - 2012
- [c6]Martin Suda, Christoph Weidenbach:
A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. IJCAR 2012: 537-543 - [c5]Martin Suda, Christoph Weidenbach:
Labelled Superposition for PLTL. LPAR 2012: 391-405 - 2010
- [c4]Martin Suda, Christoph Weidenbach, Patrick Wischnewski:
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 - 2009
- [c2]Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski:
SPASS Version 3.5. CADE 2009: 140-145 - [c1]Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo:
External Sources of Axioms in Automated Theorem Proving. KI 2009: 281-288
Editorship
- 2023
- [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] - 2021
- [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] - 2019
- [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] - 2018
- [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
- [e1]Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, Martin Suda:
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]
Informal and Other Publications
- 2024
- [i18]Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban:
Learning Guided Automated Reasoning: A Brief Survey. CoRR abs/2403.04017 (2024) - [i17]Filip Bártek, Karel Chvalovský, Martin Suda:
Regularization in Spider-Style Strategy Discovery and Schedule Construction. CoRR abs/2403.12869 (2024) - 2023
- [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) - 2021
- [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
- [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) - 2019
- [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) - 2017
- [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
- [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) - 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)
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-04-21 18:03 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:
