Andrei Voronkov

Bing Citeseer DBLP Google Google Scholar Kosmix Wikipedia Yahoo!
Loading Google Thumbnails...
2012
125Playing in the grey area of proofs. Krystof Hoder, Laura Kovács, Andrei Voronkov. POPL 2012, 259-272. Web SearchBibTeXDownload
2011
124Solving Systems of Linear Inequalities by Bound Propagation. Konstantin Korovin, Andrei Voronkov. CADE 2011, 369-383. Web SearchBibTeXDownload
123On Transfinite Knuth-Bendix Orders. Laura Kovács, Georg Moser, Andrei Voronkov. CADE 2011, 384-399. Web SearchBibTeXDownload
122Sine Qua Non for Large Theory Reasoning. Krystof Hoder, Andrei Voronkov. CADE 2011, 299-314. Web SearchBibTeXDownload
121Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Nikolaj Bjřrner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov. Dagstuhl Reports (1): 23-35 (2011). Web SearchBibTeXDownload
120Case Studies on Invariant Generation Using a Saturation Theorem Prover. Krystof Hoder, Laura Kovács, Andrei Voronkov. MICAI (1) 2011, 1-15. Web SearchBibTeXDownload
119Invariant Generation in Vampire. Krystof Hoder, Laura Kovács, Andrei Voronkov. TACAS 2011, 60-64. Web SearchBibTeXDownload
2010
118Encoding industrial hardware verification problems into effectively propositional logic. Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov. FMCAD 2010, 137-144. Web SearchBibTeXDownload
117Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. Josef Urban, Krystof Hoder, Andrei Voronkov. ICMS 2010, 155-166. Web SearchBibTeXDownload
116Interpolation and Symbol Elimination in Vampire. Krystof Hoder, Laura Kovács, Andrei Voronkov. IJCAR 2010, 188-195. Web SearchBibTeXDownload
115Translating Regular Expression Matching into Transducers. Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov. SYNASC 2010, 107-115. Web SearchBibTeXDownload
114Invariant and Type Inference for Matrices. Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov. VMCAI 2010, 163-179. Web SearchBibTeXDownload
2009
113Interpolation and Symbol Elimination. Laura Kovács, Andrei Voronkov. CADE 2009, 199-213. Web SearchBibTeXDownload
112Conflict Resolution. Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov. CP 2009, 509-523. Web SearchBibTeXDownload
111Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. Laura Kovács, Andrei Voronkov. FASE 2009, 470-485. Web SearchBibTeXDownload
110Verifying equivalence of memories using a first order logic theorem prover. Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov. FMCAD 2009, 128-135. Web SearchBibTeXDownload
109Comparing Unification Algorithms in First-Order Theorem Proving. Krystof Hoder, Andrei Voronkov. KI 2009, 435-443. Web SearchBibTeXDownload
108Inter-program Properties. Andrei Voronkov, Iman Narasamdya. SAS 2009, 343-359. Web SearchBibTeXDownload
107Path Feasibility Analysis for String-Manipulating Programs. Nikolaj Bjřrner, Nikolai Tillmann, Andrei Voronkov. TACAS 2009, 307-321. Web SearchBibTeXDownload
2008
106Proof Systems for Effectively Propositional Logic. Juan Antonio Navarro Pérez, Andrei Voronkov. IJCAR 2008, 426-440. Web SearchBibTeXDownload
2007
105Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. Juan Antonio Navarro Pérez, Andrei Voronkov. CADE 2007, 346-361. Web SearchBibTeXDownload
104Integrating Linear Arithmetic into Superposition Calculus. Konstantin Korovin, Andrei Voronkov. CSL 2007, 223-237. Web SearchBibTeXDownload
103Encodings of Problems in Effectively Propositional Logic. Juan Antonio Navarro Pérez, Andrei Voronkov. SAT 2007, 3. Web SearchBibTeXDownload
2006
102Implementation of UNIDOOR, a Deductive Object-Oriented Database System. Mohammed K. Jaber, Andrei Voronkov. ADBIS 2006, 155-170. Web SearchBibTeXDownload
101Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. Ian Horrocks, Andrei Voronkov. FoIKS 2006, 201-218. Web SearchBibTeXDownload
100UNIDOOR: a Deductive Object-Oriented Database Management System. Mohammed K. Jaber, Andrei Voronkov. ICDE 2006, 157. Web SearchBibTeXDownload
99Inconsistencies in Ontologies. Andrei Voronkov. JELIA 2006, 19. Web SearchBibTeXDownload
2005
98Generation of Hard Non-Clausal Random Satisfiability Problems. Juan Antonio Navarro Pérez, Andrei Voronkov. AAAI 2005, 436-442. Web SearchBibTeX
97Knuth-Bendix constraint solving is NP-complete. Konstantin Korovin, Andrei Voronkov. ACM Trans. Comput. Log. (6): 361-388 (2005). Web SearchBibTeXDownload
9605431 Executive Summary - Deduction and Applications. Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov. Deduction and Applications 2005. Web SearchBibTeXDownload
9505431 Abstracts Collection - Deduction and Applications. Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov. Deduction and Applications 2005. Web SearchBibTeXDownload
94Efficient instance retrieval with standard and relational path indexing. Alexandre Riazanov, Andrei Voronkov. Inf. Comput. (199): 228-252 (2005). Web SearchBibTeXDownload
93Solving First-Order Constraints over the Monadic Class. Dimitri Chubarov, Andrei Voronkov. Mechanizing Mathematical Reasoning 2005, 132-138. Web SearchBibTeXDownload
92Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. Dimitri Chubarov, Andrei Voronkov. MFCS 2005, 260-270. Web SearchBibTeXDownload
91Random Databases and Threshold for Monotone Non-recursive Datalog. Konstantin Korovin, Andrei Voronkov. MFCS 2005, 591-602. Web SearchBibTeXDownload
90Finding Basic Block and Variable Correspondence. Iman Narasamdya, Andrei Voronkov. SAS 2005, 251-267. Web SearchBibTeXDownload
2004
89TeMP: A Temporal Monodic Prover. Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov. IJCAR 2004, 326-330. Web SearchBibTeXDownload
88Efficient Checking of Term Ordering Constraints. Alexandre Riazanov, Andrei Voronkov. IJCAR 2004, 60-74. Web SearchBibTeXDownload
2003
87An AC-Compatible Knuth-Bendix Order. Konstantin Korovin, Andrei Voronkov. CADE 2003, 47-59. Web SearchBibTeXDownload
86Efficient Instance Retrieval with Standard and Relational Path Indexing. Alexandre Riazanov, Andrei Voronkov. CADE 2003, 380-396. Web SearchBibTeXDownload
85Complexity of Some Problems in Modal and Intuitionistic Calculi. Larisa Maksimova, Andrei Voronkov. CSL 2003, 397-412. Web SearchBibTeXDownload
84Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture). Tatiana Rybina, Andrei Voronkov. CSL 2003, 546-573. Web SearchBibTeXDownload
83A Logical Reconstruction of Reachability. Tatiana Rybina, Andrei Voronkov. Ershov Memorial Conference 2003, 222-237. Web SearchBibTeXDownload
82Upper Bounds for a Theory of Queues. Tatiana Rybina, Andrei Voronkov. ICALP 2003, 714-724. Web SearchBibTeXDownload
81Automated Reasoning: Past Story and New Trends. Andrei Voronkov. IJCAI 2003, 1607-1612. Web SearchBibTeX
80Orienting rewrite rules with the Knuth-Bendix order. Konstantin Korovin, Andrei Voronkov. Inf. Comput. (183): 165-186 (2003). Web SearchBibTeXDownload
79Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. Andrei Voronkov. J. Autom. Reasoning (30): 121-151 (2003). Web SearchBibTeXDownload
78Limited resource strategy in resolution theorem proving. Alexandre Riazanov, Andrei Voronkov. J. Symb. Comput. (36): 101-115 (2003). Web SearchBibTeXDownload
77Stratified resolution. Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov. J. Symb. Comput. (36): 79-99 (2003). Web SearchBibTeXDownload
76Orienting Equalities with the Knuth-Bendix Order. Konstantin Korovin, Andrei Voronkov. LICS 2003, 75. Web SearchBibTeXDownload
2002
75The design and implementation of VAMPIRE. Alexandre Riazanov, Andrei Voronkov. AI Commun. (15): 91-110 (2002). Web SearchBibTeXDownload
74BRAIN : Backward Reachability Analysis with Integers. Tatiana Rybina, Andrei Voronkov. AMAST 2002, 489-494. Web SearchBibTeXDownload
73Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. Tatiana Rybina, Andrei Voronkov. CAV 2002, 386-400. Web SearchBibTeXDownload
72Knuth-Bendix constraint solving is NP-complete. Konstantin Korovin, Andrei Voronkov. CoRR (cs.LO/0207068) (2002). Web SearchBibTeXDownload
71The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. Konstantin Korovin, Andrei Voronkov. FSTTCS 2002, 230-240. Web SearchBibTeXDownload
2001
70Complexity and expressive power of logic programming. Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov. ACM Comput. Surv. (33): 374-425 (2001). Web SearchBibTeXDownload
69A decision procedure for term algebras with queues. Tatiana Rybina, Andrei Voronkov. ACM Trans. Comput. Log. (2): 155-181 (2001). Web SearchBibTeXDownload
68How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Andrei Voronkov. ACM Trans. Comput. Log. (2): 182-215 (2001). Web SearchBibTeXDownload
67Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov. Current Trends in Theoretical Computer Science 2001, 303-326. Web SearchBibTeX
66Adaptive Saturation-Based Reasoning. Alexandre Riazanov, Andrei Voronkov. Ershov Memorial Conference 2001, 95-108. Web SearchBibTeXDownload
65The Inverse Method. Anatoli Degtyarev, Andrei Voronkov. Handbook of Automated Reasoning 2001, 179-272. Web SearchBibTeX
64Equality Reasoning in Sequent-Based Calculi. Anatoli Degtyarev, Andrei Voronkov. Handbook of Automated Reasoning 2001, 611-706. Web SearchBibTeX
63Term Indexing. I. V. Ramakrishnan, R. C. Sekar, Andrei Voronkov. Handbook of Automated Reasoning 2001, 1853-1964. Web SearchBibTeX
62Knuth-Bendix Constraint Solving Is NP-Complete. Konstantin Korovin, Andrei Voronkov. ICALP 2001, 979-992. Web SearchBibTeXDownload
61Splitting Without Backtracking. Alexandre Riazanov, Andrei Voronkov. IJCAI 2001, 611-617. Web SearchBibTeX
60On the Evaluation of Indexing Techniques for Theorem Proving. Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov. IJCAR 2001, 257-271. Web SearchBibTeXDownload
59Vampire 1.1 (System Description). Alexandre Riazanov, Andrei Voronkov. IJCAR 2001, 376-380. Web SearchBibTeXDownload
58Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. Andrei Voronkov. IJCAR 2001, 13-28. Web SearchBibTeXDownload
57Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. Konstantin Korovin, Andrei Voronkov. RTA 2001, 137-153. Web SearchBibTeXDownload
56Term-Modal Logics. Melvin Fitting, Lars Thalmann, Andrei Voronkov. Studia Logica (69): 133-169 (2001). Web SearchBibTeXDownload
2000
55Stratified Resolution. Anatoli Degtyarev, Andrei Voronkov. CADE 2000, 365-384. Web SearchBibTeXDownload
54Partially Adaptive Code Trees. Alexandre Riazanov, Andrei Voronkov. JELIA 2000, 209-223. Web SearchBibTeXDownload
53Deciding K using inverse-K. Andrei Voronkov. KR 2000, 198-209. Web SearchBibTeX
52A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. Konstantin Korovin, Andrei Voronkov. LICS 2000, 291-302. Web SearchBibTeXDownload
51How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. Andrei Voronkov. LICS 2000, 401-412. Web SearchBibTeXDownload
50A Decision Procedure for Term Algebras with Queues. Tatiana Rybina, Andrei Voronkov. LICS 2000, 279-290. Web SearchBibTeXDownload
49Expressive Power and Data Complexity of Query Languages for Trees and Lists. Evgeny Dantsin, Andrei Voronkov. PODS 2000, 157-165. Web SearchBibTeX
48Term-Modal Logics. Melvin Fitting, Lars Thalmann, Andrei Voronkov. TABLEAUX 2000, 220-236. Web SearchBibTeXDownload
47Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov. Theor. Comput. Sci. (243): 167-184 (2000). Web SearchBibTeXDownload
1999
46KK: a theorem prover for K. Andrei Voronkov. CADE 1999, 383-387. Web SearchBibTeXDownload
45A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees. Evgeny Dantsin, Andrei Voronkov. FoSSaCS 1999, 180-196. Web SearchBibTeXDownload
44The Ground-Negative Fragment of First-Order Logic Is Pip2-Complete. Andrei Voronkov. J. Symb. Log. (64): 984-990 (1999). Web SearchBibTeXDownload
43Monadic Simultaneous Rigid E-unification. Yuri Gurevich, Andrei Voronkov. Theor. Comput. Sci. (222): 133-152 (1999). Web SearchBibTeXDownload
42Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem. Andrei Voronkov. Theor. Comput. Sci. (224): 319-352 (1999). Web SearchBibTeXDownload
1998
41Elimination of Equality via Transformation with Ordering Constraints. Leo Bachmair, Harald Ganzinger, Andrei Voronkov. CADE 1998, 175-190. Web SearchBibTeXDownload
40Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. Andrei Voronkov. J. Autom. Reasoning (21): 205-231 (1998). Web SearchBibTeXDownload
39What You Always Wanted to Know about Rigid E-Unification. Anatoli Degtyarev, Andrei Voronkov. J. Autom. Reasoning (20): 47-80 (1998). Web SearchBibTeXDownload
38Herbrand's Theorem, Automated Reasoning and Semantics Tableaux. Andrei Voronkov. LICS 1998, 252-263. Web SearchBibTeXDownload
37Complexity of Nonrecursive Logic Programs with Complex Values. Sergei G. Vorobyov, Andrei Voronkov. PODS 1998, 244-253. Web SearchBibTeX
36The Decidability of Simultaneous Rigid E-Unification with One Variable. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov. RTA 1998, 181-195. Web SearchBibTeXDownload
1997
35Monadic Simultaneous Rigid E-Unification and Related Problems. Yuri Gurevich, Andrei Voronkov. ICALP 1997, 154-165. Web SearchBibTeXDownload
34Complexity and Expressive Power of Logic Programming. Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov. IEEE Conference on Computational Complexity 1997, 82-101. Web SearchBibTeXDownload
33Strategies in Rigid-Variable Methods. Andrei Voronkov. IJCAI (1) 1997, 114-121. Web SearchBibTeX
32Complexity of Query Answering in Logic Databases with Complex Values. Evgeny Dantsin, Andrei Voronkov. LFCS 1997, 56-66. Web SearchBibTeXDownload
1996
31Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov. Bulletin of the EATCS (60): 78-96 (1996). Web SearchBibTeX
30Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. Andrei Voronkov. CADE 1996, 32-46. Web SearchBibTeXDownload
29Equality Elimination for the Tableau Method. Anatoli Degtyarev, Andrei Voronkov. DISCO 1996, 46-60. Web SearchBibTeXDownload
28Semantics of Constraint Logic Programs with Bounded Quantifiers. Martin Argenius, Andrei Voronkov. ELP 1996, 1-18. Web SearchBibTeXDownload
27Handling Equality in Logic Programming via Basic Folding. Anatoli Degtyarev, Andrei Voronkov. ELP 1996, 119-136. Web SearchBibTeXDownload
26Merging Relational Database Technology with Constraint Technology. Andrei Voronkov. Ershov Memorial Conference 1996, 409-419. Web SearchBibTeXDownload
25What You Always Wanted to Know About Rigid E-Unification. Anatoli Degtyarev, Andrei Voronkov. JELIA 1996, 50-69. Web SearchBibTeXDownload
24A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers. Anatoli Degtyarev, Andrei Voronkov. J. Log. Program. (28): 207-216 (1996). Web SearchBibTeXDownload
23Simultaneous E-Unification and Related Algorithmic Problems. Anatoli Degtyarev, Yuri Matiyasevich, Andrei Voronkov. LICS 1996, 494-502. Web SearchBibTeXDownload
22Decidability Problems for the Prenex Fragment of Intuitionistic Logic. Anatoli Degtyarev, Andrei Voronkov. LICS 1996, 503-512. Web SearchBibTeXDownload
21Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction. Andrei Voronkov. TABLEAUX 1996, 312-329. Web SearchBibTeXDownload
20The Undecidability of Simultaneous Rigid E-Unification. Anatoli Degtyarev, Andrei Voronkov. Theor. Comput. Sci. (166): 291-300 (1996). Web SearchBibTeXDownload
1995
19On Computability by Logic Programs. Andrei Voronkov. Ann. Math. Artif. Intell. (15): 437-456 (1995). Web SearchBibTeXDownload
18Simultaneous Regid E-Unification Is Undecidable. Anatoli Degtyarev, Andrei Voronkov. CSL 1995, 178-190. Web SearchBibTeXDownload
17A New Procedural Interpretation of Horn Clauses with Equality. Anatoli Degtyarev, Andrei Voronkov. ICLP 1995, 565-579. Web SearchBibTeX
16Equality Elimination for the Inverse Method and Extension Procedures. Anatoli Degtyarev, Andrei Voronkov. IJCAI 1995, 342-347. Web SearchBibTeX
15The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees. Andrei Voronkov. J. Autom. Reasoning (15): 237-265 (1995). Web SearchBibTeXDownload
14General Connections via Equality Elimination. Anatoli Degtyarev, Andrei Voronkov. WOCFAI 1995, 109-120. Web SearchBibTeX
1994
13An Implementation Technique for a Class of Bottom-Up Procedures. Andrei Voronkov. PLILP 1994, 147-164. Web SearchBibTeXDownload
1993
12A Construction of Typed Lambda Models Related to Feasible Computability. Vladimir Yu. Sazonov, Andrei Voronkov. Kurt Gödel Colloquium 1993, 301-312. Web SearchBibTeXDownload
1992
11Theorem Proving in Non-Standard Logics Based on the Inverse Method. Andrei Voronkov. CADE 1992, 648-662. Web SearchBibTeXDownload
10Higher Order Functions in First Order Theory. Andrei Voronkov. ISTCS 1992, 43-54. Web SearchBibTeXDownload
9On Computability by Logic Programs. Andrei Voronkov. Structural Complexity and Recursion-theoretic methods in Logic-Programming 1992, 165. Web SearchBibTeX
1991
8On Completeness of Program Synthesis Systems. Andrei Voronkov. CSL 1991, 411-418. Web SearchBibTeXDownload
7Declarative and Procedural Paradigms - Do they Really Compete? (Panel). Harold Boley, Micha Meier, Chris Moss, Michael M. Richter, Andrei Voronkov. PDK 1991, 383-398. Web SearchBibTeXDownload
6Logic Programming with Bounded Quantifiers. Andrei Voronkov. RCLP 1991, 486-514. Web SearchBibTeXDownload
1990
5LISS - The Logic Inference Search System. Andrei Voronkov. CADE 1990, 677-678. Web SearchBibTeXDownload
4Towards the Theory of Programming in Constructive Logic. Andrei Voronkov. ESOP 1990, 421-435. Web SearchBibTeXDownload
1988
3A proof-search method for the first-order logic. Andrei Voronkov. Conference on Computer Logic 1988, 327-338. Web SearchBibTeXDownload
2On connections between classical and constructive semantics. Sergei Starchenko, Andrei Voronkov. Conference on Computer Logic 1988, 275-285. Web SearchBibTeXDownload
1987
1Deductive Program Synthesis and Markov's Principle. Andrei Voronkov. FCT 1987, 479-482. Web SearchBibTeXDownload
from DBLP and Google Scholar
Developed by the Database Group at the University of Wisconsin and Yahoo! Research