×
Author ID: voronkov.andrei Recent zbMATH articles by "Voronkov, Andrei"
Published as: Voronkov, Andrei; Voronkov, A.
all top 5

Co-Authors

20 single-authored
15 Kovács, Laura Ildikó
13 Korovin, Konstantin
12 Degtyarev, Anatoli Ivanovich
9 Reger, Giles
9 Riazanov, Alexandre
6 Gurevich, Yuri
6 Hoder, Kryštof
5 Hozzová, Petra
5 Rybina, Tatiana
5 Suda, Martin
4 Nieuwenhuis, Robert
4 Virbitskaite, Irina B.
3 Hajdú, Márton
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 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 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 Norman, Chase
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

Publications by Year

Citations contained in zbMATH Open

94 Publications have been cited 703 times in 446 Documents Cited by Year
The design and implementation of VAMPIRE. Zbl 1021.68082
Riazanov, Alexandre; Voronkov, Andrei
80
2002
Handbook of automated reasoning. In 2 vols. Zbl 0964.00020
78
2001
AVATAR: the architecture for first-order theorem provers. Zbl 1495.68240
Voronkov, Andrei
39
2014
Term indexing. Zbl 0992.68189
Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei
32
2001
Sine qua non for large theory reasoning. Zbl 1341.68189
Hoder, Kryštof; Voronkov, Andrei
26
2011
Path feasibility analysis for string-manipulating programs. Zbl 1234.68070
Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
22
2009
Interpolation and symbol elimination. Zbl 1250.68193
Kovács, Laura; Voronkov, Andrei
20
2009
The undecidability of simultaneous rigid E-unification. Zbl 0872.68173
Degtyarev, Anatoli; Voronkov, Andrei
18
1996
Term-modal logics. Zbl 0992.03026
Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei
18
2001
Integrating linear arithmetic into superposition calculus. Zbl 1179.03018
Korovin, Konstantin; Voronkov, Andrei
18
2007
Playing with AVATAR. Zbl 1465.68295
Reger, Giles; Suda, Martin; Voronkov, Andrei
17
2015
Interpolation and symbol elimination in Vampire. Zbl 1291.68348
Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei
15
2010
Limited resource strategy in resolution theorem proving. Zbl 1023.68089
Riazanov, Alexandre; Voronkov, Andrei
14
2003
The anatomy of vampire. Implementing bottom-up procedures with code trees. Zbl 0838.68100
Voronkov, Andrei
14
1995
Equality reasoning in sequent-based calculi. Zbl 1011.03004
Degtyarev, Anatoli; Voronkov, Andrei
13
2001
Vampire 1. 1 (system description). Zbl 0988.68607
Riazanov, Alexandre; Voronkov, Andrei
13
2001
Proof systems for effectively propositional logic. Zbl 1165.03318
Navarro, Juan Antonio; Voronkov, Andrei
12
2008
Coming to terms with quantified reasoning. Zbl 1380.68280
Kovács, Laura; Robillard, Simon; Voronkov, Andrei
11
2017
A decision procedure for term algebras with queues. Zbl 1171.68557
Rybina, Tatiana; Voronkov, Andrei
11
2001
The inverse method. Zbl 0992.03016
Degtyarev, Anatoli; Voronkov, Andrei
11
2001
TeMP: A temporal monodic prover. Zbl 1126.68568
Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei
11
2004
Selecting the selection. Zbl 1475.68436
Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei
10
2016
Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128
Urban, Josef; Hoder, Krystof; Voronkov, Andrei
10
2010
Conflict resolution. Zbl 1336.68236
Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei
10
2009
Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079
Korovin, Konstantin; Voronkov, Andrei
10
2003
A logical reconstruction of reachability. Zbl 1254.68153
Rybina, Tatiana; Voronkov, Andrei
10
2003
Playing in the grey area of proofs. Zbl 1321.68196
Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei
9
2012
What you always wanted to know about rigid \(E\)-unification. Zbl 0893.68135
Degtyarev, Anatoli; Voronkov, Andrei
9
1998
Unification with abstraction and theory instantiation in saturation-based reasoning. Zbl 1423.68424
Reger, Giles; Suda, Martin; Voronkov, Andrei
8
2018
On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei
8
2001
Induction in saturation-based proof search. Zbl 07178993
Reger, Giles; Voronkov, Andrei
8
2019
Induction with generalization in superposition reasoning. Zbl 1455.68248
Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei
8
2020
Extensional crisis and proving identity. Zbl 1448.68459
Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei
7
2014
Monadic simultaneous rigid \(E\)-unification and related problems. Zbl 1401.03037
Gurevich, Yuri; Voronkov, Andrei
7
1997
Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Zbl 0944.68103
Degtyarev, A.; Gurevich, Y.; Narendran, P.; Veanes, M.; Voronkov, A.
7
2000
Proof-search in intuitionistic logic based on constraint satisfaction. Zbl 1415.03010
Voronkov, Andrei
7
1996
Theorem proving in nonstandard logics based on the inverse method. Zbl 0925.03075
Voronkov, Andrei
7
1992
Algorithms, datastructures, and other issues in efficient automated deduction. Zbl 0988.68585
Voronkov, Andrei
7
2001
Elimination of equality via transformation with ordering constraints. Zbl 0926.03006
Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei
7
1998
Encodings of bounded LTL model checking in effectively propositional logic. Zbl 1213.68386
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
7
2007
The 481 ways to split a clause and deal with propositional variables. Zbl 1382.68216
Hoder, Kryštof; Voronkov, Andrei
6
2013
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 0866.68102
Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei
6
1996
Translating regular expression matching into transducers. Zbl 1238.68052
Sakuma, Yuto; Minamide, Yasuhiko; Voronkov, Andrei
6
2012
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 1415.03011
Voronkov, Andrei
5
1996
Complexity of some problems in modal and intuitionistic calculi. Zbl 1116.03328
Maksimova, Larisa; Voronkov, Andrei
5
2003
Finding finite models in multi-sorted first-order logic. Zbl 1475.68447
Reger, Giles; Suda, Martin; Voronkov, Andrei
4
2016
Reasoning support for expressive ontology languages using a theorem prover. Zbl 1177.68179
Horrocks, Ian; Voronkov, Andrei
4
2006
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
4
2010
Logic programming with bounded quantifiers. Zbl 0925.03147
Voronkov, Andrei
4
1992
Herbrand’s theorem, automated reasoning and semantic tableaux. Zbl 0945.03553
Voronkov, Andrei
4
1998
Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045
Korovin, Konstantin; Voronkov, Andrei
4
2001
Making theory reasoning simpler. Zbl 1474.68060
Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei
4
2021
First-order interpolation and interpolating proof systems. Zbl 1402.03041
Kovács, Laura; Voronkov, Andrei
3
2017
A first class Boolean sort in first-order theorem proving and TPTP. Zbl 1417.68187
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei
3
2015
Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016
3
2013
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Zbl 1171.03308
Voronkov, Andrei
3
2001
Solving systems of linear inequalities by bound propagation. Zbl 1341.68193
Korovin, Konstantin; Voronkov, Andrei
3
2011
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Zbl 0937.03020
Voronkov, Andrei
3
1999
Stratified resolution. Zbl 1024.03013
Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei
3
2003
Upper bounds for a theory of queues. Zbl 1039.03005
Rybina, Tatiana; Voronkov, Andrei
3
2003
Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 0921.03012
Voronkov, Andrei
3
1998
Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Zbl 0993.00050
3
2002
The decidability of simultaneous rigid \(E\)-unification with one variable. Zbl 0903.03007
Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei
3
1998
Invariant and type inference for matrices. Zbl 1273.68083
Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei
3
2010
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
3
2007
Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012
3
2012
Integer induction in saturation. Zbl 07437089
Hozzová, Petra; Kovács, Laura; Voronkov, Andrei
3
2021
Cooperating proof attempts. Zbl 1465.68296
Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei
2
2015
Basis of solutions for a system of linear inequalities in integers: Computation and applications. Zbl 1156.68623
Chubarov, D.; Voronkov, A.
2
2005
Efficient instance retrieval with standard and relational path indexing. Zbl 1081.68018
Riazanov, Alexandre; Voronkov, Andrei
2
2005
Inter-program properties. Zbl 1248.68156
Voronkov, Andrei; Narasamdya, Iman
2
2009
EPR-based bounded model checking at word level. Zbl 1358.68190
Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei
2
2012
On transfinite Knuth-Bendix orders. Zbl 1341.68194
Kovács, Laura; Moser, Georg; Voronkov, Andrei
2
2011
Stratified resolution. Zbl 0963.03014
Degtyarev, Anatoli; Voronkov, Andrei
2
2000
Logic programming and automated reasoning. International conference, LPAR ‘92, St. Peterburg, Russia, July 15–20, 1992. Proceedings. Zbl 0916.00020
2
1992
Partially adaptive code trees. Zbl 0998.68155
Riazanov, Alexandre; Voronkov, Andrei
2
2000
A nondeterministic polynomial-time unification algorithm for bags, sets and trees. Zbl 0942.68023
Dantsin, Evgenyi; Voronkov, Andrei
2
1999
Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Zbl 1142.68011
2
2008
An AC-compatible Knuth-Bendix order. Zbl 1278.68268
Korovin, Konstantin; Voronkov, Andrei
2
2003
Planning with effectively propositional logic. Zbl 1383.68086
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
2
2013
Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3–7, 2001. Proceedings. Zbl 1046.03001
1
2001
Finding basic block and variable correspondence. Zbl 1141.68361
Narasamdya, Iman; Voronkov, Andrei
1
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
A note on semantics of logic programs with equality based on complete sets of \(E\)-unifiers. Zbl 0874.68058
Degtyarev, Anatoli; Voronkov, Andrei
1
1996
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 and automated reasoning. 6th international conference, LPAR ’99, Tbilisi, Georgia, September 6–10, 1999. Proceedings. Zbl 0921.00037
1
1999
Using canonical representations of solutions to speed up infinite-state model checking. Zbl 1010.68519
Rybina, Tatiana; Voronkov, Andrei
1
2002
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 1049.68120
Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei
1
2001
Verifying orientability of rewrite rules using the Knuth-Bendix order. Zbl 0981.68072
Korovin, Konstantin; Voronkov, Andrei
1
2001
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
Efficient checking of term ordering constraints. Zbl 1126.68577
Riazanov, Alexandre; Voronkov, Andrei
1
2004
Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Zbl 1136.68004
1
2007
Inductive benchmarks for automated reasoning. Zbl 1485.68281
Hajdu, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei
1
2021
A FOOLish encoding of the next state relations of imperative programs. Zbl 1511.68160
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei
1
2018
Making theory reasoning simpler. Zbl 1474.68060
Reger, Giles; Schoisswohl, Johannes; Voronkov, Andrei
4
2021
Integer induction in saturation. Zbl 07437089
Hozzová, Petra; Kovács, Laura; Voronkov, Andrei
3
2021
Inductive benchmarks for automated reasoning. Zbl 1485.68281
Hajdu, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei
1
2021
Induction with generalization in superposition reasoning. Zbl 1455.68248
Hajdú, Márton; Hozzová, Petra; Kovács, Laura; Schoisswohl, Johannes; Voronkov, Andrei
8
2020
Induction in saturation-based proof search. Zbl 07178993
Reger, Giles; Voronkov, Andrei
8
2019
Unification with abstraction and theory instantiation in saturation-based reasoning. Zbl 1423.68424
Reger, Giles; Suda, Martin; Voronkov, Andrei
8
2018
A FOOLish encoding of the next state relations of imperative programs. Zbl 1511.68160
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei
1
2018
Coming to terms with quantified reasoning. Zbl 1380.68280
Kovács, Laura; Robillard, Simon; Voronkov, Andrei
11
2017
First-order interpolation and interpolating proof systems. Zbl 1402.03041
Kovács, Laura; Voronkov, Andrei
3
2017
Selecting the selection. Zbl 1475.68436
Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei
10
2016
Finding finite models in multi-sorted first-order logic. Zbl 1475.68447
Reger, Giles; Suda, Martin; Voronkov, Andrei
4
2016
Playing with AVATAR. Zbl 1465.68295
Reger, Giles; Suda, Martin; Voronkov, Andrei
17
2015
A first class Boolean sort in first-order theorem proving and TPTP. Zbl 1417.68187
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei
3
2015
Cooperating proof attempts. Zbl 1465.68296
Reger, Giles; Tishkovsky, Dmitry; Voronkov, Andrei
2
2015
AVATAR: the architecture for first-order theorem provers. Zbl 1495.68240
Voronkov, Andrei
39
2014
Extensional crisis and proving identity. Zbl 1448.68459
Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei
7
2014
The 481 ways to split a clause and deal with propositional variables. Zbl 1382.68216
Hoder, Kryštof; Voronkov, Andrei
6
2013
Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Zbl 1277.68016
3
2013
Planning with effectively propositional logic. Zbl 1383.68086
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
2
2013
Playing in the grey area of proofs. Zbl 1321.68196
Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei
9
2012
Translating regular expression matching into transducers. Zbl 1238.68052
Sakuma, Yuto; Minamide, Yasuhiko; Voronkov, Andrei
6
2012
Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012
3
2012
EPR-based bounded model checking at word level. Zbl 1358.68190
Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei
2
2012
Sine qua non for large theory reasoning. Zbl 1341.68189
Hoder, Kryštof; Voronkov, Andrei
26
2011
Solving systems of linear inequalities by bound propagation. Zbl 1341.68193
Korovin, Konstantin; Voronkov, Andrei
3
2011
On transfinite Knuth-Bendix orders. Zbl 1341.68194
Kovács, Laura; Moser, Georg; Voronkov, Andrei
2
2011
Interpolation and symbol elimination in Vampire. Zbl 1291.68348
Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei
15
2010
Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128
Urban, Josef; Hoder, Krystof; Voronkov, Andrei
10
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
4
2010
Invariant and type inference for matrices. Zbl 1273.68083
Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei
3
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
Path feasibility analysis for string-manipulating programs. Zbl 1234.68070
Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
22
2009
Interpolation and symbol elimination. Zbl 1250.68193
Kovács, Laura; Voronkov, Andrei
20
2009
Conflict resolution. Zbl 1336.68236
Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei
10
2009
Inter-program properties. Zbl 1248.68156
Voronkov, Andrei; Narasamdya, Iman
2
2009
Proof systems for effectively propositional logic. Zbl 1165.03318
Navarro, Juan Antonio; Voronkov, Andrei
12
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.03018
Korovin, Konstantin; Voronkov, Andrei
18
2007
Encodings of bounded LTL model checking in effectively propositional logic. Zbl 1213.68386
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
7
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
3
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
Reasoning support for expressive ontology languages using a theorem prover. Zbl 1177.68179
Horrocks, Ian; Voronkov, Andrei
4
2006
Basis of solutions for a system of linear inequalities in integers: Computation and applications. Zbl 1156.68623
Chubarov, D.; Voronkov, A.
2
2005
Efficient instance retrieval with standard and relational path indexing. Zbl 1081.68018
Riazanov, Alexandre; Voronkov, Andrei
2
2005
Finding basic block and variable correspondence. Zbl 1141.68361
Narasamdya, Iman; Voronkov, Andrei
1
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
TeMP: A temporal monodic prover. Zbl 1126.68568
Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei
11
2004
Efficient checking of term ordering constraints. Zbl 1126.68577
Riazanov, Alexandre; Voronkov, Andrei
1
2004
Limited resource strategy in resolution theorem proving. Zbl 1023.68089
Riazanov, Alexandre; Voronkov, Andrei
14
2003
Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079
Korovin, Konstantin; Voronkov, Andrei
10
2003
A logical reconstruction of reachability. Zbl 1254.68153
Rybina, Tatiana; Voronkov, Andrei
10
2003
Complexity of some problems in modal and intuitionistic calculi. Zbl 1116.03328
Maksimova, Larisa; Voronkov, Andrei
5
2003
Stratified resolution. Zbl 1024.03013
Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei
3
2003
Upper bounds for a theory of queues. Zbl 1039.03005
Rybina, Tatiana; Voronkov, Andrei
3
2003
An AC-compatible Knuth-Bendix order. Zbl 1278.68268
Korovin, Konstantin; Voronkov, Andrei
2
2003
The design and implementation of VAMPIRE. Zbl 1021.68082
Riazanov, Alexandre; Voronkov, Andrei
80
2002
Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Zbl 0993.00050
3
2002
Using canonical representations of solutions to speed up infinite-state model checking. Zbl 1010.68519
Rybina, Tatiana; Voronkov, Andrei
1
2002
Handbook of automated reasoning. In 2 vols. Zbl 0964.00020
78
2001
Term indexing. Zbl 0992.68189
Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei
32
2001
Term-modal logics. Zbl 0992.03026
Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei
18
2001
Equality reasoning in sequent-based calculi. Zbl 1011.03004
Degtyarev, Anatoli; Voronkov, Andrei
13
2001
Vampire 1. 1 (system description). Zbl 0988.68607
Riazanov, Alexandre; Voronkov, Andrei
13
2001
A decision procedure for term algebras with queues. Zbl 1171.68557
Rybina, Tatiana; Voronkov, Andrei
11
2001
The inverse method. Zbl 0992.03016
Degtyarev, Anatoli; Voronkov, Andrei
11
2001
On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei
8
2001
Algorithms, datastructures, and other issues in efficient automated deduction. Zbl 0988.68585
Voronkov, Andrei
7
2001
Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045
Korovin, Konstantin; Voronkov, Andrei
4
2001
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Zbl 1171.03308
Voronkov, Andrei
3
2001
Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3–7, 2001. Proceedings. Zbl 1046.03001
1
2001
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 1049.68120
Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei
1
2001
Verifying orientability of rewrite rules using the Knuth-Bendix order. Zbl 0981.68072
Korovin, Konstantin; Voronkov, Andrei
1
2001
Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Zbl 0944.68103
Degtyarev, A.; Gurevich, Y.; Narendran, P.; Veanes, M.; Voronkov, A.
7
2000
Stratified resolution. Zbl 0963.03014
Degtyarev, Anatoli; Voronkov, Andrei
2
2000
Partially adaptive code trees. Zbl 0998.68155
Riazanov, Alexandre; Voronkov, Andrei
2
2000
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Zbl 0937.03020
Voronkov, Andrei
3
1999
A nondeterministic polynomial-time unification algorithm for bags, sets and trees. Zbl 0942.68023
Dantsin, Evgenyi; Voronkov, Andrei
2
1999
Logic for programming and automated reasoning. 6th international conference, LPAR ’99, Tbilisi, Georgia, September 6–10, 1999. Proceedings. Zbl 0921.00037
1
1999
What you always wanted to know about rigid \(E\)-unification. Zbl 0893.68135
Degtyarev, Anatoli; Voronkov, Andrei
9
1998
Elimination of equality via transformation with ordering constraints. Zbl 0926.03006
Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei
7
1998
Herbrand’s theorem, automated reasoning and semantic tableaux. Zbl 0945.03553
Voronkov, Andrei
4
1998
Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 0921.03012
Voronkov, Andrei
3
1998
The decidability of simultaneous rigid \(E\)-unification with one variable. Zbl 0903.03007
Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei
3
1998
Monadic simultaneous rigid \(E\)-unification and related problems. Zbl 1401.03037
Gurevich, Yuri; Voronkov, Andrei
7
1997
The undecidability of simultaneous rigid E-unification. Zbl 0872.68173
Degtyarev, Anatoli; Voronkov, Andrei
18
1996
Proof-search in intuitionistic logic based on constraint satisfaction. Zbl 1415.03010
Voronkov, Andrei
7
1996
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 0866.68102
Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei
6
1996
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 1415.03011
Voronkov, Andrei
5
1996
A note on semantics of logic programs with equality based on complete sets of \(E\)-unifiers. Zbl 0874.68058
Degtyarev, Anatoli; Voronkov, Andrei
1
1996
The anatomy of vampire. Implementing bottom-up procedures with code trees. Zbl 0838.68100
Voronkov, Andrei
14
1995
Theorem proving in nonstandard logics based on the inverse method. Zbl 0925.03075
Voronkov, Andrei
7
1992
Logic programming with bounded quantifiers. Zbl 0925.03147
Voronkov, Andrei
4
1992
Logic programming and automated reasoning. International conference, LPAR ‘92, St. Peterburg, Russia, July 15–20, 1992. Proceedings. Zbl 0916.00020
2
1992
all top 5

Cited by 609 Authors

31 Voronkov, Andrei
20 Blanchette, Jasmin Christian
19 Urban, Josef
19 Weidenbach, Christoph
15 Sutcliffe, Geoff
14 Tinelli, Cesare
13 Barrett, Clark W.
13 Reger, Giles
12 Bonacina, Maria Paola
12 Kaliszyk, Cezary
12 Kovács, Laura Ildikó
11 Reynolds, Andrew
10 Tourret, Sophie
9 Paulson, Lawrence Charles
9 Waldmann, Uwe
8 Benzmüller, Christoph Ewald
8 Ghilardi, Silvio
8 Suda, Martin
7 Vukmirović, Petar
7 Zohar, Yoni
6 Bentkamp, Alexander
6 Böhme, Sascha
6 de Moura, Leonardo
6 Dixon, Clare
6 Korovin, Konstantin
6 Middeldorp, Aart
6 Schmidt, Renate A.
6 Sofronie-Stokkermans, Viorica
5 Bhayat, Ahmed
5 Bjørner, Nikolaj S.
5 Degtyarev, Anatoli Ivanovich
5 Djelloul, Khalil
5 Fisher, Michael
5 Fontaine, Pascal
5 Liu, Jun
5 Ranise, Silvio
5 Rümmer, Philipp
5 Veanes, Margus
5 Winkler, Sarah
5 Xu, Yang
4 Backeman, Peter
4 Baumgartner, Peter
4 Biere, Armin
4 Brown, Chad Edward
4 Chen, Shuwei
4 Cruanes, Simon
4 Gurevich, Yuri
4 Hozzová, Petra
4 Kapur, Deepak
4 Nipkow, Tobias
4 Nötzli, Andres
4 Peltier, Nicolas
4 Schulz, Stephan
4 Sheng, Ying
4 Shtakser, Gennady
4 Vyskočil, Jiří
3 Berglund, Martin
3 Berzish, Murphy
3 Bromberger, Martin
3 Day, Joel D.
3 Ebner, Gabriel
3 Färber, Michael
3 Fleury, Mathias
3 Ganesh, Vijay
3 Gianola, Alessandro
3 He, Xingxing
3 Hetzl, Stefan
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 Kulczynski, Mitja
3 Leidinger, Hendrik
3 Maksimova, Larisa L’vovna
3 Meng, Jia
3 Mora, Federico
3 Nicolini, Enrica
3 Nowotka, Dirk
3 Nummelin, Visa
3 Padmanabha, Anantha
3 Peuter, Dennis
3 Plaisted, David Alan
3 Ramanujam, R.
3 Rawson, Michael
3 Ringeissen, Christophe
3 Schlichtkrull, Anders
3 Schoisswohl, Johannes
3 Sorge, Volker
3 Theiss, Frank
3 van der Merwe, Brink
3 Wernhard, Christoph
3 Zankl, Harald
2 Alama, Jesse
2 Barbosa, Haniel
2 Bensaid, Hicham
2 Beringer, Lennart
...and 509 more Authors
all top 5

Cited in 48 Serials

73 Journal of Automated Reasoning
16 Theoretical Computer Science
13 Information and Computation
11 Journal of Symbolic Computation
11 Formal Methods in System Design
11 Journal of Applied Logic
8 Annals of Mathematics and Artificial Intelligence
7 Artificial Intelligence
7 Studia Logica
7 Theory and Practice of Logic Programming
7 Logical Methods in Computer Science
6 AI Communications
5 Information Sciences
5 Formal Aspects of Computing
5 ACM Transactions on Computational Logic
4 Logica Universalis
4 Journal of Logical and Algebraic Methods in Programming
3 Mathematics in Computer Science
2 Information Processing Letters
2 Applied Mathematics and Computation
2 The Journal of Symbolic Logic
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 Programming and Computer Software
1 Siberian Mathematical Journal
1 Ergodic Theory and Dynamical Systems
1 Science of Computer Programming
1 Mathematical Structures in Computer Science
1 Applicable Algebra in Engineering, Communication and Computing
1 Journal of Logic, Language and Information
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 Logicheskie Issledovaniya
1 Journal of Membrane Computing

Citations by Year