Deductive Program Synthesis and Markov's Principle. - Andrei Voronkov (FCT, 1987)

On connections between classical and constructive semantics. - Sergei Starchenko; Andrei Voronkov (Conference on Computer Logic, 1988)

A proof-search method for the first-order logic. - Andrei Voronkov (Conference on Computer Logic, 1988)

LISS - The Logic Inference Search System. - Andrei Voronkov (CADE, 1990)

Towards the Theory of Programming in Constructive Logic. - Andrei Voronkov (ESOP, 1990)

On Completeness of Program Synthesis Systems. - Andrei Voronkov (CSL, 1991)

Logic Programming with Bounded Quantifiers. - Andrei Voronkov (RCLP, 1991)

Declarative and Procedural Paradigms - Do they Really Compete? (Panel). - Harold Boley; Micha Meier; Chris Moss; Michael M. Richter; Andrei Voronkov (PDK, 1991)

Theorem Proving in Non-Standard Logics Based on the Inverse Method. - Andrei Voronkov (CADE, 1992)

Higher Order Functions in First Order Theory. - Andrei Voronkov (ISTCS, 1992)

A Construction of Typed Lambda Models Related to Feasible Computability. - Vladimir Yu. Sazonov; Andrei Voronkov (Kurt Gödel Colloquium, 1993)

An Implementation Technique for a Class of Bottom-Up Procedures. - Andrei Voronkov (PLILP, 1994)

Simultaneous Regid E-Unification Is Undecidable. - Anatoli Degtyarev; Andrei Voronkov (CSL, 1995)

A New Procedural Interpretation of Horn Clauses with Equality. - Anatoli Degtyarev; Andrei Voronkov (ICLP, 1995)

Equality Elimination for the Inverse Method and Extension Procedures. - Anatoli Degtyarev; Andrei Voronkov (IJCAI, 1995)

General Connections via Equality Elimination. - Anatoli Degtyarev; Andrei Voronkov (WOCFAI, 1995)

On Computability by Logic Programs. - Andrei Voronkov (Ann. Math. Artif. Intell., 1995)

The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees. - Andrei Voronkov (J. Autom. Reason., 1995)

Equality Elimination for the Tableau Method. - Anatoli Degtyarev; Andrei Voronkov (DISCO, 1996)

Semantics of Constraint Logic Programs with Bounded Quantifiers. - Martin Argenius; Andrei Voronkov (ELP, 1996)

Handling Equality in Logic Programming via Basic Folding. - Anatoli Degtyarev; Andrei Voronkov (ELP, 1996)

Merging Relational Database Technology with Constraint Technology. - Andrei Voronkov (Ershov Memorial Conference, 1996)

Simultaneous E-Unification and Related Algorithmic Problems. - Anatoli Degtyarev; Yuri V. Matiyasevich; Andrei Voronkov (LICS, 1996)

Decidability Problems for the Prenex Fragment of Intuitionistic Logic. - Anatoli Degtyarev; Andrei Voronkov (LICS, 1996)

Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction. - Andrei Voronkov (TABLEAUX, 1996)

Herbrand's Theorem and Equational Reasoning: Problems and Solutions. - Anatoli Degtyarev; Yuri Gurevich; Andrei Voronkov (Bull. EATCS, 1996)

A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers. - Anatoli Degtyarev; Andrei Voronkov (J. Log. Program., 1996)

The Undecidability of Simultaneous Rigid E-Unification. - Anatoli Degtyarev; Andrei Voronkov (Theor. Comput. Sci., 1996)

Monadic Simultaneous Rigid E-Unification and Related Problems. - Yuri Gurevich; Andrei Voronkov (ICALP, 1997)

Strategies in Rigid-Variable Methods. - Andrei Voronkov (IJCAI (1), 1997)

Complexity of Query Answering in Logic Databases with Complex Values. - Evgeny Dantsin; Andrei Voronkov (LFCS, 1997)

Elimination of Equality via Transformation with Ordering Constraints. - Leo Bachmair; Harald Ganzinger; Andrei Voronkov (CADE, 1998)

Herbrand's Theorem, Automated Reasoning and Semantics Tableaux. - Andrei Voronkov (LICS, 1998)

Complexity of Nonrecursive Logic Programs with Complex Values. - Sergei G. Vorobyov; Andrei Voronkov (PODS, 1998)

The Decidability of Simultaneous Rigid E-Unification with One Variable. - Anatoli Degtyarev; Yuri Gurevich; Paliath Narendran; Margus Veanes; Andrei Voronkov (RTA, 1998)

What You Always Wanted to Know about Rigid E-Unification. - Anatoli Degtyarev; Andrei Voronkov (J. Autom. Reason., 1998)

Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. - Andrei Voronkov (J. Autom. Reason., 1998)

Vampire. - Alexandre Riazanov; Andrei Voronkov (CADE, 1999)

KK: a theorem prover for K. - Andrei Voronkov (CADE, 1999)

A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees. - Evgeny Dantsin; Andrei Voronkov (FoSSaCS, 1999)

The Ground-Negative Fragment of First-Order Logic Is Pip2-Complete. - Andrei Voronkov (J. Symb. Log., 1999)

Monadic Simultaneous Rigid E-unification. - Yuri Gurevich; Andrei Voronkov (Theor. Comput. Sci., 1999)

Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem. - Andrei Voronkov (Theor. Comput. Sci., 1999)

The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. - Konstantin Korovin; Andrei Voronkov (ARW, 2000)

System Description: Vampire 1.0. - Alexandre Riazanov; Andrei Voronkov (ARW, 2000)

Stratified Resolution. - Anatoli Degtyarev; Andrei Voronkov (CADE, 2000)

Partially Adaptive Code Trees. - Alexandre Riazanov; Andrei Voronkov (JELIA, 2000)

Deciding K using inverse-K. - Andrei Voronkov (KR, 2000)

A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. - Konstantin Korovin; Andrei Voronkov (LICS, 2000)

How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. - Andrei Voronkov (LICS, 2000)

Expressive Power and Data Complexity of Query Languages for Trees and Lists. - Evgeny Dantsin; Andrei Voronkov (PODS, 2000)

Decidability and complexity of simultaneous rigid E-unification with one variable and related results. - Anatoli Degtyarev; Yuri Gurevich; Paliath Narendran; Margus Veanes; Andrei Voronkov (Theor. Comput. Sci., 2000)

The Inverse Method. - Anatoli Degtyarev; Andrei Voronkov (Handbook of Automated Reasoning, 2001)

Equality Reasoning in Sequent-Based Calculi. - Anatoli Degtyarev; Andrei Voronkov (Handbook of Automated Reasoning, 2001)

Term Indexing. - I. V. Ramakrishnan; R. Sekar 001; Andrei Voronkov (Handbook of Automated Reasoning, 2001)

Preface. - John Alan Robinson; Andrei Voronkov (Handbook of Automated Reasoning, 2001)

Herbrand's Theorem and Equational Reasoning: Problems and Solutions. - Anatoli Degtyarev; Yuri Gurevich; Andrei Voronkov (Current Trends in Theoretical Computer Science, 2001)

On the Evaluation of Indexing Techniques for Theorem Proving. - Robert Nieuwenhuis; Thomas Hillenbrand; Alexandre Riazanov; Andrei Voronkov (IJCAR, 2001)

Vampire 1.1 (System Description). - Alexandre Riazanov; Andrei Voronkov (IJCAR, 2001)

Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. - Andrei Voronkov (IJCAR, 2001)

Adaptive Saturation-Based Reasoning. - Alexandre Riazanov; Andrei Voronkov (Ershov Memorial Conference, 2001)

Splitting Without Backtracking. - Alexandre Riazanov; Andrei Voronkov (IJCAI, 2001)

Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. - Konstantin Korovin; Andrei Voronkov (RTA, 2001)

Complexity and expressive power of logic programming. - Evgeny Dantsin; Thomas Eiter; Georg Gottlob; Andrei Voronkov (ACM Comput. Surv., 2001)

Term-Modal Logics. - Melvin Fitting; Lars Thalmann; Andrei Voronkov (Stud Logica, 2001)

A decision procedure for term algebras with queues. - Tatiana Rybina; Andrei Voronkov (ACM Trans. Comput. Log., 2001)

How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. - Andrei Voronkov (ACM Trans. Comput. Log., 2001)

BRAIN : Backward Reachability Analysis with Integers. - Tatiana Rybina; Andrei Voronkov (AMAST, 2002)

Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. - Tatiana Rybina; Andrei Voronkov (CAV, 2002)

First-Order Theorem Provers: the Next Generation. - Andrei Voronkov (Description Logics, 2002)

The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. - Konstantin Korovin; Andrei Voronkov (FSTTCS, 2002)

The design and implementation of VAMPIRE. - Alexandre Riazanov; Andrei Voronkov (AI Commun., 2002)

An AC-Compatible Knuth-Bendix Order. - Konstantin Korovin; Andrei Voronkov (CADE, 2003)

Complexity of Some Problems in Modal and Intuitionistic Calculi. - Larisa Maksimova; Andrei Voronkov (CSL, 2003)

Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture). - Tatiana Rybina; Andrei Voronkov (CSL, 2003)

A Logical Reconstruction of Reachability. - Tatiana Rybina; Andrei Voronkov (Ershov Memorial Conference, 2003)

Upper Bounds for a Theory of Queues. - Tatiana Rybina; Andrei Voronkov (ICALP, 2003)

Automated Reasoning: Past Story and New Trends. - Andrei Voronkov (IJCAI, 2003)

Orienting Equalities with the Knuth-Bendix Order. - Konstantin Korovin; Andrei Voronkov (LICS, 2003)

Orienting rewrite rules with the Knuth-Bendix order. - Konstantin Korovin; Andrei Voronkov (Inf. Comput., 2003)

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. - Andrei Voronkov (J. Autom. Reason., 2003)

Stratified resolution. - Anatoli Degtyarev; Robert Nieuwenhuis; Andrei Voronkov (J. Symb. Comput., 2003)

Limited resource strategy in resolution theorem proving. - Alexandre Riazanov; Andrei Voronkov (J. Symb. Comput., 2003)

TeMP: A Temporal Monodic Prover. - Ullrich Hustadt; Boris Konev; Alexandre Riazanov; Andrei Voronkov (IJCAR, 2004)

Efficient Checking of Term Ordering Constraints. - Alexandre Riazanov; Andrei Voronkov (IJCAR, 2004)

Generation of Hard Non-Clausal Random Satisfiability Problems. - Juan Antonio Navarro Pérez; Andrei Voronkov (AAAI, 2005)

Solving First-Order Constraints over the Monadic Class. - Dimitri Chubarov; Andrei Voronkov (Mechanizing Mathematical Reasoning, 2005)

05431 Executive Summary - Deduction and Applications. - Franz Baader; Peter Baumgartner 001; Robert Nieuwenhuis; Andrei Voronkov (Deduction and Applications, 2005)

05431 Abstracts Collection - Deduction and Applications. - Franz Baader; Peter Baumgartner 001; Robert Nieuwenhuis; Andrei Voronkov (Deduction and Applications, 2005)

Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. - Dimitri Chubarov; Andrei Voronkov (MFCS, 2005)

Random Databases and Threshold for Monotone Non-recursive Datalog. - Konstantin Korovin; Andrei Voronkov (MFCS, 2005)

Finding Basic Block and Variable Correspondence. - Iman Narasamdya; Andrei Voronkov (SAS, 2005)

Efficient instance retrieval with standard and relational path indexing. - Alexandre Riazanov; Andrei Voronkov (Inf. Comput., 2005)

Knuth-Bendix constraint solving is NP-complete. - Konstantin Korovin; Andrei Voronkov (ACM Trans. Comput. Log., 2005)

Implementation of UNIDOOR, a Deductive Object-Oriented Database System. - Mohammed K. Jaber; Andrei Voronkov (ADBIS, 2006)

Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. - Ian Horrocks 001; Andrei Voronkov (FoIKS, 2006)

UNIDOOR: a Deductive Object-Oriented Database Management System. - Mohammed K. Jaber; Andrei Voronkov (ICDE, 2006)

Inconsistencies in Ontologies. - Andrei Voronkov (JELIA, 2006)

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. - Juan Antonio Navarro Pérez; Andrei Voronkov (CADE, 2007)

Integrating Linear Arithmetic into Superposition Calculus. - Konstantin Korovin; Andrei Voronkov (CSL, 2007)

Encodings of Problems in Effectively Propositional Logic. - Juan Antonio Navarro Pérez; Andrei Voronkov (SAT, 2007)

Proof Systems for Effectively Propositional Logic. - Juan Antonio Navarro Pérez; Andrei Voronkov (IJCAR, 2008)

Interpolation and Symbol Elimination. - Laura Kovács; Andrei Voronkov (CADE, 2009)

Conflict Resolution. - Konstantin Korovin; Nestan Tsiskaridze; Andrei Voronkov (CP, 2009)

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. - Laura Kovács; Andrei Voronkov (FASE, 2009)

Verifying equivalence of memories using a first order logic theorem prover. - Zurab Khasidashvili; Mahmoud Kinanah; Andrei Voronkov (FMCAD, 2009)

Comparing Unification Algorithms in First-Order Theorem Proving. - Krystof Hoder; Andrei Voronkov (KI, 2009)

Inter-program Properties. - Andrei Voronkov; Iman Narasamdya (SAS, 2009)

Satisfiability and Theories. - Andrei Voronkov (SYNASC, 2009)

Path Feasibility Analysis for String-Manipulating Programs. - Nikolaj S. Bjørner; Nikolai Tillmann; Andrei Voronkov (TACAS, 2009)

Interpolation and Symbol Elimination in Vampire. - Krystof Hoder; Laura Kovács; Andrei Voronkov (IJCAR, 2010)

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Decision Procedures in Software, Hardware and Bioware, 2010)

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Decision Procedures in Software, Hardware and Bioware, 2010)

Encoding industrial hardware verification problems into effectively propositional logic. - Moshe Emmer; Zurab Khasidashvili; Konstantin Korovin; Andrei Voronkov (FMCAD, 2010)

Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. - Josef Urban; Krystof Hoder; Andrei Voronkov (ICMS, 2010)

Invariant and Type Inference for Matrices. - Thomas A. Henzinger; Thibaud Hottelier; Laura Kovács; Andrei Voronkov (VMCAI, 2010)

EasyChair. - Andrei Voronkov (WWV, 2010)

Sine Qua Non for Large Theory Reasoning. - Krystof Hoder; Andrei Voronkov (CADE, 2011)

Solving Systems of Linear Inequalities by Bound Propagation. - Konstantin Korovin; Andrei Voronkov (CADE, 2011)

On Transfinite Knuth-Bendix Orders. - Laura Kovács; Georg Moser; Andrei Voronkov (CADE, 2011)

Implementing Conflict Resolution. - Konstantin Korovin; Nestan Tsiskaridze; Andrei Voronkov (Ershov Memorial Conference, 2011)

GoRRiLA and Hard Reality. - Konstantin Korovin; Andrei Voronkov (Ershov Memorial Conference, 2011)

Case Studies on Invariant Generation Using a Saturation Theorem Prover. - Krystof Hoder; Laura Kovács; Andrei Voronkov (MICAI (1), 2011)

Invariant Generation in Vampire. - Krystof Hoder; Laura Kovács; Andrei Voronkov (TACAS, 2011)

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Dagstuhl Reports, 2011)

Vinter: A Vampire-Based Tool for Interpolation. - Krystof Hoder; Andreas Holzer; Laura Kovács; Andrei Voronkov (APLAS, 2012)

EPR-Based Bounded Model Checking at Word Level. - Moshe Emmer; Zurab Khasidashvili; Konstantin Korovin; Christoph Sticksel; Andrei Voronkov (IJCAR, 2012)

Preprocessing techniques for first-order clausification. - Krystof Hoder; Zurab Khasidashvili; Konstantin Korovin; Andrei Voronkov (FMCAD, 2012)

Playing in the grey area of proofs. - Krystof Hoder; Laura Kovács; Andrei Voronkov (POPL, 2012)

Translating regular expression matching into transducers. - Yuto Sakuma; Yasuhiko Minamide; Andrei Voronkov (J. Appl. Log., 2012)

Harald Ganzinger's Legacy: Contributions to Logics and Programming. - Deepak Kapur; Robert Nieuwenhuis; Andrei Voronkov; Christoph Weidenbach; Reinhard Wilhelm (Programming Logics, 2013)

Planning with Effectively Propositional Logic. - Juan Antonio Navarro Pérez; Andrei Voronkov (Programming Logics, 2013)

The 481 Ways to Split a Clause and Deal with Propositional Variables. - Krystof Hoder; Andrei Voronkov (CADE, 2013)

First-Order Theorem Proving and Vampire. - Laura Kovács; Andrei Voronkov (CAV, 2013)

PDFX: fully-automated PDF-to-XML conversion of scientific literature. - Alexandru Constantin; Steve Pettifer; Andrei Voronkov (ACM Symposium on Document Engineering, 2013)

The Inverse Method for Many-Valued Logics. - Laura Kovács; Andrei Mantsivoda; Andrei Voronkov (MICAI (1), 2013)

Bound Propagation for Arithmetic Reasoning in Vampire. - Ioan Dragan; Konstantin Korovin; Laura Kovács; Andrei Voronkov (SYNASC, 2013)

Extensional Crisis and Proving Identity. - Ashutosh Gupta; Laura Kovács; Bernhard Kragl; Andrei Voronkov (ATVA, 2014)

SAT solving experiments in Vampire. - Armin Biere; Ioan Dragan; Laura Kovács; Andrei Voronkov (Vampire Workshop, 2014)

The Challenges of Evaluating a New Feature in Vampire. - Giles Reger; Martin Suda 001; Andrei Voronkov (Vampire Workshop, 2014)

AVATAR: The Architecture for First-Order Theorem Provers. - Andrei Voronkov (CAV, 2014)

Keynote talk: EasyChair. - Andrei Voronkov (ASE, 2014)

Experimenting with SAT Solvers in Vampire. - Armin Biere; Ioan Dragan; Laura Kovács; Andrei Voronkov (MICAI (1), 2014)

Playing with AVATAR. - Giles Reger; Martin Suda 001; Andrei Voronkov (CADE, 2015)

Cooperating Proof Attempts. - Giles Reger; Dmitry Tishkovsky; Andrei Voronkov (CADE, 2015)

A First Class Boolean Sort in First-Order Theorem Proving and TPTP. - Evgenii Kotelnikov; Laura Kovács; Andrei Voronkov (CICM, 2015)

Selecting the Selection. - Krystof Hoder; Giles Reger; Martin Suda 001; Andrei Voronkov (IJCAR, 2016)

The vampire and the FOOL. - Evgenii Kotelnikov; Laura Kovács; Giles Reger; Andrei Voronkov (CPP, 2016)

A Clausal Normal Form Translation for FOOL. - Evgenii Kotelnikov; Laura Kovács; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

New Techniques in Clausal Form Generation. - Giles Reger; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

AVATAR Modulo Theories. - Giles Reger; Nikolaj S. Bjørner; Martin Suda 001; Andrei Voronkov (GCAI, 2016)

Finding Finite Models in Multi-sorted First-Order Logic. - Giles Reger; Martin Suda 001; Andrei Voronkov (SAT, 2016)

First-Order Interpolation and Interpolating Proof Systems. - Laura Kovács; Andrei Voronkov (LPAR, 2017)

Coming to terms with quantified reasoning. - Laura Kovács; Simon Robillard; Andrei Voronkov (POPL, 2017)

Instantiation and Pretending to be an SMT Solver with Vampire. - Giles Reger; Martin Suda 001; Andrei Voronkov (SMT, 2017)

Testing a Saturation-Based Theorem Prover: Experiences and Challenges. - Giles Reger; Martin Suda 001; Andrei Voronkov (TAP@STAF, 2017)

Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). - Giles Reger; Martin Suda 001; Andrei Voronkov (CoRR, 2017)

A FOOLish Encoding of the Next State Relations of Imperative Programs. - Evgenii Kotelnikov; Laura Kovács; Andrei Voronkov (IJCAR, 2018)

Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning. - Andrei Voronkov (SYNASC, 2018)

Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. - Giles Reger; Martin Suda 001; Andrei Voronkov (TACAS (1), 2018)

Induction in Saturation-Based Proof Search. - Giles Reger; Andrei Voronkov (CADE, 2019)

Induction with Generalization in Superposition Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2020)

Integer Induction in Saturation. - Petra Hozzová; Laura Kovács; Andrei Voronkov (CADE, 2021)

Induction with Recursive Definitions in Superposition. - Márton Hajdú; Petra Hozzová; Laura Kovács; Andrei Voronkov (FMCAD, 2021)

Inductive Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Johannes Schoisswohl; Andrei Voronkov (CICM, 2021)

Making Theory Reasoning Simpler. - Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (2), 2021)

Getting Saturated with Induction. - Márton Hajdú; Petra Hozzová; Laura Kovács; Giles Reger; Andrei Voronkov (Principles of Systems Design, 2022)

The Vampire Approach to Induction (short paper). - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (PAAR@IJCAR, 2022)

Program Synthesis in Saturation. - Petra Hozzová; Laura Kovács; Chase Norman; Andrei Voronkov (CADE, 2023)

ALASCA: Reasoning in Quantified Linear Arithmetic. - Konstantin Korovin; Laura Kovács; Giles Reger; Johannes Schoisswohl; Andrei Voronkov (TACAS (1), 2023)

Reducibility Constraints in Superposition. - Márton Hajdú; Laura Kovács; Michael Rawson 001; Andrei Voronkov (IJCAR (1), 2024)

Synthesis of Recursive Programs in Saturation. - Petra Hozzová; Daneshvar Amrollahi; Márton Hajdú; Laura Kovács; Andrei Voronkov; Eva Maria Wagner (IJCAR (1), 2024)

Induction in Saturation. - Laura Kovács; Petra Hozzová; Márton Hajdú; Andrei Voronkov (IJCAR (1), 2024)

Term Ordering Diagrams. - Márton Hajdú; Robin Coutelier; Laura Kovács; Andrei Voronkov (CADE, 2025)

Partial Redundancy in Saturation. - Márton Hajdú; Laura Kovács; Andrei Voronkov (CADE, 2025)

Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. - Michael Rawson 001; Andrei Voronkov; Johannes Schoisswohl; Anja Petkovic Komel (CADE, 2025)

The Vampire Diary. - Filip Bártek; Ahmed Bhayat; Robin Coutelier; Márton Hajdú; Matthias Hetzenberger; Petra Hozzová; Laura Kovács; Jakob Rath; Michael Rawson 001; Giles Reger; Martin Suda 001; Johannes Schoisswohl; et al. (CAV (3), 2025)

Synthesis Benchmarks for Automated Reasoning. - Márton Hajdú; Petra Hozzová; Laura Kovács; Andrei Voronkov; Eva Maria Wagner; Richard Steven Zilincík (CoRR, 2025)