Martin Suda

According to our database1, Martin Suda authored at least 42 papers between 2009 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
Layered Clause Selection for Theory Reasoning.
CoRR, 2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Layered Clause Selection for Theory Reasoning - (Short Paper).
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
SAT Competition 2018.
J. Satisf. Boolean Model. Comput., 2019

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.
J. Autom. Reason., 2019

TOOLympics 2019: An Overview of Competitions in Formal Methods.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Superposition Reasoning about Quantified Bitvector Formulas.
Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019

Symmetry Avoidance in MACE-Style Finite Model Finding.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Local Soundness for QBF Calculi.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

A Theory of Satisfiability-Preserving Proofs in SAT Solving.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Towards Smarter MACE-style Model Finders.
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

2017
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).
CoRR, 2017

Testing a Saturation-Based Theorem Prover: Experiences and Challenges.
Proceedings of the Tests and Proofs - 11th International Conference, 2017

Set of Support for Theory Reasoning.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Blocked Clauses in First-Order Logic.
Proceedings of the LPAR-21, 2017

Automated Invention of Strategies and Term Orderings for Vampire.
Proceedings of the GCAI 2017, 2017

Checkable Proofs for First-Order Theorem Proving.
Proceedings of the ARCADE 2017, 2017

A Unifying Principle for Clause Elimination in First-Order Logic.
Proceedings of the Automated Deduction - CADE 26, 2017

Splitting Proofs for Interpolation.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Lifting QBF Resolution Calculi to DQBF.
Electron. Colloquium Comput. Complex., 2016

Finding Finite Models in Multi-sorted First-Order Logic.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

AVATAR Modulo Theories.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

New Techniques in Clausal Form Generation.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

A Clausal Normal Form Translation for FOOL.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

Global Subsumption Revisited (Briefly).
Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016

Selecting the Selection.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Resolution-based methods for linear temporal reasoning.
PhD thesis, 2015

Variable and Clause Elimination for LTL Satisfiability Checking.
Math. Comput. Sci., 2015

Playing with AVATAR.
Proceedings of the Automated Deduction - CADE-25, 2015

The Uses of SAT Solvers in Vampire.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2015

2014
Property Directed Reachability for Automated Planning.
J. Artif. Intell. Res., 2014

The Challenges of Evaluating a New Feature in Vampire.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

2013
Duality in STRIPS planning
CoRR, 2013

Triggered Clause Pushing for IC3.
CoRR, 2013

2012
Labelled Superposition for PLTL.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2010
Progress Towards Effective Automated Reasoning with World Knowledge.
Proceedings of the Twenty-Third International Florida Artificial Intelligence Research Society Conference, 2010

On the Saturation of YAGO.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
External Sources of Axioms in Automated Theorem Proving.
Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

SPASS Version 3.5.
Proceedings of the Automated Deduction, 2009


  Loading...