Martin Suda

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

New Techniques that Improve ENIGMA-style Clause Selection Guidance.

[BibT_eX]

[DOI]

CoRR, 2021

SAT Competition 2020.

[BibT_eX]

[DOI]

Artif. Intell., 2021

Vampire with a Brain Is a Good ITP Hammer.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Neural Precedence Recommender.

[BibT_eX]

[DOI]

Filip Bártek

Proceedings of the Automated Deduction - CADE 28, 2021

Improving ENIGMA-style Clause Selection while Learning From History.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Layered Clause Selection for Theory Reasoning.

[BibT_eX]

[DOI]

CoRR, 2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Layered Clause Selection for Saturation-Based Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020

Layered Clause Selection for Theory Reasoning - (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

Learning Precedences from Simple Symbol Features.

[BibT_eX]

[DOI]

Filip Bártek

2019

SAT Competition 2018.

[BibT_eX]

[DOI]

Marijn J. H. Heule

Matti Järvisalo

J. Satisf. Boolean Model. Comput., 2019

Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Aiming for the Goal with SInE.

[BibT_eX]

[DOI]

Proceedings of the Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, 2019

TOOLympics 2019: An Overview of Competitions in Formal Methods.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Superposition Reasoning about Quantified Bitvector Formulas.

[BibT_eX]

[DOI]

David Damestani

Laura Kovács

Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019

Symmetry Avoidance in MACE-Style Finite Model Finding.

[BibT_eX]

[DOI]

Martin Riener

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Local Soundness for QBF Calculi.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

A Theory of Satisfiability-Preserving Proofs in SAT Solving.

[BibT_eX]

[DOI]

Adrián Rebola-Pardo

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Towards Smarter MACE-style Model Finders.

[BibT_eX]

[DOI]

Mikolas Janota

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).

[BibT_eX]

[DOI]

CoRR, 2017

Testing a Saturation-Based Theorem Prover: Experiences and Challenges.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 11th International Conference, 2017

Instantiation and Pretending to be an SMT Solver with Vampire.

[BibT_eX]

[DOI]

Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

Set of Support for Theory Reasoning.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Blocked Clauses in First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Automated Invention of Strategies and Term Orderings for Vampire.

[BibT_eX]

[DOI]

Jan Jakubuv

Josef Urban

Proceedings of the GCAI 2017, 2017

Checkable Proofs for First-Order Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the ARCADE 2017, 2017

A Unifying Principle for Clause Elimination in First-Order Logic.

[BibT_eX]

[DOI]

Benjamin Kiesl

Proceedings of the Automated Deduction - CADE 26, 2017

Splitting Proofs for Interpolation.

[BibT_eX]

[DOI]

Laura Kovács

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Lifting QBF Resolution Calculi to DQBF.

[BibT_eX]

[DOI]

Electron. Colloquium Comput. Complex., 2016

Finding Finite Models in Multi-sorted First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

AVATAR Modulo Theories.

[BibT_eX]

[DOI]

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

New Techniques in Clausal Form Generation.

[BibT_eX]

[DOI]

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

A Clausal Normal Form Translation for FOOL.

[BibT_eX]

[DOI]

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

Global Subsumption Revisited (Briefly).

[BibT_eX]

[DOI]

Proceedings of the Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, 2016

Selecting the Selection.

[BibT_eX]

[DOI]

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

2015

Resolution-based methods for linear temporal reasoning.

[BibT_eX]

[DOI]

PhD thesis, 2015

Variable and Clause Elimination for LTL Satisfiability Checking.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2015

Playing with AVATAR.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

The Uses of SAT Solvers in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2015

2014

Property Directed Reachability for Automated Planning.

[BibT_eX]

[DOI]

J. Artif. Intell. Res., 2014

The Challenges of Evaluating a New Feature in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

2013

Duality in STRIPS planning

[BibT_eX]

[DOI]

CoRR, 2013

Triggered Clause Pushing for IC3.

[BibT_eX]

[DOI]

CoRR, 2013

2012

Labelled Superposition for PLTL.

[BibT_eX]

[DOI]

Christoph Weidenbach

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance.

[BibT_eX]

[DOI]

Christoph Weidenbach

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2010

Progress Towards Effective Automated Reasoning with World Knowledge.

[BibT_eX]

[DOI]

Geoff Sutcliffe

Alexandra Teyssandier

Nelson Dellis

Gerard de Melo

Proceedings of the Twenty-Third International Florida Artificial Intelligence Research Society Conference, 2010

On the Saturation of YAGO.

[BibT_eX]

[DOI]

Christoph Weidenbach

Patrick Wischnewski

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

External Sources of Axioms in Automated Theorem Proving.

[BibT_eX]

[DOI]