| 2009 |
| 130 | EE | Laura Kovács,
Andrei Voronkov:
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover.
FASE 2009: 470-485 |
| 129 | EE | Nikolaj Bjørner,
Nikolai Tillmann,
Andrei Voronkov:
Path Feasibility Analysis for String-Manipulating Programs.
TACAS 2009: 307-321 |
| 2008 |
| 128 | | Andrei Voronkov:
Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings
Springer 2008 |
| 127 | | Iliano Cervesato,
Helmut Veith,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings
Springer 2008 |
| 126 | EE | Juan Antonio Navarro Pérez,
Andrei Voronkov:
Proof Systems for Effectively Propositional Logic.
IJCAR 2008: 426-440 |
| 2007 |
| 125 | | Irina Virbitskaite,
Andrei Voronkov:
Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers
Springer 2007 |
| 124 | | Volker Diekert,
Mikhail V. Volkov,
Andrei Voronkov:
Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings
Springer 2007 |
| 123 | | Nachum Dershowitz,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings
Springer 2007 |
| 122 | EE | Juan Antonio Navarro Pérez,
Andrei Voronkov:
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic.
CADE 2007: 346-361 |
| 121 | EE | Konstantin Korovin,
Andrei Voronkov:
Integrating Linear Arithmetic into Superposition Calculus.
CSL 2007: 223-237 |
| 120 | EE | Juan Antonio Navarro Pérez,
Andrei Voronkov:
Encodings of Problems in Effectively Propositional Logic.
SAT 2007: 3 |
| 2006 |
| 119 | | Franz Baader,
Peter Baumgartner,
Robert Nieuwenhuis,
Andrei Voronkov:
Deduction and Applications, 23.-28. October 2005
Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006 |
| 118 | | Miki Hermann,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings
Springer 2006 |
| 117 | EE | Mohammed K. Jaber,
Andrei Voronkov:
Implementation of UNIDOOR, a Deductive Object-Oriented Database System.
ADBIS 2006: 155-170 |
| 116 | EE | Ian Horrocks,
Andrei Voronkov:
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.
FoIKS 2006: 201-218 |
| 115 | EE | Mohammed K. Jaber,
Andrei Voronkov:
UNIDOOR: a Deductive Object-Oriented Database Management System.
ICDE 2006: 157 |
| 114 | EE | Andrei Voronkov:
Inconsistencies in Ontologies.
JELIA 2006: 19 |
| 2005 |
| 113 | | Franz Baader,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings
Springer 2005 |
| 112 | | Geoff Sutcliffe,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings
Springer 2005 |
| 111 | | Juan Antonio Navarro Pérez,
Andrei Voronkov:
Generation of Hard Non-Clausal Random Satisfiability Problems.
AAAI 2005: 436-442 |
| 110 | EE | Franz Baader,
Peter Baumgartner,
Robert Nieuwenhuis,
Andrei Voronkov:
05431 Abstracts Collection - Deduction and Applications.
Deduction and Applications 2005 |
| 109 | EE | Franz Baader,
Peter Baumgartner,
Robert Nieuwenhuis,
Andrei Voronkov:
05431 Executive Summary - Deduction and Applications.
Deduction and Applications 2005 |
| 108 | EE | Dimitri Chubarov,
Andrei Voronkov:
Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications.
MFCS 2005: 260-270 |
| 107 | EE | Konstantin Korovin,
Andrei Voronkov:
Random Databases and Threshold for Monotone Non-recursive Datalog.
MFCS 2005: 591-602 |
| 106 | EE | Dimitri Chubarov,
Andrei Voronkov:
Solving First-Order Constraints over the Monadic Class.
Mechanizing Mathematical Reasoning 2005: 132-138 |
| 105 | EE | Iman Narasamdya,
Andrei Voronkov:
Finding Basic Block and Variable Correspondence.
SAS 2005: 251-267 |
| 104 | EE | Konstantin Korovin,
Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete.
ACM Trans. Comput. Log. 6(2): 361-388 (2005) |
| 103 | EE | Alexandre Riazanov,
Andrei Voronkov:
Efficient instance retrieval with standard and relational path indexing.
Inf. Comput. 199(1-2): 228-252 (2005) |
| 2004 |
| 102 | EE | Ullrich Hustadt,
Boris Konev,
Alexandre Riazanov,
Andrei Voronkov:
TeMP: A Temporal Monodic Prover.
IJCAR 2004: 326-330 |
| 101 | EE | Alexandre Riazanov,
Andrei Voronkov:
Efficient Checking of Term Ordering Constraints.
IJCAR 2004: 60-74 |
| 2003 |
| 100 | | Moshe Y. Vardi,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings
Springer 2003 |
| 99 | EE | Alexandre Riazanov,
Andrei Voronkov:
Efficient Instance Retrieval with Standard and Relational Path Indexing.
CADE 2003: 380-396 |
| 98 | EE | Konstantin Korovin,
Andrei Voronkov:
An AC-Compatible Knuth-Bendix Order.
CADE 2003: 47-59 |
| 97 | EE | Larisa Maksimova,
Andrei Voronkov:
Complexity of Some Problems in Modal and Intuitionistic Calculi.
CSL 2003: 397-412 |
| 96 | EE | Tatiana Rybina,
Andrei Voronkov:
Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture).
CSL 2003: 546-573 |
| 95 | EE | Tatiana Rybina,
Andrei Voronkov:
A Logical Reconstruction of Reachability.
Ershov Memorial Conference 2003: 222-237 |
| 94 | EE | Tatiana Rybina,
Andrei Voronkov:
Upper Bounds for a Theory of Queues.
ICALP 2003: 714-724 |
| 93 | | Andrei Voronkov:
Automated Reasoning: Past Story and New Trends.
IJCAI 2003: 1607-1612 |
| 92 | EE | Konstantin Korovin,
Andrei Voronkov:
Orienting Equalities with the Knuth-Bendix Order.
LICS 2003: 75- |
| 91 | EE | Konstantin Korovin,
Andrei Voronkov:
Orienting rewrite rules with the Knuth-Bendix order.
Inf. Comput. 183(2): 165-186 (2003) |
| 90 | | Andrei Voronkov:
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.
J. Autom. Reasoning 30(2): 121-151 (2003) |
| 89 | EE | Alexandre Riazanov,
Andrei Voronkov:
Limited resource strategy in resolution theorem proving.
J. Symb. Comput. 36(1-2): 101-115 (2003) |
| 88 | EE | Anatoli Degtyarev,
Robert Nieuwenhuis,
Andrei Voronkov:
Stratified resolution.
J. Symb. Comput. 36(1-2): 79-99 (2003) |
| 2002 |
| 87 | | Andrei Voronkov:
Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings
Springer 2002 |
| 86 | | Matthias Baaz,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings
Springer 2002 |
| 85 | EE | Tatiana Rybina,
Andrei Voronkov:
BRAIN : Backward Reachability Analysis with Integers.
AMAST 2002: 489-494 |
| 84 | EE | Tatiana Rybina,
Andrei Voronkov:
Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking.
CAV 2002: 386-400 |
| 83 | EE | 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 |
| 82 | EE | Alexandre Riazanov,
Andrei Voronkov:
The design and implementation of VAMPIRE.
AI Commun. 15(2-3): 91-110 (2002) |
| 81 | EE | Konstantin Korovin,
Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete
CoRR cs.LO/0207068: (2002) |
| 2001 |
| 80 | | John Alan Robinson,
Andrei Voronkov:
Handbook of Automated Reasoning (in 2 volumes)
Elsevier and MIT Press 2001 |
| 79 | | Robert Nieuwenhuis,
Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings
Springer 2001 |
| 78 | EE | Alexandre Riazanov,
Andrei Voronkov:
Adaptive Saturation-Based Reasoning.
Ershov Memorial Conference 2001: 95-108 |
| 77 | EE | Konstantin Korovin,
Andrei Voronkov:
Knuth-Bendix Constraint Solving Is NP-Complete.
ICALP 2001: 979-992 |
| 76 | | Alexandre Riazanov,
Andrei Voronkov:
Splitting Without Backtracking.
IJCAI 2001: 611-617 |
| 75 | EE | Andrei Voronkov:
Algorithms, Datastructures, and other Issues in Efficient Automated Deduction.
IJCAR 2001: 13-28 |
| 74 | EE | Robert Nieuwenhuis,
Thomas Hillenbrand,
Alexandre Riazanov,
Andrei Voronkov:
On the Evaluation of Indexing Techniques for Theorem Proving.
IJCAR 2001: 257-271 |
| 73 | EE | Alexandre Riazanov,
Andrei Voronkov:
Vampire 1.1 (System Description).
IJCAR 2001: 376-380 |
| 72 | EE | Konstantin Korovin,
Andrei Voronkov:
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.
RTA 2001: 137-153 |
| 71 | | Anatoli Degtyarev,
Yuri Gurevich,
Andrei Voronkov:
Herbrand's Theorem and Equational Reasoning: Problems and Solutions.
Current Trends in Theoretical Computer Science 2001: 303-326 |
| 70 | | Anatoli Degtyarev,
Andrei Voronkov:
The Inverse Method.
Handbook of Automated Reasoning 2001: 179-272 |
| 69 | | Anatoli Degtyarev,
Andrei Voronkov:
Equality Reasoning in Sequent-Based Calculi.
Handbook of Automated Reasoning 2001: 611-706 |
| 68 | | John Alan Robinson,
Andrei Voronkov:
Preface.
Handbook of Automated Reasoning 2001 |
| 67 | | I. V. Ramakrishnan,
R. C. Sekar,
Andrei Voronkov:
Term Indexing.
Handbook of Automated Reasoning 2001: 1853-1964 |
| 66 | EE | Evgeny Dantsin,
Thomas Eiter,
Georg Gottlob,
Andrei Voronkov:
Complexity and expressive power of logic programming.
ACM Comput. Surv. 33(3): 374-425 (2001) |
| 65 | EE | Tatiana Rybina,
Andrei Voronkov:
A decision procedure for term algebras with queues.
ACM Trans. Comput. Log. 2(2): 155-181 (2001) |
| 64 | EE | 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) |
| 63 | | Melvin Fitting,
Lars Thalmann,
Andrei Voronkov:
Term-Modal Logics.
Studia Logica 69(1): 133-169 (2001) |
| 2000 |
| 62 | | Michel Parigot,
Andrei Voronkov:
Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings
Springer 2000 |
| 61 | | Anatoli Degtyarev,
Andrei Voronkov:
Stratified Resolution.
CADE 2000: 365-384 |
| 60 | EE | Alexandre Riazanov,
Andrei Voronkov:
Partially Adaptive Code Trees.
JELIA 2000: 209-223 |
| 59 | | Andrei Voronkov:
Deciding K using inverse-K.
KR 2000: 198-209 |
| 58 | EE | Tatiana Rybina,
Andrei Voronkov:
A Decision Procedure for Term Algebras with Queues.
LICS 2000: 279-290 |
| 57 | EE | Konstantin Korovin,
Andrei Voronkov:
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.
LICS 2000: 291-302 |
| 56 | EE | Andrei Voronkov:
How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi.
LICS 2000: 401-412 |
| 55 | EE | Evgeny Dantsin,
Andrei Voronkov:
Expressive Power and Data Complexity of Query Languages for Trees and Lists.
PODS 2000: 157-165 |
| 54 | | Melvin Fitting,
Lars Thalmann,
Andrei Voronkov:
Term-Modal Logics.
TABLEAUX 2000: 220-236 |
| 53 | EE | 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 |
| 52 | | Harald Ganzinger,
David A. McAllester,
Andrei Voronkov:
Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings
Springer 1999 |
| 51 | EE | Alexandre Riazanov,
Andrei Voronkov:
Vampire.
CADE 1999: 292-296 |
| 50 | EE | Andrei Voronkov:
KK: a theorem prover for K.
CADE 1999: 383-387 |
| 49 | | Evgeny Dantsin,
Andrei Voronkov:
A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees.
FoSSaCS 1999: 180-196 |
| 48 | | Andrei Voronkov:
The Ground-Negative Fragment of First-Order Logic Is Pip2-Complete.
J. Symb. Log. 64(3): 984-990 (1999) |
| 47 | EE | Yuri Gurevich,
Andrei Voronkov:
Monadic Simultaneous Rigid E-unification.
Theor. Comput. Sci. 222(1-2): 133-152 (1999) |
| 46 | EE | 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 |
| 45 | | Burkhard Freitag,
Hendrik Decker,
Michael Kifer,
Andrei Voronkov:
Transactions and Change in Logic Databases, International Seminar on Logic Databases and the Meaning of Change, Schloss Dagstuhl, Germany, September 23-27, 1996 and ILPS '97 Post-Conference Workshop on (Trans)Actions and Change in Logic Programming and Deductive Databases, (DYNAMICS'97) Port Jefferson, NY, USA, October 17, 1997, Invited Surveys and Selected Papers
Springer 1998 |
| 44 | EE | Leo Bachmair,
Harald Ganzinger,
Andrei Voronkov:
Elimination of Equality via Transformation with Ordering Constraints.
CADE 1998: 175-190 |
| 43 | | Andrei Voronkov:
Herbrand's Theorem, Automated Reasoning and Semantics Tableaux.
LICS 1998: 252-263 |
| 42 | EE | Sergei G. Vorobyov,
Andrei Voronkov:
Complexity of Nonrecursive Logic Programs with Complex Values.
PODS 1998: 244-253 |
| 41 | EE | Anatoli Degtyarev,
Yuri Gurevich,
Paliath Narendran,
Margus Veanes,
Andrei Voronkov:
The Decidability of Simultaneous Rigid E-Unification with One Variable.
RTA 1998: 181-195 |
| 40 | | Anatoli Degtyarev,
Andrei Voronkov:
What You Always Wanted to Know about Rigid E-Unification.
J. Autom. Reasoning 20(1): 47-80 (1998) |
| 39 | | Andrei Voronkov:
Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.
J. Autom. Reasoning 21(2): 205-231 (1998) |
| 1997 |
| 38 | | Yuri Gurevich,
Andrei Voronkov:
Monadic Simultaneous Rigid E-Unification and Related Problems.
ICALP 1997: 154-165 |
| 37 | EE | Evgeny Dantsin,
Thomas Eiter,
Georg Gottlob,
Andrei Voronkov:
Complexity and Expressive Power of Logic Programming.
IEEE Conference on Computational Complexity 1997: 82-101 |
| 36 | | Andrei Voronkov:
Strategies in Rigid-Variable Methods.
IJCAI (1) 1997: 114-121 |
| 35 | | Evgeny Dantsin,
Andrei Voronkov:
Complexity of Query Answering in Logic Databases with Complex Values.
LFCS 1997: 56-66 |
| 1996 |
| 34 | | Andrei Voronkov:
Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.
CADE 1996: 32-46 |
| 33 | | Anatoli Degtyarev,
Andrei Voronkov:
Equality Elimination for the Tableau Method.
DISCO 1996: 46-60 |
| 32 | | Martin Argenius,
Andrei Voronkov:
Semantics of Constraint Logic Programs with Bounded Quantifiers.
ELP 1996: 1-18 |
| 31 | | Anatoli Degtyarev,
Andrei Voronkov:
Handling Equality in Logic Programming via Basic Folding.
ELP 1996: 119-136 |
| 30 | | Andrei Voronkov:
Merging Relational Database Technology with Constraint Technology.
Ershov Memorial Conference 1996: 409-419 |
| 29 | | Anatoli Degtyarev,
Andrei Voronkov:
What You Always Wanted to Know About Rigid E-Unification.
JELIA 1996: 50-69 |
| 28 | | Anatoli Degtyarev,
Yuri Matiyasevich,
Andrei Voronkov:
Simultaneous E-Unification and Related Algorithmic Problems.
LICS 1996: 494-502 |
| 27 | | Anatoli Degtyarev,
Andrei Voronkov:
Decidability Problems for the Prenex Fragment of Intuitionistic Logic.
LICS 1996: 503-512 |
| 26 | | Andrei Voronkov:
Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction.
TABLEAUX 1996: 312-329 |
| 25 | | Anatoli Degtyarev,
Yuri Gurevich,
Andrei Voronkov:
Herbrand's Theorem and Equational Reasoning: Problems and Solutions.
Bulletin of the EATCS 60: 78-96 (1996) |
| 24 | | 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) |
| 23 | EE | Anatoli Degtyarev,
Andrei Voronkov:
The Undecidability of Simultaneous Rigid E-Unification.
Theor. Comput. Sci. 166(1&2): 291-300 (1996) |
| 1995 |
| 22 | | Anatoli Degtyarev,
Andrei Voronkov:
Simultaneous Regid E-Unification Is Undecidable.
CSL 1995: 178-190 |
| 21 | | Anatoli Degtyarev,
Andrei Voronkov:
A New Procedural Interpretation of Horn Clauses with Equality.
ICLP 1995: 565-579 |
| 20 | | Anatoli Degtyarev,
Andrei Voronkov:
Equality Elimination for the Inverse Method and Extension Procedures.
IJCAI 1995: 342-347 |
| 19 | | Anatoli Degtyarev,
Andrei Voronkov:
General Connections via Equality Elimination.
WOCFAI 1995: 109-120 |
| 18 | | Andrei Voronkov:
On Computability by Logic Programs.
Ann. Math. Artif. Intell. 15(3-4): 437-456 (1995) |
| 17 | | Andrei Voronkov:
The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees.
J. Autom. Reasoning 15(2): 237-265 (1995) |
| 1994 |
| 16 | | Andrei Voronkov:
An Implementation Technique for a Class of Bottom-Up Procedures.
PLILP 1994: 147-164 |
| 1993 |
| 15 | | Andrei Voronkov:
Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings
Springer 1993 |
| 14 | | Vladimir Yu. Sazonov,
Andrei Voronkov:
A Construction of Typed Lambda Models Related to Feasible Computability.
Kurt Gödel Colloquium 1993: 301-312 |
| 1992 |
| 13 | | Andrei Voronkov:
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
Springer 1992 |
| 12 | | Andrei Voronkov:
Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings
Springer 1992 |
| 11 | | Andrei Voronkov:
Theorem Proving in Non-Standard Logics Based on the Inverse Method.
CADE 1992: 648-662 |
| 10 | | Andrei Voronkov:
Higher Order Functions in First Order Theory.
ISTCS 1992: 43-54 |
| 9 | | Andrei Voronkov:
On Computability by Logic Programs.
Structural Complexity and Recursion-theoretic methods in Logic-Programming 1992: 165- |
| 1991 |
| 8 | | Andrei Voronkov:
On Completeness of Program Synthesis Systems.
CSL 1991: 411-418 |
| 7 | | Harold Boley,
Micha Meier,
Chris Moss,
Michael M. Richter,
Andrei Voronkov:
Declarative and Procedural Paradigms - Do they Really Compete? (Panel).
PDK 1991: 383-398 |
| 6 | | Andrei Voronkov:
Logic Programming with Bounded Quantifiers.
RCLP 1991: 486-514 |
| 1990 |
| 5 | | Andrei Voronkov:
LISS - The Logic Inference Search System.
CADE 1990: 677-678 |
| 4 | | Andrei Voronkov:
Towards the Theory of Programming in Constructive Logic.
ESOP 1990: 421-435 |
| 1988 |
| 3 | | Sergei Starchenko,
Andrei Voronkov:
On connections between classical and constructive semantics.
Conference on Computer Logic 1988: 275-285 |
| 2 | | Andrei Voronkov:
A proof-search method for the first-order logic.
Conference on Computer Logic 1988: 327-338 |
| 1987 |
| 1 | | Andrei Voronkov:
Deductive Program Synthesis and Markov's Principle.
FCT 1987: 479-482 |