Martin Suda

Karel Chvalovský

Sólrún Halla Einarsdóttir

Proceedings of the 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

Lemma Discovery and Strategies for Automated Induction.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

A Higher-Order Vampire (Short Paper).

[BibT_eX]

[DOI]

Ahmed Bhayat

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Regularization in Spider-Style Strategy Discovery and Schedule Construction.

[BibT_eX]

[DOI]

Karel Chvalovský

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Learning Guided Automated Reasoning: A Brief Survey.

[BibT_eX]

[DOI]

Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2023

How Much Should This Symbol Weigh? A GNN-Advised Clause Selection.

[BibT_eX]

[DOI]

Zarathustra Amadeus Goertzel

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

MizAR 60 for Mizar 50.

[BibT_eX]

[DOI]

Jan Jakubuv

Karel Chvalovský

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

Reuse of Introduced Symbols in Automatic Theorem Provers (short paper).

[BibT_eX]

[DOI]

Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description).

[BibT_eX]

[DOI]

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]

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]

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]