Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndrei Voronkov
Person information
- affiliation: University of Manchester, UK
- affiliation: Chalmers University of Technology, Sweden
- award (2015): Herbrand Award
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Journal Articles
- 2012
[j23]Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov:
Translating regular expression matching into transducers. J. Appl. Log. 10(1): 32-51 (2012)- 2005
- [j22]Alexandre Riazanov, Andrei Voronkov:
Efficient instance retrieval with standard and relational path indexing. Inf. Comput. 199(1-2): 228-252 (2005) - [j21]Konstantin Korovin, Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete. ACM Trans. Comput. Log. 6(2): 361-388 (2005) - 2003
- [j20]Konstantin Korovin, Andrei Voronkov:
Orienting rewrite rules with the Knuth-Bendix order. Inf. Comput. 183(2): 165-186 (2003) - [j19]Andrei Voronkov:
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. J. Autom. Reason. 30(2): 121-151 (2003) - [j18]Anatoli Degtyarev, Robert Nieuwenhuis
, Andrei Voronkov:
Stratified resolution. J. Symb. Comput. 36(1-2): 79-99 (2003) - [j17]Alexandre Riazanov, Andrei Voronkov:
Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1-2): 101-115 (2003) - 2002
- [j16]Alexandre Riazanov, Andrei Voronkov:
The design and implementation of VAMPIRE. AI Commun. 15(2-3): 91-110 (2002) - 2001
- [j15]Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov:
Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3): 374-425 (2001) - [j14]Melvin Fitting, Lars Thalmann, Andrei Voronkov:
Term-Modal Logics. Stud Logica 69(1): 133-169 (2001) - [j13]Tatiana Rybina, Andrei Voronkov:
A decision procedure for term algebras with queues. ACM Trans. Comput. Log. 2(2): 155-181 (2001) - [j12]Andrei Voronkov:
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Trans. Comput. Log. 2(2): 182-215 (2001) - 2000
- [j11]Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov:
Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Theor. Comput. Sci. 243(1-2): 167-184 (2000) - 1999
- [j10]Andrei Voronkov:
The Ground-Negative Fragment of First-Order Logic Is Pip2-Complete. J. Symb. Log. 64(3): 984-990 (1999) - [j9]Yuri Gurevich, Andrei Voronkov:
Monadic Simultaneous Rigid E-unification. Theor. Comput. Sci. 222(1-2): 133-152 (1999) - [j8]Andrei Voronkov:
Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem. Theor. Comput. Sci. 224(1-2): 319-352 (1999) - 1998
- [j7]Anatoli Degtyarev, Andrei Voronkov:
What You Always Wanted to Know about Rigid E-Unification. J. Autom. Reason. 20(1): 47-80 (1998) - [j6]Andrei Voronkov:
Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. J. Autom. Reason. 21(2): 205-231 (1998) - 1996
- [j5]Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov:
Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Bull. EATCS 60: 78-96 (1996) - [j4]Anatoli Degtyarev, Andrei Voronkov:
A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers. J. Log. Program. 28(3): 207-216 (1996) - [j3]Anatoli Degtyarev, Andrei Voronkov:
The Undecidability of Simultaneous Rigid E-Unification. Theor. Comput. Sci. 166(1&2): 291-300 (1996) - 1995
- [j2]Andrei Voronkov:
On Computability by Logic Programs. Ann. Math. Artif. Intell. 15(3-4): 437-456 (1995) - [j1]Andrei Voronkov:
The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees. J. Autom. Reason. 15(2): 237-265 (1995)
Conference and Workshop Papers
- 2023
- [c147]Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov:
Program Synthesis in Saturation. CADE 2023: 307-324 - [c146]Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov:
ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) 2023: 647-665 - 2022
- [c145]Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov:
Getting Saturated with Induction. Principles of Systems Design 2022: 306-322 - [c144]Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov:
The Vampire Approach to Induction (short paper). PAAR@IJCAR 2022 - 2021
- [c143]Petra Hozzová, Laura Kovács, Andrei Voronkov:
Integer Induction in Saturation. CADE 2021: 361-377 - [c142]Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov:
Induction with Recursive Definitions in Superposition. FMCAD 2021: 1-10 - [c141]Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov:
Inductive Benchmarks for Automated Reasoning. CICM 2021: 124-129 - [c140]Giles Reger, Johannes Schoisswohl, Andrei Voronkov:
Making Theory Reasoning Simpler. TACAS (2) 2021: 164-180 - 2020
- [c139]Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov:
Induction with Generalization in Superposition Reasoning. CICM 2020: 123-137 - 2019
- [c138]Giles Reger, Andrei Voronkov:
Induction in Saturation-Based Proof Search. CADE 2019: 477-494 - 2018
- [c137]Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov:
A FOOLish Encoding of the Next State Relations of Imperative Programs. IJCAR 2018: 405-421 - [c136]Andrei Voronkov:
Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning. SYNASC 2018: 18 - [c135]Giles Reger, Martin Suda, Andrei Voronkov:
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS (1) 2018: 3-22 - 2017
- [c134]Laura Kovács, Andrei Voronkov:
First-Order Interpolation and Interpolating Proof Systems. LPAR 2017: 49-64 - [c133]Laura Kovács, Simon Robillard, Andrei Voronkov:
Coming to terms with quantified reasoning. POPL 2017: 260-270 - [c132]Giles Reger, Martin Suda, Andrei Voronkov:
Instantiation and Pretending to be an SMT Solver with Vampire. SMT 2017: 63-75 - [c131]Giles Reger, Martin Suda, Andrei Voronkov:
Testing a Saturation-Based Theorem Prover: Experiences and Challenges. TAP@STAF 2017: 152-161 - 2016
- [c130]Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov:
Selecting the Selection. IJCAR 2016: 313-329 - [c129]Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov:
The vampire and the FOOL. CPP 2016: 37-48 - [c128]Giles Reger, Martin Suda, Andrei Voronkov:
New Techniques in Clausal Form Generation. GCAI 2016: 11-23 - [c127]Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov:
AVATAR Modulo Theories. GCAI 2016: 39-52 - [c126]Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov:
A Clausal Normal Form Translation for FOOL. GCAI 2016: 53-71 - [c125]Giles Reger, Martin Suda, Andrei Voronkov:
Finding Finite Models in Multi-sorted First-Order Logic. SAT 2016: 323-341 - 2015
- [c124]Giles Reger, Dmitry Tishkovsky, Andrei Voronkov:
Cooperating Proof Attempts. CADE 2015: 339-355 - [c123]Giles Reger, Martin Suda, Andrei Voronkov:
Playing with AVATAR. CADE 2015: 399-415 - [c122]Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov:
A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CICM 2015: 71-86 - 2014
- [c121]Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov:
Extensional Crisis and Proving Identity. ATVA 2014: 185-200 - [c120]Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov:
SAT solving experiments in Vampire. Vampire Workshop 2014: 29-32 - [c119]Giles Reger, Martin Suda, Andrei Voronkov:
The Challenges of Evaluating a New Feature in Vampire. Vampire Workshop 2014: 70-74 - [c118]Andrei Voronkov:
AVATAR: The Architecture for First-Order Theorem Provers. CAV 2014: 696-710 - [c117]Andrei Voronkov:
Keynote talk: EasyChair. ASE 2014: 3-4 - [c116]Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov:
Experimenting with SAT Solvers in Vampire. MICAI (1) 2014: 431-442 - 2013
- [c115]Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm:
Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics 2013: 1-18 - [c114]Juan Antonio Navarro Pérez, Andrei Voronkov:
Planning with Effectively Propositional Logic. Programming Logics 2013: 302-316 - [c113]Krystof Hoder, Andrei Voronkov:
The 481 Ways to Split a Clause and Deal with Propositional Variables. CADE 2013: 450-464 - [c112]Laura Kovács, Andrei Voronkov:
First-Order Theorem Proving and Vampire. CAV 2013: 1-35 - [c111]Alexandru Constantin, Steve Pettifer, Andrei Voronkov:
PDFX: fully-automated PDF-to-XML conversion of scientific literature. ACM Symposium on Document Engineering 2013: 177-180 - [c110]Laura Kovács, Andrei Mantsivoda, Andrei Voronkov:
The Inverse Method for Many-Valued Logics. MICAI (1) 2013: 12-23 - [c109]Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov:
Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC 2013: 169-176 - 2012
- [c108]Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov:
Vinter: A Vampire-Based Tool for Interpolation. APLAS 2012: 148-156 - [c107]Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov:
EPR-Based Bounded Model Checking at Word Level. IJCAR 2012: 210-224 - [c106]Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov:
Preprocessing techniques for first-order clausification. FMCAD 2012: 44-51 - [c105]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Playing in the grey area of proofs. POPL 2012: 259-272 - 2011
- [c104]Krystof Hoder, Andrei Voronkov:
Sine Qua Non for Large Theory Reasoning. CADE 2011: 299-314 - [c103]Konstantin Korovin, Andrei Voronkov:
Solving Systems of Linear Inequalities by Bound Propagation. CADE 2011: 369-383 - [c102]Laura Kovács, Georg Moser, Andrei Voronkov:
On Transfinite Knuth-Bendix Orders. CADE 2011: 384-399 - [c101]Konstantin Korovin, Andrei Voronkov:
GoRRiLA and Hard Reality. Ershov Memorial Conference 2011: 243-250 - [c100]Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov:
Implementing Conflict Resolution. Ershov Memorial Conference 2011: 362-376 - [c99]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Case Studies on Invariant Generation Using a Saturation Theorem Prover. MICAI (1) 2011: 1-15 - [c98]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Invariant Generation in Vampire. TACAS 2011: 60-64 - 2010
- [c97]Krystof Hoder, Laura Kovács, Andrei Voronkov:
Interpolation and Symbol Elimination in Vampire. IJCAR 2010: 188-195 - [c96]Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov:
Encoding industrial hardware verification problems into effectively propositional logic. FMCAD 2010: 137-144 - [c95]Josef Urban, Krystof Hoder, Andrei Voronkov:
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. ICMS 2010: 155-166 - [c94]Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov:
Translating Regular Expression Matching into Transducers. SYNASC 2010: 107-115 - [c93]Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov:
Invariant and Type Inference for Matrices. VMCAI 2010: 163-179 - [c92]Andrei Voronkov:
EasyChair. WWV 2010: 2 - 2009
- [c91]Laura Kovács, Andrei Voronkov:
Interpolation and Symbol Elimination. CADE 2009: 199-213 - [c90]Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov:
Conflict Resolution. CP 2009: 509-523 - [c89]Laura Kovács, Andrei Voronkov:
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. FASE 2009: 470-485 - [c88]Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov:
Verifying equivalence of memories using a first order logic theorem prover. FMCAD 2009: 128-135 - [c87]Krystof Hoder, Andrei Voronkov:
Comparing Unification Algorithms in First-Order Theorem Proving. KI 2009: 435-443 - [c86]Andrei Voronkov, Iman Narasamdya:
Inter-program Properties. SAS 2009: 343-359 - [c85]Laura Kovács, Andrei Voronkov:
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. SYNASC 2009: 10 - [c84]Andrei Voronkov:
Satisfiability and Theories. SYNASC 2009: 16 - [c83]Nikolaj S. Bjørner, Nikolai Tillmann, Andrei Voronkov:
Path Feasibility Analysis for String-Manipulating Programs. TACAS 2009: 307-321 - 2008
- [c82]Juan Antonio Navarro Pérez, Andrei Voronkov:
Proof Systems for Effectively Propositional Logic. IJCAR 2008: 426-440 - 2007
- [c81]Juan Antonio Navarro Pérez, Andrei Voronkov:
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. CADE 2007: 346-361 - [c80]Konstantin Korovin, Andrei Voronkov:
Integrating Linear Arithmetic into Superposition Calculus. CSL 2007: 223-237 - [c79]Juan Antonio Navarro Pérez, Andrei Voronkov:
Encodings of Problems in Effectively Propositional Logic. SAT 2007: 3 - 2006
- [c78]Mohammed K. Jaber, Andrei Voronkov:
Implementation of UNIDOOR, a Deductive Object-Oriented Database System. ADBIS 2006: 155-170 - [c77]Ian Horrocks, Andrei Voronkov:
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. FoIKS 2006: 201-218 - [c76]Mohammed K. Jaber, Andrei Voronkov:
UNIDOOR: a Deductive Object-Oriented Database Management System. ICDE 2006: 157 - [c75]Andrei Voronkov:
Inconsistencies in Ontologies. JELIA 2006: 19 - 2005
- [c74]Juan Antonio Navarro Pérez, Andrei Voronkov:
Generation of Hard Non-Clausal Random Satisfiability Problems. AAAI 2005: 436-442 - [c73]Dimitri Chubarov, Andrei Voronkov:
Solving First-Order Constraints over the Monadic Class. Mechanizing Mathematical Reasoning 2005: 132-138 - [c72]Dimitri Chubarov, Andrei Voronkov:
Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. MFCS 2005: 260-270 - [c71]Konstantin Korovin, Andrei Voronkov:
Random Databases and Threshold for Monotone Non-recursive Datalog. MFCS 2005: 591-602 - [c70]Iman Narasamdya, Andrei Voronkov:
Finding Basic Block and Variable Correspondence. SAS 2005: 251-267 - 2004
- [c69]Alexandre Riazanov, Andrei Voronkov:
Efficient Checking of Term Ordering Constraints. IJCAR 2004: 60-74 - [c68]Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov:
TeMP: A Temporal Monodic Prover. IJCAR 2004: 326-330 - 2003
- [c67]Konstantin Korovin, Andrei Voronkov:
An AC-Compatible Knuth-Bendix Order. CADE 2003: 47-59 - [c66]Alexandre Riazanov, Andrei Voronkov:
Efficient Instance Retrieval with Standard and Relational Path Indexing. CADE 2003: 380-396 - [c65]Larisa Maksimova, Andrei Voronkov:
Complexity of Some Problems in Modal and Intuitionistic Calculi. CSL 2003: 397-412 - [c64]Tatiana Rybina, Andrei Voronkov:
Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture). CSL 2003: 546-573 - [c63]Tatiana Rybina, Andrei Voronkov:
A Logical Reconstruction of Reachability. Ershov Memorial Conference 2003: 222-237 - [c62]Tatiana Rybina, Andrei Voronkov:
Upper Bounds for a Theory of Queues. ICALP 2003: 714-724 - [c61]Andrei Voronkov:
Automated Reasoning: Past Story and New Trends. IJCAI 2003: 1607-1612 - [c60]Konstantin Korovin, Andrei Voronkov:
Orienting Equalities with the Knuth-Bendix Order. LICS 2003: 75- - 2002
- [c59]Tatiana Rybina, Andrei Voronkov:
BRAIN : Backward Reachability Analysis with Integers. AMAST 2002: 489-494 - [c58]Tatiana Rybina, Andrei Voronkov:
Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. CAV 2002: 386-400 - [c57]Andrei Voronkov:
First-Order Theorem Provers: the Next Generation. Description Logics 2002 - [c56]Konstantin Korovin, Andrei Voronkov:
The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. FSTTCS 2002: 230-240 - 2001
- [c55]Andrei Voronkov:
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. IJCAR 2001: 13-28 - [c54]Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov:
On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR 2001: 257-271 - [c53]Alexandre Riazanov, Andrei Voronkov:
Vampire 1.1 (System Description). IJCAR 2001: 376-380 - [c52]Alexandre Riazanov, Andrei Voronkov:
Adaptive Saturation-Based Reasoning. Ershov Memorial Conference 2001: 95-108 - [c51]Konstantin Korovin, Andrei Voronkov:
Knuth-Bendix Constraint Solving Is NP-Complete. ICALP 2001: 979-992 - [c50]Alexandre Riazanov, Andrei Voronkov:
Splitting Without Backtracking. IJCAI 2001: 611-617 - [c49]Konstantin Korovin, Andrei Voronkov:
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. RTA 2001: 137-153 - 2000
- [c48]Konstantin Korovin, Andrei Voronkov:
The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. ARW 2000 - [c47]Alexandre Riazanov, Andrei Voronkov:
System Description: Vampire 1.0. ARW 2000 - [c46]