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 |