2024
Induction in Saturation.
Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Synthesis of Recursive Programs in Saturation.
Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Reducibility Constraints in Superposition.
Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023
ALASCA: Reasoning in Quantified Linear Arithmetic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Program Synthesis in Saturation.
Proceedings of the Automated Deduction - CADE 29, 2023

2022
The Vampire Approach to Induction (short paper).
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

Getting Saturated with Induction.
Proceedings of the Principles of Systems Design, 2022

2021
Making Theory Reasoning Simpler.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Inductive Benchmarks for Automated Reasoning.
Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Induction with Recursive Definitions in Superposition.
Proceedings of the Formal Methods in Computer Aided Design, 2021

Integer Induction in Saturation.
Proceedings of the Automated Deduction - CADE 28, 2021

2020
Induction with Generalization in Superposition Reasoning.
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019
Induction in Saturation-Based Proof Search.
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

Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning.
Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

A FOOLish Encoding of the Next State Relations of Imperative Programs.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 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

Instantiation and Pretending to be an SMT Solver with Vampire.
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

Coming to terms with quantified reasoning.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

First-Order Interpolation and Interpolating Proof Systems.
Proceedings of the LPAR-21, 2017

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

The vampire and the FOOL.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

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

2015
A First Class Boolean Sort in First-Order Theorem Proving and TPTP.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Cooperating Proof Attempts.
Proceedings of the Automated Deduction - CADE-25, 2015

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

2014
Experimenting with SAT Solvers in Vampire.
Proceedings of the Human-Inspired Computing and Its Applications, 2014

Keynote talk: EasyChair.
Proceedings of the ACM/IEEE International Conference on Automated Software Engineering, 2014

AVATAR: The Architecture for First-Order Theorem Provers.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

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

SAT solving experiments in Vampire.
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

Extensional Crisis and Proving Identity.
Proceedings of the Automated Technology for Verification and Analysis, 2014

2013
Bound Propagation for Arithmetic Reasoning in Vampire.
Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

The Inverse Method for Many-Valued Logics.
Proceedings of the Advances in Artificial Intelligence and Its Applications, 2013

PDFX: fully-automated PDF-to-XML conversion of scientific literature.
Proceedings of the ACM Symposium on Document Engineering 2013, 2013

First-Order Theorem Proving and Vampire.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

The 481 Ways to Split a Clause and Deal with Propositional Variables.
Proceedings of the Automated Deduction - CADE-24, 2013

Planning with Effectively Propositional Logic.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

Harald Ganzinger's Legacy: Contributions to Logics and Programming.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012
Translating regular expression matching into transducers.
J. Appl. Log., 2012

Playing in the grey area of proofs.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Preprocessing techniques for first-order clausification.
Proceedings of the Formal Methods in Computer-Aided Design, 2012

EPR-Based Bounded Model Checking at Word Level.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Vinter: A Vampire-Based Tool for Interpolation.
Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272).
Dagstuhl Reports, 2011

Invariant Generation in Vampire.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Case Studies on Invariant Generation Using a Saturation Theorem Prover.
Proceedings of the Advances in Artificial Intelligence, 2011

GoRRiLA and Hard Reality.
Proceedings of the Perspectives of Systems Informatics, 2011

Implementing Conflict Resolution.
Proceedings of the Perspectives of Systems Informatics, 2011

On Transfinite Knuth-Bendix Orders.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Solving Systems of Linear Inequalities by Bound Propagation.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Sine Qua Non for Large Theory Reasoning.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
EasyChair.
Proceedings of the 6th International Workshop on Automated Specification and Verification of Web Systems, 2010

Invariant and Type Inference for Matrices.
Proceedings of the Verification, 2010

Evaluation of Automated Theorem Proving on the Mizar Mathematical Library.
Proceedings of the Mathematical Software, 2010

Encoding industrial hardware verification problems into effectively propositional logic.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware.
Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware.
Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

Interpolation and Symbol Elimination in Vampire.
Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009
Path Feasibility Analysis for String-Manipulating Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Satisfiability and Theories.
Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Inter-program Properties.
Proceedings of the Static Analysis, 16th International Symposium, 2009

Comparing Unification Algorithms in First-Order Theorem Proving.
Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

Verifying equivalence of memories using a first order logic theorem prover.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover.
Proceedings of the Fundamental Approaches to Software Engineering, 2009

Conflict Resolution.
Proceedings of the Principles and Practice of Constraint Programming, 2009

Interpolation and Symbol Elimination.
Proceedings of the Automated Deduction, 2009

2008
Proof Systems for Effectively Propositional Logic.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Encodings of Problems in Effectively Propositional Logic.
Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Integrating Linear Arithmetic into Superposition Calculus.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic.
Proceedings of the Automated Deduction, 2007

2006
Inconsistencies in Ontologies.
Proceedings of the Logics in Artificial Intelligence, 10th European Conference, 2006

UNIDOOR: a Deductive Object-Oriented Database Management System.
Proceedings of the 22nd International Conference on Data Engineering, 2006

Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.
Proceedings of the Foundations of Information and Knowledge Systems, 2006

Implementation of UNIDOOR, a Deductive Object-Oriented Database System.
Proceedings of the Advances in Databases and Information Systems, 2006

2005
Knuth-Bendix constraint solving is NP-complete.
ACM Trans. Comput. Log., 2005

Efficient instance retrieval with standard and relational path indexing.
Inf. Comput., 2005

Finding Basic Block and Variable Correspondence.
Proceedings of the Static Analysis, 12th International Symposium, 2005

Random Databases and Threshold for Monotone Non-recursive Datalog.
Proceedings of the Mathematical Foundations of Computer Science 2005, 2005

Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications.
Proceedings of the Mathematical Foundations of Computer Science 2005, 2005

05431 Abstracts Collection - Deduction and Applications.
Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

05431 Executive Summary - Deduction and Applications.
Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

Solving First-Order Constraints over the Monadic Class.
Proceedings of the Mechanizing Mathematical Reasoning, 2005

Generation of Hard Non-Clausal Random Satisfiability Problems.
Proceedings of the Proceedings, 2005

2004
Efficient Checking of Term Ordering Constraints.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

TeMP: A Temporal Monodic Prover.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Limited resource strategy in resolution theorem proving.
J. Symb. Comput., 2003

Stratified resolution.
J. Symb. Comput., 2003

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

Orienting rewrite rules with the Knuth-Bendix order.
Inf. Comput., 2003

Orienting Equalities with the Knuth-Bendix Order.
Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Automated Reasoning: Past Story and New Trends.
Proceedings of the IJCAI-03, 2003

Upper Bounds for a Theory of Queues.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

A Logical Reconstruction of Reachability.
Proceedings of the Perspectives of Systems Informatics, 2003

Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture).
Proceedings of the Computer Science Logic, 17th International Workshop, 2003

Complexity of Some Problems in Modal and Intuitionistic Calculi.
Proceedings of the Computer Science Logic, 17th International Workshop, 2003

An AC-Compatible Knuth-Bendix Order.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002
The design and implementation of VAMPIRE.
AI Commun., 2002

The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures.
Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

First-Order Theorem Provers: the Next Generation.
Proceedings of the 2002 International Workshop on Description Logics (DL2002), 2002

Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

BRAIN : Backward Reachability Analysis with Integers.
Proceedings of the Algebraic Methodology and Software Technology, 2002

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

A decision procedure for term algebras with queues.
ACM Trans. Comput. Log., 2001

Term-Modal Logics.
Stud Logica, 2001

Complexity and expressive power of logic programming.
ACM Comput. Surv., 2001

Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.
Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

Splitting Without Backtracking.
Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

Adaptive Saturation-Based Reasoning.
Proceedings of the Perspectives of System Informatics, 2001

Algorithms, Datastructures, and other Issues in Efficient Automated Deduction.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Vampire 1.1 (System Description).
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

On the Evaluation of Indexing Techniques for Theorem Proving.
Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Herbrand's Theorem and Equational Reasoning: Problems and Solutions.
Proceedings of the Current Trends in Theoretical Computer Science, 2001

Preface.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Term Indexing.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Equality Reasoning in Sequent-Based Calculi.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

The Inverse Method.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000
Decidability and complexity of simultaneous rigid E-unification with one variable and related results.
Theor. Comput. Sci., 2000

Expressive Power and Data Complexity of Query Languages for Trees and Lists.
Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2000

How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi.
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Deciding K using inverse-K.
Proceedings of the KR 2000, 2000

Partially Adaptive Code Trees.
Proceedings of the Logics in Artificial Intelligence, European Workshop, 2000

Stratified Resolution.
Proceedings of the Automated Deduction, 2000

System Description: Vampire 1.0.
Proceedings of the Seventh Workshop on Automated Reasoning, 2000

The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable.
Proceedings of the Seventh Workshop on Automated Reasoning, 2000

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

Monadic Simultaneous Rigid E-unification.
Theor. Comput. Sci., 1999

The Ground-Negative Fragment of First-Order Logic Is Pi<sup>p</sup><sub>2</sub>-Complete.
J. Symb. Log., 1999

A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees.
Proceedings of the Foundations of Software Science and Computation Structure, 1999

KK: a theorem prover for K.
Proceedings of the Automated Deduction, 1999

Vampire.
Proceedings of the Automated Deduction, 1999

1998
Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid <i>E</i>-Unification.
J. Autom. Reason., 1998

What You Always Wanted to Know about Rigid E-Unification.
J. Autom. Reason., 1998

The Decidability of Simultaneous Rigid <i>E</i>-Unification with One Variable.
Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

Complexity of Nonrecursive Logic Programs with Complex Values.
Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1998

Herbrand's Theorem, Automated Reasoning and Semantics Tableaux.
Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Elimination of Equality via Transformation with Ordering Constraints.
Proceedings of the Automated Deduction, 1998

1997
Complexity of Query Answering in Logic Databases with Complex Values.
Proceedings of the Logical Foundations of Computer Science, 4th International Symposium, 1997

Strategies in Rigid-Variable Methods.
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

Monadic Simultaneous Rigid E-Unification and Related Problems.
Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997

1996
The Undecidability of Simultaneous Rigid E-Unification.
Theor. Comput. Sci., 1996

A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers.
J. Log. Program., 1996

Herbrand's Theorem and Equational Reasoning: Problems and Solutions.
Bull. EATCS, 1996

Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction.
Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1996

Decidability Problems for the Prenex Fragment of Intuitionistic Logic.
Proceedings of the Proceedings, 1996

Simultaneous E-Unification and Related Algorithmic Problems.
Proceedings of the Proceedings, 1996

Merging Relational Database Technology with Constraint Technology.
Proceedings of the Perspectives of System Informatics, 1996

Handling Equality in Logic Programming via Basic Folding.
Proceedings of the Extensions of Logic Programming, 5th International Workshop, 1996

Semantics of Constraint Logic Programs with Bounded Quantifiers.
Proceedings of the Extensions of Logic Programming, 5th International Workshop, 1996

Equality Elimination for the Tableau Method.
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

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

On Computability by Logic Programs.
Ann. Math. Artif. Intell., 1995

General Connections via Equality Elimination.
Proceedings of the Second World Conference on the Fundamentals of Artificial Intelligence, 1995

Equality Elimination for the Inverse Method and Extension Procedures.
Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

A New Procedural Interpretation of Horn Clauses with Equality.
Proceedings of the Logic Programming, 1995

Simultaneous Regid E-Unification Is Undecidable.
Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994
An Implementation Technique for a Class of Bottom-Up Procedures.
Proceedings of the Programming Language Implementation and Logic Programming, 1994

1993
A Construction of Typed Lambda Models Related to Feasible Computability.
Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

1992
Higher Order Functions in First Order Theory.
Proceedings of the Theory of Computing and Systems, 1992

Theorem Proving in Non-Standard Logics Based on the Inverse Method.
Proceedings of the Automated Deduction, 1992

1991
Declarative and Procedural Paradigms - Do they Really Compete? (Panel).
Proceedings of the Processing Declarative Knowledge, 1991

Logic Programming with Bounded Quantifiers.
Proceedings of the Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990, 1991

On Completeness of Program Synthesis Systems.
Proceedings of the Computer Science Logic, 5th Workshop, 1991

1990
Towards the Theory of Programming in Constructive Logic.
Proceedings of the ESOP'90, 1990

LISS - The Logic Inference Search System.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1988
A proof-search method for the first-order logic.
Proceedings of the COLOG-88, 1988

On connections between classical and constructive semantics.
Proceedings of the COLOG-88, 1988

1987
Deductive Program Synthesis and Markov's Principle.
Proceedings of the Fundamentals of Computation Theory, 1987