Edit Profile (opens in new tab) Voronkov, Andrei Compute Distance To: Compute Author ID: voronkov.andrei Published as: Voronkov, Andrei; Voronkov, A. Documents Indexed: 99 Publications since 1992 30 Contributions as Editor Co-Authors: 75 Co-Authors with 107 Joint Publications 2,004 Co-Co-Authors all top 5 Co-Authors 20 single-authored 13 Korovin, Konstantin 13 Kovács, Laura Ildikó 12 Degtyarev, Anatoli Ivanovich 9 Riazanov, Alexandre 8 Reger, Giles 6 Gurevich, Yuri 6 Hoder, Kryštof 5 Rybina, Tatiana 5 Suda, Martin 4 Nieuwenhuis, Robert 4 Virbitskaite, Irina B. 3 Hozzová, Petra 3 Schoisswohl, Johannes 2 Bjørner, Nikolaj S. 2 Chubarov, Dmitri Leonidovich 2 Clarke, Edmund Melson jun. 2 Dantsin, Evgeny 2 Fitting, Melvin Chris 2 Ganzinger, Harald 2 Hajdú, Márton 2 Kotel’nikov, Evgeny A. 2 Narasamdya, Iman 2 Narendran, Paliath 2 Pérez, Juan Antonio Navarro 2 Thalmann, Lars 2 Tsiskaridze, Nestan 2 Veanes, Margus 2 Weidenbach, Christoph 1 Baader, Franz 1 Baaz, Matthias 1 Bachmair, Leo 1 Cervesato, Iliano 1 Davis, Martin David 1 Decker, Hendrik 1 Dershowitz, Nachum 1 Diekert, Volker 1 Emmer, Moshe 1 Fehnker, Ansgar 1 Fermüller, Christian G. 1 Freitag, Burkhard 1 Gupta, Ashutosh 1 Henzinger, Thomas A. 1 Hermann, Miki 1 Hillenbrand, Thomas 1 Horrocks, Ian 1 Hottelier, Thibaud 1 Hustadt, Ullrich 1 Kapur, Deepak 1 Khasidashvili, Zurab O. 1 Kifer, Michael 1 Konev, Boris 1 Kragl, Bernhard 1 Maksimova, Larisa L’vovna 1 Mazzara, Manuel 1 McAllester, David Allen 1 McIver, Annabelle K. 1 McMillan, Kenneth L. 1 Middeldorp, Aart 1 Minamide, Yasuhiko 1 Moser, Georg 1 Navarro, Juan Antonio 1 Parigot, Michel 1 Petrenko, Alexander K. 1 Pnueli, Amir 1 Ramakrishnan, I. V. 1 Robillard, Simon 1 Sakuma, Yuto 1 Sazonov, Vladimir Yu. 1 Sekar, R. Chandra Guru 1 Sticksel, Christoph 1 Sutcliffe, Geoff 1 Tillmann, Nikolai 1 Tishkovsky, Dmitry 1 Urban, Josef 1 Vardi, Moshe Ya’akov 1 Veith, Helmut 1 Volkov, Mikhail Vladimirovich 1 Wilhelm, Reinhard all top 5 Serials 29 Lecture Notes in Computer Science 4 Theoretical Computer Science 4 Journal of Automated Reasoning 3 ACM Transactions on Computational Logic 2 Journal of Symbolic Computation 2 Information and Computation 1 The Journal of Symbolic Logic 1 Studia Logica 1 The Journal of Logic Programming 1 Bulletin of the European Association for Theoretical Computer Science (EATCS) 1 AI Communications 1 Annals of Mathematics and Artificial Intelligence 1 Reports of Enlarged Sessions of the Seminar of I. Vekua Institute of Applied Mathematics 1 Journal of Applied Logic all top 5 Fields 114 Computer science (68-XX) 64 Mathematical logic and foundations (03-XX) 30 General and overarching topics; collections (00-XX) 3 Linear and multilinear algebra; matrix theory (15-XX) 2 Operations research, mathematical programming (90-XX) 1 History and biography (01-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 89 Publications have been cited 574 times in 372 Documents Cited by ▼ Year ▼ The design and implementation of VAMPIRE. Zbl 1021.68082Riazanov, Alexandre; Voronkov, Andrei 69 2002 Handbook of automated reasoning. In 2 vols. Zbl 0964.00020 45 2001 Term indexing. Zbl 0992.68189Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei 30 2001 Sine qua non for large theory reasoning. Zbl 1341.68189Hoder, Kryštof; Voronkov, Andrei 26 2011 Interpolation and symbol elimination. Zbl 1250.68193Kovács, Laura; Voronkov, Andrei 19 2009 Path feasibility analysis for string-manipulating programs. Zbl 1234.68070Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei 18 2009 The undecidability of simultaneous rigid E-unification. Zbl 0872.68173Degtyarev, Anatoli; Voronkov, Andrei 18 1996 Interpolation and symbol elimination in Vampire. Zbl 1291.68348Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei 14 2010 Integrating linear arithmetic into superposition calculus. Zbl 1179.03018Korovin, Konstantin; Voronkov, Andrei 14 2007 The anatomy of vampire. Implementing bottom-up procedures with code trees. Zbl 0838.68100Voronkov, Andrei 14 1995 Term-modal logics. Zbl 0992.03026Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei 13 2001 Playing with AVATAR. Zbl 1465.68295Reger, Giles; Suda, Martin; Voronkov, Andrei 13 2015 Limited resource strategy in resolution theorem proving. Zbl 1023.68089Riazanov, Alexandre; Voronkov, Andrei 13 2003 Equality reasoning in sequent-based calculi. Zbl 1011.03004Degtyarev, Anatoli; Voronkov, Andrei 12 2001 AVATAR: the architecture for first-order theorem provers. Zbl 1495.68240Voronkov, Andrei 12 2014 Vampire 1. 1 (system description). Zbl 0988.68607Riazanov, Alexandre; Voronkov, Andrei 11 2001 Proof systems for effectively propositional logic. Zbl 1165.03318Navarro, Juan Antonio; Voronkov, Andrei 10 2008 TeMP: A temporal monodic prover. Zbl 1126.68568Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei 10 2004 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128Urban, Josef; Hoder, Krystof; Voronkov, Andrei 10 2010 The inverse method. Zbl 0992.03016Degtyarev, Anatoli; Voronkov, Andrei 10 2001 A decision procedure for term algebras with queues. Zbl 1171.68557Rybina, Tatiana; Voronkov, Andrei 10 2001 Selecting the selection. Zbl 1475.68436Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei 9 2016 What you always wanted to know about rigid \(E\)-unification. Zbl 0893.68135Degtyarev, Anatoli; Voronkov, Andrei 9 1998 A logical reconstruction of reachability. Zbl 1254.68153Rybina, Tatiana; Voronkov, Andrei 8 2003 Playing in the grey area of proofs. Zbl 1321.68196Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei 8 2012 Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079Korovin, Konstantin; Voronkov, Andrei 8 2003 Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Zbl 0944.68103Degtyarev, A.; Gurevich, Y.; Narendran, P.; Veanes, M.; Voronkov, A. 7 2000 Coming to terms with quantified reasoning. Zbl 1380.68280Kovács, Laura; Robillard, Simon; Voronkov, Andrei 7 2017 Monadic simultaneous rigid \(E\)-unification and related problems. Zbl 1401.03037Gurevich, Yuri; Voronkov, Andrei 7 1997 Conflict resolution. Zbl 1336.68236Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei 7 2009 Algorithms, datastructures, and other issues in efficient automated deduction. Zbl 0988.68585Voronkov, Andrei 7 2001 On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei 7 2001 Extensional crisis and proving identity. Zbl 1448.68459Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei 7 2014 Proof-search in intuitionistic logic based on constraint satisfaction. Zbl 1415.03010Voronkov, Andrei 7 1996 Theorem proving in nonstandard logics based on the inverse method. Zbl 0925.03075Voronkov, Andrei 7 1992 Encodings of bounded LTL model checking in effectively propositional logic. Zbl 1213.68386Navarro-Pérez, Juan Antonio; Voronkov, Andrei 6 2007 Unification with abstraction and theory instantiation in saturation-based reasoning. Zbl 1423.68424Reger, Giles; Suda, Martin; Voronkov, Andrei 6 2018 The 481 ways to split a clause and deal with propositional variables. Zbl 1382.68216Hoder, Kryštof; Voronkov, Andrei 6 2013 Translating regular expression matching into transducers. Zbl 1238.68052Sakuma, Yuto; Minamide, Yasuhiko; Voronkov, Andrei 5 2012 Complexity of some problems in modal and intuitionistic calculi. Zbl 1116.03328Maksimova, Larisa; Voronkov, Andrei 5 2003 Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 0866.68102Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei 5 1996 Elimination of equality via transformation with ordering constraints. Zbl 0926.03006Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei 5 1998 Induction in saturation-based proof search. Zbl 07178993Reger, Giles; Voronkov, Andrei 4 2019 Herbrand’s theorem, automated reasoning and semantic tableaux. Zbl 0945.03553Voronkov, Andrei 4 1998 A first class Boolean sort in first-order theorem proving and TPTP. Zbl 1417.68187Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei 4 2015 Logic programming with bounded quantifiers. Zbl 0925.03147Voronkov, Andrei 4 1992 Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 1415.03011Voronkov, Andrei 4 1996 Finding finite models in multi-sorted first-order logic. Zbl 1475.68447Reger, Giles; Suda, Martin; Voronkov, Andrei 3 2016 Upper bounds for a theory of queues. Zbl 1039.03005Rybina, Tatiana; Voronkov, Andrei 3 2003 Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Zbl 0937.03020Voronkov, Andrei 3 1999 The decidability of simultaneous rigid \(E\)-unification with one variable. Zbl 0903.03007Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei 3 1998 Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 0921.03012Voronkov, Andrei 3 1998 Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045Korovin, Konstantin; Voronkov, Andrei 3 2001 Induction with generalization in superposition reasoning. Zbl 1455.68248Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei 3 2020 Efficient instance retrieval with standard and relational path indexing. Zbl 1081.68018Riazanov, Alexandre; Voronkov, Andrei 2 2005 Basis of solutions for a system of linear inequalities in integers: Computation and applications. Zbl 1156.68623Chubarov, D.; Voronkov, A. 2 2005 Reasoning support for expressive ontology languages using a theorem prover. Zbl 1177.68179Horrocks, Ian; Voronkov, Andrei 2 2006 An AC-compatible Knuth-Bendix order. Zbl 1278.68268Korovin, Konstantin; Voronkov, Andrei 2 2003 Invariant and type inference for matrices. Zbl 1273.68083Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei 2 2010 Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012 2 2012 Inter-program properties. Zbl 1248.68156Voronkov, Andrei; Narasamdya, Iman 2 2009 How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Zbl 1171.03308Voronkov, Andrei 2 2001 Solving systems of linear inequalities by bound propagation. Zbl 1341.68193Korovin, Konstantin; Voronkov, Andrei 2 2011 On transfinite Knuth-Bendix orders. Zbl 1341.68194Kovács, Laura; Moser, Georg; Voronkov, Andrei 2 2011 Stratified resolution. Zbl 0963.03014Degtyarev, Anatoli; Voronkov, Andrei 2 2000 A nondeterministic polynomial-time unification algorithm for bags, sets and trees. Zbl 0942.68023Dantsin, Evgenyi; Voronkov, Andrei 2 1999 Planning with effectively propositional logic. Zbl 1383.68086Navarro-Pérez, Juan Antonio; Voronkov, Andrei 2 2013 Stratified resolution. Zbl 1024.03013Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei 2 2003 Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Zbl 1142.68011 2 2008 EPR-based bounded model checking at word level. Zbl 1358.68190Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei 2 2012 Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Zbl 0993.00050 2 2002 Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Zbl 1070.68001 1 2005 Efficient checking of term ordering constraints. Zbl 1126.68577Riazanov, Alexandre; Voronkov, Andrei 1 2004 Finding basic block and variable correspondence. Zbl 1141.68361Narasamdya, Iman; Voronkov, Andrei 1 2005 Perspectives of systems informatics. 6th international Andrei Ershov memorial conference, PSI 2006, Novosibirsk, Russia, June 27–30, 2006. Revised papers. Zbl 1179.68007 1 2007 A foolish encoding of the next state relations of imperative programs. Zbl 06958113Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei 1 2018 A note on semantics of logic programs with equality based on complete sets of \(E\)-unifiers. Zbl 0874.68058Degtyarev, Anatoli; Voronkov, Andrei 1 1996 Logic programming and automated reasoning. International conference, LPAR ‘92, St. Peterburg, Russia, July 15–20, 1992. Proceedings. Zbl 0916.00020 1 1992 Partially adaptive code trees. Zbl 0998.68155Riazanov, Alexandre; Voronkov, Andrei 1 2000 Integer induction in saturation. Zbl 07437089Hozzová, Petra; Kovács, Laura; Voronkov, Andrei 1 2021 Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016 1 2013 Making theory reasoning simpler. Zbl 1474.68060Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei 1 2021 First-order interpolation and interpolating proof systems. Zbl 1402.03041Kovács, Laura; Voronkov, Andrei 1 2017 Using canonical representations of solutions to speed up infinite-state model checking. Zbl 1010.68519Rybina, Tatiana; Voronkov, Andrei 1 2002 Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Zbl 1136.68004 1 2007 Computer science – theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3–7, 2007. Proceedings. Zbl 1135.68001 1 2007 Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings. Zbl 1197.68008 1 2010 Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Zbl 1203.68004 1 2010 Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 1049.68120Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei 1 2001 Integer induction in saturation. Zbl 07437089Hozzová, Petra; Kovács, Laura; Voronkov, Andrei 1 2021 Making theory reasoning simpler. Zbl 1474.68060Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei 1 2021 Induction with generalization in superposition reasoning. Zbl 1455.68248Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei 3 2020 Induction in saturation-based proof search. Zbl 07178993Reger, Giles; Voronkov, Andrei 4 2019 Unification with abstraction and theory instantiation in saturation-based reasoning. Zbl 1423.68424Reger, Giles; Suda, Martin; Voronkov, Andrei 6 2018 A foolish encoding of the next state relations of imperative programs. Zbl 06958113Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei 1 2018 Coming to terms with quantified reasoning. Zbl 1380.68280Kovács, Laura; Robillard, Simon; Voronkov, Andrei 7 2017 First-order interpolation and interpolating proof systems. Zbl 1402.03041Kovács, Laura; Voronkov, Andrei 1 2017 Selecting the selection. Zbl 1475.68436Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei 9 2016 Finding finite models in multi-sorted first-order logic. Zbl 1475.68447Reger, Giles; Suda, Martin; Voronkov, Andrei 3 2016 Playing with AVATAR. Zbl 1465.68295Reger, Giles; Suda, Martin; Voronkov, Andrei 13 2015 A first class Boolean sort in first-order theorem proving and TPTP. Zbl 1417.68187Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei 4 2015 AVATAR: the architecture for first-order theorem provers. Zbl 1495.68240Voronkov, Andrei 12 2014 Extensional crisis and proving identity. Zbl 1448.68459Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei 7 2014 The 481 ways to split a clause and deal with propositional variables. Zbl 1382.68216Hoder, Kryštof; Voronkov, Andrei 6 2013 Planning with effectively propositional logic. Zbl 1383.68086Navarro-Pérez, Juan Antonio; Voronkov, Andrei 2 2013 Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016 1 2013 Playing in the grey area of proofs. Zbl 1321.68196Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei 8 2012 Translating regular expression matching into transducers. Zbl 1238.68052Sakuma, Yuto; Minamide, Yasuhiko; Voronkov, Andrei 5 2012 Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012 2 2012 EPR-based bounded model checking at word level. Zbl 1358.68190Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei 2 2012 Sine qua non for large theory reasoning. Zbl 1341.68189Hoder, Kryštof; Voronkov, Andrei 26 2011 Solving systems of linear inequalities by bound propagation. Zbl 1341.68193Korovin, Konstantin; Voronkov, Andrei 2 2011 On transfinite Knuth-Bendix orders. Zbl 1341.68194Kovács, Laura; Moser, Georg; Voronkov, Andrei 2 2011 Interpolation and symbol elimination in Vampire. Zbl 1291.68348Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei 14 2010 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128Urban, Josef; Hoder, Krystof; Voronkov, Andrei 10 2010 Invariant and type inference for matrices. Zbl 1273.68083Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei 2 2010 Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings. Zbl 1197.68008 1 2010 Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Zbl 1203.68004 1 2010 Interpolation and symbol elimination. Zbl 1250.68193Kovács, Laura; Voronkov, Andrei 19 2009 Path feasibility analysis for string-manipulating programs. Zbl 1234.68070Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei 18 2009 Conflict resolution. Zbl 1336.68236Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei 7 2009 Inter-program properties. Zbl 1248.68156Voronkov, Andrei; Narasamdya, Iman 2 2009 Proof systems for effectively propositional logic. Zbl 1165.03318Navarro, Juan Antonio; Voronkov, Andrei 10 2008 Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Zbl 1142.68011 2 2008 Integrating linear arithmetic into superposition calculus. Zbl 1179.03018Korovin, Konstantin; Voronkov, Andrei 14 2007 Encodings of bounded LTL model checking in effectively propositional logic. Zbl 1213.68386Navarro-Pérez, Juan Antonio; Voronkov, Andrei 6 2007 Perspectives of systems informatics. 6th international Andrei Ershov memorial conference, PSI 2006, Novosibirsk, Russia, June 27–30, 2006. Revised papers. Zbl 1179.68007 1 2007 Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Zbl 1136.68004 1 2007 Computer science – theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3–7, 2007. Proceedings. Zbl 1135.68001 1 2007 Reasoning support for expressive ontology languages using a theorem prover. Zbl 1177.68179Horrocks, Ian; Voronkov, Andrei 2 2006 Efficient instance retrieval with standard and relational path indexing. Zbl 1081.68018Riazanov, Alexandre; Voronkov, Andrei 2 2005 Basis of solutions for a system of linear inequalities in integers: Computation and applications. Zbl 1156.68623Chubarov, D.; Voronkov, A. 2 2005 Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Zbl 1070.68001 1 2005 Finding basic block and variable correspondence. Zbl 1141.68361Narasamdya, Iman; Voronkov, Andrei 1 2005 TeMP: A temporal monodic prover. Zbl 1126.68568Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei 10 2004 Efficient checking of term ordering constraints. Zbl 1126.68577Riazanov, Alexandre; Voronkov, Andrei 1 2004 Limited resource strategy in resolution theorem proving. Zbl 1023.68089Riazanov, Alexandre; Voronkov, Andrei 13 2003 A logical reconstruction of reachability. Zbl 1254.68153Rybina, Tatiana; Voronkov, Andrei 8 2003 Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079Korovin, Konstantin; Voronkov, Andrei 8 2003 Complexity of some problems in modal and intuitionistic calculi. Zbl 1116.03328Maksimova, Larisa; Voronkov, Andrei 5 2003 Upper bounds for a theory of queues. Zbl 1039.03005Rybina, Tatiana; Voronkov, Andrei 3 2003 An AC-compatible Knuth-Bendix order. Zbl 1278.68268Korovin, Konstantin; Voronkov, Andrei 2 2003 Stratified resolution. Zbl 1024.03013Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei 2 2003 The design and implementation of VAMPIRE. Zbl 1021.68082Riazanov, Alexandre; Voronkov, Andrei 69 2002 Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Zbl 0993.00050 2 2002 Using canonical representations of solutions to speed up infinite-state model checking. Zbl 1010.68519Rybina, Tatiana; Voronkov, Andrei 1 2002 Handbook of automated reasoning. In 2 vols. Zbl 0964.00020 45 2001 Term indexing. Zbl 0992.68189Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei 30 2001 Term-modal logics. Zbl 0992.03026Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei 13 2001 Equality reasoning in sequent-based calculi. Zbl 1011.03004Degtyarev, Anatoli; Voronkov, Andrei 12 2001 Vampire 1. 1 (system description). Zbl 0988.68607Riazanov, Alexandre; Voronkov, Andrei 11 2001 The inverse method. Zbl 0992.03016Degtyarev, Anatoli; Voronkov, Andrei 10 2001 A decision procedure for term algebras with queues. Zbl 1171.68557Rybina, Tatiana; Voronkov, Andrei 10 2001 Algorithms, datastructures, and other issues in efficient automated deduction. Zbl 0988.68585Voronkov, Andrei 7 2001 On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei 7 2001 Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045Korovin, Konstantin; Voronkov, Andrei 3 2001 How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Zbl 1171.03308Voronkov, Andrei 2 2001 Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 1049.68120Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei 1 2001 Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Zbl 0944.68103Degtyarev, A.; Gurevich, Y.; Narendran, P.; Veanes, M.; Voronkov, A. 7 2000 Stratified resolution. Zbl 0963.03014Degtyarev, Anatoli; Voronkov, Andrei 2 2000 Partially adaptive code trees. Zbl 0998.68155Riazanov, Alexandre; Voronkov, Andrei 1 2000 Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Zbl 0937.03020Voronkov, Andrei 3 1999 A nondeterministic polynomial-time unification algorithm for bags, sets and trees. Zbl 0942.68023Dantsin, Evgenyi; Voronkov, Andrei 2 1999 What you always wanted to know about rigid \(E\)-unification. Zbl 0893.68135Degtyarev, Anatoli; Voronkov, Andrei 9 1998 Elimination of equality via transformation with ordering constraints. Zbl 0926.03006Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei 5 1998 Herbrand’s theorem, automated reasoning and semantic tableaux. Zbl 0945.03553Voronkov, Andrei 4 1998 The decidability of simultaneous rigid \(E\)-unification with one variable. Zbl 0903.03007Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei 3 1998 Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 0921.03012Voronkov, Andrei 3 1998 Monadic simultaneous rigid \(E\)-unification and related problems. Zbl 1401.03037Gurevich, Yuri; Voronkov, Andrei 7 1997 The undecidability of simultaneous rigid E-unification. Zbl 0872.68173Degtyarev, Anatoli; Voronkov, Andrei 18 1996 Proof-search in intuitionistic logic based on constraint satisfaction. Zbl 1415.03010Voronkov, Andrei 7 1996 Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 0866.68102Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei 5 1996 Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 1415.03011Voronkov, Andrei 4 1996 A note on semantics of logic programs with equality based on complete sets of \(E\)-unifiers. Zbl 0874.68058Degtyarev, Anatoli; Voronkov, Andrei 1 1996 The anatomy of vampire. Implementing bottom-up procedures with code trees. Zbl 0838.68100Voronkov, Andrei 14 1995 Theorem proving in nonstandard logics based on the inverse method. Zbl 0925.03075Voronkov, Andrei 7 1992 Logic programming with bounded quantifiers. Zbl 0925.03147Voronkov, Andrei 4 1992 Logic programming and automated reasoning. International conference, LPAR ‘92, St. Peterburg, Russia, July 15–20, 1992. Proceedings. Zbl 0916.00020 1 1992 all cited Publications top 5 cited Publications all top 5 Cited by 510 Authors 29 Voronkov, Andrei 18 Urban, Josef 17 Blanchette, Jasmin Christian 14 Weidenbach, Christoph 13 Sutcliffe, Geoff 12 Kaliszyk, Cezary 11 Reger, Giles 11 Tinelli, Cesare 10 Barrett, Clark W. 9 Bonacina, Maria Paola 9 Tourret, Sophie 8 Paulson, Lawrence Charles 8 Reynolds, Andrew 8 Suda, Martin 7 Ghilardi, Silvio 7 Kovács, Laura Ildikó 7 Vukmirović, Petar 7 Waldmann, Uwe 6 Bentkamp, Alexander 6 Benzmüller, Christoph Ewald 6 Böhme, Sascha 6 Middeldorp, Aart 6 Zohar, Yoni 5 Degtyarev, Anatoli Ivanovich 5 Dixon, Clare 5 Fontaine, Pascal 5 Korovin, Konstantin 5 Rümmer, Philipp 5 Schmidt, Renate A. 5 Sofronie-Stokkermans, Viorica 5 Veanes, Margus 4 Backeman, Peter 4 Baumgartner, Peter 4 Cruanes, Simon 4 de Moura, Leonardo 4 Djelloul, Khalil 4 Gurevich, Yuri 4 Kapur, Deepak 4 Nipkow, Tobias 4 Ranise, Silvio 4 Schulz, Stephan 4 Winkler, Sarah 3 Berzish, Murphy 3 Bhayat, Ahmed 3 Biere, Armin 3 Bjørner, Nikolaj S. 3 Brown, Chad Edward 3 Day, Joel D. 3 Färber, Michael 3 Ganesh, Vijay 3 Gianola, Alessandro 3 He, Xingxing 3 Hillenbrand, Thomas 3 Hirokawa, Nao 3 Hoder, Kryštof 3 Hustadt, Ullrich 3 Janičić, Predrag 3 Johansson, Moa 3 Konev, Boris 3 Kühlwein, Daniel 3 Liu, Jun 3 Maksimova, Larisa L’vovna 3 Meng, Jia 3 Mora, Federico 3 Nummelin, Visa 3 Peltier, Nicolas 3 Plaisted, David Alan 3 Rabe, Florian 3 Rawson, Michael 3 Ringeissen, Christophe 3 Sheng, Ying 3 Sorge, Volker 3 Vyskočil, Jiří 3 Woltzenlogel Paleo, Bruno 3 Xu, Yang 3 Zankl, Harald 2 Alama, Jesse 2 Bensaid, Hicham 2 Berglund, Martin 2 Beringer, Lennart 2 Bozzelli, Laura 2 Bringsjord, Selmer 2 Bromberger, Martin 2 Bruttomesso, Roberto 2 Bultan, Tevfik 2 Calvanese, Diego 2 Chaudhuri, Kaustuv 2 Chen, Mingshuai 2 Chen, Shuwei 2 Cheney, James 2 Egly, Uwe 2 Erkens, Rick 2 Fleury, Mathias 2 Furbach, Ulrich 2 Galmiche, Didier 2 Gauthier, Thibault 2 Gleiss, Bernhard 2 Goertzel, Zarathustra Amadeus 2 Goubault-Larrecq, Jean 2 Heljanko, Keijo ...and 410 more Authors all top 5 Cited in 46 Serials 62 Journal of Automated Reasoning 13 Theoretical Computer Science 13 Information and Computation 10 Journal of Symbolic Computation 10 Journal of Applied Logic 9 Formal Methods in System Design 8 Annals of Mathematics and Artificial Intelligence 7 Artificial Intelligence 7 Logical Methods in Computer Science 6 Studia Logica 6 Theory and Practice of Logic Programming 5 AI Communications 4 Formal Aspects of Computing 4 ACM Transactions on Computational Logic 4 Journal of Logical and Algebraic Methods in Programming 3 Mathematics in Computer Science 3 Logica Universalis 2 Information Processing Letters 2 Applied Mathematics and Computation 2 Information Sciences 2 Annals of Pure and Applied Logic 2 New Generation Computing 2 Journal of Applied Non-Classical Logics 2 Soft Computing 1 Acta Informatica 1 Lithuanian Mathematical Journal 1 Algebra and Logic 1 Automatica 1 Journal of Philosophical Logic 1 The Journal of Symbolic Logic 1 Programming and Computer Software 1 Siberian Mathematical Journal 1 Ergodic Theory and Dynamical Systems 1 Science of Computer Programming 1 MSCS. Mathematical Structures in Computer Science 1 Applicable Algebra in Engineering, Communication and Computing 1 Constraints 1 Higher-Order and Symbolic Computation 1 LMS Journal of Computation and Mathematics 1 Fundamenta Informaticae 1 The Journal of Logic and Algebraic Programming 1 Sibirskie Èlektronnye Matematicheskie Izvestiya 1 Proceedings of the Steklov Institute of Mathematics 1 The Review of Symbolic Logic 1 Izvestiya Irkutskogo Gosudarstvennogo Universiteta. Seriya Matematika 1 Journal of Membrane Computing all top 5 Cited in 14 Fields 328 Computer science (68-XX) 182 Mathematical logic and foundations (03-XX) 6 Operations research, mathematical programming (90-XX) 4 Information and communication theory, circuits (94-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 2 Systems theory; control (93-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Number theory (11-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Geometry (51-XX) 1 Numerical analysis (65-XX) Citations by Year