2024
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
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
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
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
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
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
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
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
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
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001
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
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
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
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