Andrei Voronkov | Academic Influence

Andrei Voronkov's AcademicInfluence.com Rankings

Andrei Voronkov

Computer Science

#1308

World Rank

#1352

Historical Rank

Database

#7285

World Rank

#7541

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Andrei Voronkov's Degrees

PhD Computer Science University of Manchester
Masters Computer Science University of Manchester
Bachelors Computer Science University of Manchester

Similar Degrees You Can Earn

Why Is Andrei Voronkov Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester. Education Voronkov was educated at Novosibirsk State University, graduating with a PhD in 1987.

(See a Problem?)

Andrei Voronkov's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Complexity and expressive power of logic programming (1997) (854)
Handbook of automated reasoning (2001) (545)
The design and implementation of VAMPIRE (2002) (528)
First-Order Theorem Proving and Vampire (2013) (476)
Handbook of Automated Reasoning (in 2 volumes) (2001) (201)
Term Indexing (1995) (198)
Conflict Resolution (2009) (196)
Path Feasibility Analysis for String-Manipulating Programs (2009) (184)
Automated Deduction—CADE-18 (2002) (171)
Sine Qua Non for Large Theory Reasoning (2011) (155)
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (2009) (153)
Handbook of Automated Reasoning: Volume 1 (2001) (117)
PDFX: fully-automated PDF-to-XML conversion of scientific literature (2013) (116)
Vampire 1.1 (System Description) (2001) (113)
AVATAR: The Architecture for First-Order Theorem Provers (2014) (111)
The Inverse Method (2001) (99)
Splitting Without Backtracking (2001) (85)
Limited resource strategy in resolution theorem proving (2003) (81)
Interpolation and Symbol Elimination (2009) (78)
Logic for Programming, Artificial Intelligence, and Reasoning (2015) (64)
Equality Reasoning in Sequent-Based Calculi (2001) (64)
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover (2006) (59)
The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees (1995) (59)
Current Trends in Theoretical Computer Science (2001) (58)
The Undecidability of Simultaneous Rigid E-Unification (1996) (58)
Integrating Linear Arithmetic into Superposition Calculus (2007) (56)
A decision procedure for term algebras with queues (2000) (55)
The anatomy of vampire (1995) (52)
On the Evaluation of Indexing Techniques for Theorem Proving (2001) (50)
Interpolation and Symbol Elimination in Vampire (2010) (49)
Transactions and Change in Logic Databases (1997) (47)
TeMP: A Temporal Monodic Prover (2004) (47)
Logic Programming with Bounded Quantifiers (1990) (46)
Coming to terms with quantified reasoning (2016) (45)
Orienting rewrite rules with the Knuth-Bendix order (2003) (44)
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library (2010) (44)
Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction (1996) (44)
Playing with AVATAR (2015) (44)
Theorem Proving in Non-Standard Logics Based on the Inverse Method (1992) (42)
Selecting the Selection (2016) (40)
Invariant Generation in Vampire (2011) (40)
Complexity of nonrecursive logic programs with complex values (1998) (38)
Simultaneous Regid E-Unification Is Undecidable (1995) (36)
Playing in the grey area of proofs (2012) (36)
The vampire and the FOOL (2015) (35)
Elimination of Equality via Transformation with Ordering Constraints (1998) (33)
New Techniques in Clausal Form Generation (2016) (33)
Simultaneous rigid E-unification and related algorithmic problems (1996) (31)
Equality Elimination for the Tableau Method (1996) (30)
What You Always Wanted to Know about Rigid E-Unification (1996) (30)
AVATAR Modulo Theories (2016) (30)
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (2007) (30)
Decidability problems for the prenex fragment of intuitionistic logic (1996) (29)
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi (2001) (28)
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction (2001) (28)
A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering (2000) (27)
Finding Finite Models in Multi-Sorted First Order Logic (2016) (26)
Encoding industrial hardware verification problems into effectively propositional logic (2010) (25)
Comparing Unification Algorithms in First-Order Theorem Proving (2009) (24)
Generation of Hard Non-Clausal Random Satisfiability Problems (2005) (22)
Complexity of Query Answering in Logic Databases with Complex Values (1997) (22)
A Logical Reconstruction of Reachability (2003) (22)
Induction in Saturation-Based Proof Search (2019) (21)
A First Class Boolean Sort in First-Order Theorem Proving and TPTP (2015) (21)
Invariant and Type Inference for Matrices (2010) (21)
The Decidability of Simultaneous Rigid E-Unification with One Variable (1998) (20)
Herbrand's Theorem and Equational Reasoning: Problems and Solutions (2001) (20)
Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking (2002) (19)
Proof Systems for Effectively Propositional Logic (2008) (19)
Preprocessing techniques for first-order clausification (2012) (19)
A Clausal Normal Form Translation for FOOL (2016) (18)
Monadic Simultaneous Rigid E-Unification and Related Problems (1997) (18)
Extensional Crisis and Proving Identity (2014) (18)
The 481 Ways to Split a Clause and Deal with Propositional Variables (2013) (18)
BRAIN : Backward Reachability Analysis with Integers (2002) (17)
Solving Systems of Linear Inequalities by Bound Propagation (2011) (17)
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning (2017) (17)
A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees (1999) (17)
Induction with Generalization in Superposition Reasoning (2020) (16)
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (2001) (16)
Logic for Programming and Automated Reasoning (2002) (15)
Equality Elimination for the Inverse Method and Extension Procedures (1995) (15)
Case Studies on Invariant Generation Using a Saturation Theorem Prover (2011) (15)
Verifying equivalence of memories using a first order logic theorem prover (2009) (15)
Knuth--bendix constraint solving is NP-complete (2002) (14)
Proceedings of the 13th international conference on Logic for Programming, Artificial Intelligence, and Reasoning (2010) (14)
The Challenges of Evaluating a New Feature in Vampire (2016) (14)
Translating Regular Expression Matching into Transducers (2010) (14)
Stratified resolution (2000) (13)
Herbrand's theorem, automated reasoning and semantic tableaux (1998) (13)
KK: a theorem prover for K (1999) (13)
Partially Adaptive Code Trees (2000) (12)
K? : A theorem prover for K (1999) (12)
General Connections via Equality Elimination (1995) (12)
Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem (1999) (12)
Experimenting with SAT Solvers in Vampire (2014) (12)
Decidability and complexity of simultaneous rigid E-unification with one variable and related results (2000) (12)
On Transfinite Knuth-Bendix Orders (2011) (11)
Strategies in Rigid-Variable Methods (1997) (11)
Efficient instance retrieval with standard and relational path indexing (2005) (11)
EasyChair (2010) (11)
Reduction of Second-Order Unification to Simultaneous Rigid E-Unification (1995) (11)
A FOOLish Encoding of the Next State Relations of Imperative Programs (2018) (10)
A New Procedural Interpretation of Horn Clauses with Equality (1995) (10)
Automated Reasoning: Past Story and New Trends (2003) (10)
Planning with Effectively Propositional Logic (2013) (10)
Knuth-Bendix Constraint Solving Is NP-Complete (2001) (10)
Logic for Programming, Artificial Intelligence, and Reasoning (2013) (10)
Upper Bounds for a Theory of Queues (2003) (10)
Equality control methods in machine theorem proving (1986) (10)
An AC-Compatible Knuth-Bendix Order (2003) (9)
Proceedings of the 18th International Conference on Automated Deduction (2002) (9)
Keynote talk: EasyChair (2014) (9)
The Inverse Method for Many-Valued Logics (2013) (9)
Expressive power and data complexity of nonrecursive query languages for lists and trees (extended abstract) (2000) (9)
Efficient Checking of Term Ordering Constraints (2004) (9)
Declarative and Procedural Paradigms - Do they Really Compete? (Panel) (1991) (8)
EPR-Based Bounded Model Checking at Word Level (2012) (8)
First-Order Interpolation and Interpolating Proof Systems (2017) (8)
Expressive Power and Data Complexity of Query Languages for Trees and Lists (2000) (8)
Kanger’s Choices in Automated Reasoning (2001) (8)
A proof-search method for the first-order logic (1988) (8)
Vinter: A Vampire-Based Tool for Interpolation (2012) (8)
Implementing Bottom-up Procedures with Code Trees: a Case Study of Forward Subsumption (2020) (8)
Handling Equality in Logic Programming via Basic Folding (1996) (7)
Logic for Programming and Automated Reasoning (1999) (7)
Bound Propagation for Arithmetic Reasoning in Vampire (2013) (7)
Proceedings of the 7th international conference on Logic for programming and automated reasoning (1992) (7)
Cooperating Proof Attempts (2015) (7)
Complexity of Some Problems in Modal and Intuitionistic Calculi (2003) (6)
Logic Databases and the Meaning of Change (1996) (6)
A Construction of Typed Lambda Models Related to Feasible Computability (1993) (6)
Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (1998) (6)
Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications (2005) (6)
On Strong Normalization of the Calculus of Constructions with Type-Based Termination (2018) (5)
Implementing Conflict Resolution (2011) (5)
How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi (2000) (5)
Finding Basic Block and Variable Correspondence (2005) (5)
Current trends in theoretical computer science: entering the 21st centuary (2001) (5)
Instantiation and Pretending to be an SMT Solver with Vampire (2017) (5)
Adaptive Saturation-Based Reasoning (2001) (5)
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (1996) (5)
GoRRiLA and Hard Reality (2011) (4)
Encodings of Problems in Effectively Propositional Logic (2007) (4)
The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures (2002) (4)
Semantics of Constraint Logic Programs with Bounded Quantifiers (1996) (4)
Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings (2010) (4)
Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings (2008) (4)
Induction with Recursive Definitions in Superposition (2021) (4)
Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings (2005) (4)
Programming Logics (2013) (4)
Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings (2007) (4)
Inconsistencies in Ontologies (2006) (4)
Complexity of some problems in modal and superintuitionistic logics (2000) (4)
The ground-negative fragment of first-order logic is -complete (1999) (4)
Monadic Simultaneous Rigid E-unification (1999) (4)
HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday (2014) (4)
Logic programming and automated reasoning : 4th International Conference, LPAR '93, St. Petersburg, Russia, July 13-20, 1993 : proceedings (1993) (4)
Deductive Program Synthesis and Markov's Principle (1987) (4)
Deduction and applications (2006) (3)
Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (2010) (3)
Towards the Theory of Programming in Constructive Logic (1990) (3)
Logic for Programming, Artificial Intelligence, and Reasoning 9th International Conference, Lpar 2002, Tbilisi, Georgia, October 14-18, 2002 : Proceedings (2002) (3)
Proceedings of the First Russian Conference on Logic Programming (1990) (3)
A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers (1996) (3)
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (2017) (3)
Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings (2005) (3)
Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture) (2003) (3)
On connections between classical and constructive semantics (1990) (3)
Using Program Synthesis for Program Analysis (2018) (3)
Merging Relational Database Technology with Constraint Technology (1996) (3)
Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings (1992) (3)
Satisfiability and Theories (2009) (3)
Orienting equalities with the Knuth-Bendix order (2003) (3)
Automatic theorem proving. II (1987) (2)
On Completeness of Program Synthesis Systems (1991) (2)
Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012 (2012) (2)
Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008, Proceedings ... / Lecture Notes in Artificial Intelligence) (2008) (2)
Inter-program Properties (2009) (2)
Proceedings of the 19th international conference on Rewriting Techniques and Applications (2008) (2)
International Seminar on Logic Databases and the Meaning of Change, Transactions and Change in Logic Databases (1996) (2)
Automated deduction -- CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 : proceedings (2002) (2)
Logic for Programming, Artificial Intelligence, and Reasoning (2012) (2)
AVATAR : a new Architecture for First-Order Theorem Provers (2015) (2)
Proving Inter-Program Properties (2008) (2)
System Description: Vampire 1.0 (2000) (2)
Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings (2006) (2)
Proceedings of the Artificial Intelligence on Logic for Programming (2001) (2)
On computability by logic programs (1995) (2)
Implementation of UNIDOOR, a Deductive Object-Oriented Database System (2006) (2)
Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings (2007) (1)
Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers (2007) (1)
Logic for Programming, Artificial Intelligence, and Reasoning: 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings (2003) (1)
Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990 - Second Russian Conference on Logic Programming, St. Petersburg, Russia, September 11-16, 1991, Proceedings (1992) (1)
Logic programming and Σ-programming (1989) (1)
Handling Equality in Monodic Temporal Resolution (2013) (1)
Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers (2010) (1)
Perspectives of System Informatics: 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Novosibirsk, Russia, July 2–5, 2019, Revised Selected Papers (2019) (1)
LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations (2015) (1)
Perspectives of System Informatics (2014) (1)
Perspectives of System Informatics : 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (2016) (1)
Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers (2012) (1)
An Implementation Technique for a Class of Bottom-Up Procedures (1994) (1)
Proceedings of the 7th international Andrei Ershov Memorial conference on Perspectives of Systems Informatics (2006) (1)
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272) (2011) (1)
First-Order Theorem Provers: the Next Generation (2002) (1)
05431 Abstracts Collection - Deduction and Applications (2005) (1)
Deciding K using inverse-K (2000) (1)
Logic for Programming, Artificial Intelligence, and Reasoning 8th International Conference, Lpar 2001, Havana, Cuba, December 3-7, 2001 ; Proceedings (2001) (1)
Making Theory Reasoning Simpler (2021) (1)
UNIDOOR: a Deductive Object-Oriented Database Management System (2006) (1)
Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings (2012) (1)
First-Order Theorem Provers: the Next Generation (Extended Abstract) (2007) (0)
Proof-Search in Intui t ionis t ic Logic wi th Equality , or Back to S imul taneous Rigid E-Uni f i ca t ion (0)
Solving First-Order Constraints over the Monadic Class (2005) (0)
SMT Second-Order Principles in Speci cation Languages for Object-Oriented Programs (2006) (0)
10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware (2010) (0)
Harald Ganzinger's Legacy: Contributions to Logics and Programming (2013) (0)
Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015 (2016) (0)
PSI 2014. Ershov Informatics Conference, June 24-27, 2014, Peterhof, St. Petersburg, Russia, Poster Presentations (2014) (0)
Proceedings of the 2nd international symposium on Computer Science in Russia: Theory and Applications (2007) (0)
Higher Order Functions in First Order Theory (1992) (0)
LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings (2014) (0)
EasyChair Preprint No 826 Induction in Saturation-Based Proof Search (0)
The easychair Class File Documentation and Guide, for Authors and Editors (2010) (0)
Dagstuhl Report on Logic Databases and the Meaning of Change (2008) (0)
Enhancing model finding techniques for function-free logics (2006) (0)
Random Databases and Threshold for Monotone Non-recursive Datalog (2005) (0)
Deduction and Applications, 23.-28. October 2005 (2006) (0)
On the Evaluation of Indexing Te hniques forTheorem (2007) (0)
05431 Executive Summary - Deduction and Applications (2005) (0)
Programming Logics Group (2001) (0)
Expressive Power and Data Complexity of Nonrecursive Logic Programming (2000) (0)
Magically Constraining the Inverse Method Using Dynamic Polarity Assignment (2018) (0)
Logic for programming and automated reasoning : 7th International Conference, LPAR 2000, Reunion Island, France, November 6-10, 2000 : proceedings (2000) (0)
Short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta, Indonesia, October 10-15, 2010 (2013) (0)
Atomic Cut Introduction by Resolution Woltzenlogel Paleo 2 The CIRes Method (2019) (0)
The Vampire Approach to Induction (short paper) (2022) (0)
SAT solving experiments in Vampire (2016) (0)
Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning (2018) (0)
Program Semantics , Verification , and Construction (0)
Proceedings of the Second international conference on Computer Science: theory and applications (2007) (0)
Automatic theorem proving. I (1986) (0)
Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings (1999) (0)
Stratiied Resolution (2000) (0)
Equality Reasoning in Sequent-Based Methods, Volume 1 (2001) (0)
10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware (2010) (0)
Proceedings of the 8th international conference on Perspectives of System Informatics (2011) (0)
Max-planck-institut F Ur Informatik Complexity of Nonrecursive Logic Programs with Complex Values K I N F O R M a T I K We Thank (1997) (0)
Efficient Reasoning with Large Knowledge Bases (2005) (0)
A note on logical description, observational orders and minimum models (2014) (0)
6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014 (2014) (0)
The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable (2000) (0)
TOWARDS THE THEORY OF PROGRAHHING IN CONSTRUCTIVE LOGIC (2005) (0)

This paper list is powered by the following services:

Other Resources About Andrei Voronkov

What Schools Are Affiliated With Andrei Voronkov?

Andrei Voronkov is affiliated with the following schools:

Image Attributions

Image Source for Andrei Voronkov