×

zbMATH — the first resource for mathematics

Voronkov, Andrei

Compute Distance To:
Author ID: voronkov.andrei Recent zbMATH articles by "Voronkov, Andrei"
Published as: Voronkov, A.; Voronkov, Andrei
Documents Indexed: 124 Publications since 1992, including 30 Books
all top 5

Co-Authors

16 single-authored
13 Korovin, Konstantin
11 Degtyarev, Anatoli Ivanovich
11 Kovács, Laura Ildikó
9 Riazanov, Alexandre
6 Hoder, Kryštof
6 Reger, Giles
5 Gurevich, Yuri
5 Rybina, Tatiana
4 Nieuwenhuis, Robert
4 Suda, Martin
4 Virbitskaite, Irina B.
2 Bjørner, Nikolaj S.
2 Chubarov, Dmitri Leonidovich
2 Clarke, Edmund Melson jun.
2 Fitting, Melvin Chris
2 Ganzinger, Harald
2 Kotelnikov, Evgenii
2 Narasamdya, Iman
2 Pérez, Juan Antonio Navarro
2 Thalmann, Lars
2 Tsiskaridze, Nestan
2 Weidenbach, Christoph
1 Baader, Franz
1 Baaz, Matthias
1 Bachmair, Leo
1 Cervesato, Iliano
1 Dantsin, Evgeny
1 Davis, Martin David
1 Dershowitz, Nachum
1 Diekert, Volker
1 Emmer, Moshe
1 Fehnker, Ansgar
1 Fermüller, Christian G.
1 Gupta, Ashutosh
1 Hajdú, Márton
1 Henzinger, Thomas A.
1 Hermann, Miki
1 Hillenbrand, Thomas
1 Horrocks, Ian
1 Hottelier, Thibaud
1 Hozzová, Petra
1 Hustadt, Ullrich
1 Kapur, Deepak
1 Khasidashvili, Zurab O.
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 Narendran, Paliath
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 Schoisswohl, Johannes
1 Sekar, R. Chandra Guru
1 Sticksel, Christoph
1 Sutcliffe, Geoff
1 Tillmann, Nikolai
1 Tishkovsky, Dmitry
1 Urban, Josef
1 Vardi, Moshe Y.
1 Veanes, Margus
1 Veith, Helmut
1 Volkov, Mikhail Vladimirovich
1 Wilhelm, Reinhard

Publications by Year

Citations contained in zbMATH

76 Publications have been cited 451 times in 301 Documents Cited by Year
The design and implementation of VAMPIRE. Zbl 1021.68082
Riazanov, Alexandre; Voronkov, Andrei
60
2002
Handbook of automated reasoning. In 2 vols. Zbl 0964.00020
Robinson, Alan (ed.); Voronkov, A. (ed.)
43
2001
Sine qua non for large theory reasoning. Zbl 1341.68189
Hoder, Kryštof; Voronkov, Andrei
17
2011
Term indexing. Zbl 0992.68189
Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei
17
2001
The undecidability of simultaneous rigid E-unification. Zbl 0872.68173
Degtyarev, Anatoli; Voronkov, Andrei
15
1996
Interpolation and symbol elimination in Vampire. Zbl 1291.68348
Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei
11
2010
Interpolation and symbol elimination. Zbl 1250.68193
Kovács, Laura; Voronkov, Andrei
11
2009
Integrating linear arithmetic into superposition calculus. Zbl 1179.03018
Korovin, Konstantin; Voronkov, Andrei
11
2007
Vampire 1. 1 (system description). Zbl 0988.68607
Riazanov, Alexandre; Voronkov, Andrei
10
2001
Term-modal logics. Zbl 0992.03026
Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei
10
2001
The anatomy of vampire. Implementing bottom-up procedures with code trees. Zbl 0838.68100
Voronkov, Andrei
10
1995
Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128
Urban, Josef; Hoder, Krystof; Voronkov, Andrei
9
2010
Path feasibility analysis for string-manipulating programs. Zbl 1234.68070
Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
9
2009
The inverse method. Zbl 0992.03016
Degtyarev, Anatoli; Voronkov, Andrei
9
2001
TeMP: A temporal monodic prover. Zbl 1126.68568
Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei
8
2004
Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079
Korovin, Konstantin; Voronkov, Andrei
8
2003
Equality reasoning in sequent-based calculi. Zbl 1011.03004
Degtyarev, Anatoli; Voronkov, Andrei
8
2001
What you always wanted to know about rigid \(E\)-unification. Zbl 0893.68135
Degtyarev, Anatoli; Voronkov, Andrei
8
1998
Playing in the grey area of proofs. Zbl 1321.68196
Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei
7
2012
A decision procedure for term algebras with queues. Zbl 1171.68557
Rybina, Tatiana; Voronkov, Andrei
7
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
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 0866.68102
Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei
7
1996
Theorem proving in nonstandard logics based on the inverse method. Zbl 0925.03075
Voronkov, Andrei
7
1992
The 481 ways to split a clause and deal with propositional variables. Zbl 1382.68216
Hoder, Kryštof; Voronkov, Andrei
6
2013
Conflict resolution. Zbl 1336.68236
Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei
6
2009
Proof systems for effectively propositional logic. Zbl 1165.03318
Navarro, Juan Antonio; Voronkov, Andrei
6
2008
A logical reconstruction of reachability. Zbl 1254.68153
Rybina, Tatiana; Voronkov, Andrei
6
2003
Limited resource strategy in resolution theorem proving. Zbl 1023.68089
Riazanov, Alexandre; Voronkov, Andrei
6
2003
Algorithms, datastructures, and other issues in efficient automated deduction. Zbl 0988.68585
Voronkov, Andrei
6
2001
Monadic simultaneous rigid \(E\)-unification and related problems. Zbl 1401.03037
Gurevich, Yuri; Voronkov, Andrei
6
1997
Proof-search in intuitionistic logic based on constraint satisfaction. Zbl 1415.03010
Voronkov, Andrei
6
1996
Playing with AVATAR. Zbl 06515522
Reger, Giles; Suda, Martin; Voronkov, Andrei
5
2015
On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei
5
2001
Translating regular expression matching into transducers. Zbl 1238.68052
Sakuma, Yuto; Minamide, Yasuhiko; Voronkov, Andrei
4
2012
Encodings of bounded LTL model checking in effectively propositional logic. Zbl 1213.68386
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
4
2007
Herbrand’s theorem, automated reasoning and semantic tableaux. Zbl 0945.03553
Voronkov, Andrei
4
1998
The decidability of simultaneous rigid \(E\)-unification with one variable. Zbl 0903.03007
Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei
4
1998
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 1415.03011
Voronkov, Andrei
4
1996
Invariant and type inference for matrices. Zbl 1273.68083
Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura; Voronkov, Andrei
3
2010
Complexity of some problems in modal and intuitionistic calculi. Zbl 1116.03328
Maksimova, Larisa; Voronkov, Andrei
3
2003
Upper bounds for a theory of queues. Zbl 1039.03005
Rybina, Tatiana; Voronkov, Andrei
3
2003
Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Zbl 0993.00050
Voronkov, Andrei (ed.)
3
2002
Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045
Korovin, Konstantin; Voronkov, Andrei
3
2001
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Zbl 0937.03020
Voronkov, Andrei
3
1999
Elimination of equality via transformation with ordering constraints. Zbl 0926.03006
Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei
3
1998
Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 0921.03012
Voronkov, Andrei
3
1998
Logic programming with bounded quantifiers. Zbl 0925.03147
Voronkov, Andrei
3
1992
A first class Boolean sort in first-order theorem proving and TPTP. Zbl 1417.68187
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei
2
2015
Inter-program properties. Zbl 1248.68156
Voronkov, Andrei; Narasamdya, Iman
2
2009
Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Zbl 1142.68011
Voronkov, Andrei (ed.)
2
2008
An AC-compatible Knuth-Bendix order. Zbl 1278.68268
Korovin, Konstantin; Voronkov, Andrei
2
2003
Stratified resolution. Zbl 1024.03013
Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei
2
2003
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Zbl 1171.03308
Voronkov, Andrei
2
2001
Stratified resolution. Zbl 0963.03014
Degtyarev, Anatoli; Voronkov, Andrei
2
2000
A note on semantics of logic programs with equality based on complete sets of \(E\)-unifiers. Zbl 0874.68058
Degtyarev, Anatoli; Voronkov, Andrei
2
1996
Finding finite models in multi-sorted first-order logic. Zbl 06623520
Reger, Giles; Suda, Martin; Voronkov, Andrei
1
2016
Selecting the selection. Zbl 06623270
Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei
1
2016
Extensional crisis and proving identity. Zbl 1448.68459
Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei
1
2014
Planning with effectively propositional logic. Zbl 1383.68086
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
1
2013
EPR-based bounded model checking at word level. Zbl 1358.68190
Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei
1
2012
Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012
Bjørner, Nikolaj (ed.); Voronkov, Andrei (ed.)
1
2012
On transfinite Knuth-Bendix orders. Zbl 1341.68194
Kovács, Laura; Moser, Georg; Voronkov, Andrei
1
2011
Solving systems of linear inequalities by bound propagation. Zbl 1341.68193
Korovin, Konstantin; Voronkov, Andrei
1
2011
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
Clarke, Edmund M. (ed.); Voronkov, Andrei (ed.)
1
2010
Perspectives of systems informatics. 6th international Andrei Ershov memorial conference, PSI 2006, Novosibirsk, Russia, June 27–30, 2006. Revised papers. Zbl 1179.68007
Virbitskaite, Irina (ed.); Voronkov, Andrei (ed.)
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
Diekert, Volker (ed.); Volkov, Mikhail V. (ed.); Voronkov, Andrei (ed.)
1
2007
Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Zbl 1136.68004
Dershowitz, Nachum (ed.); Voronkov, Andrei (ed.)
1
2007
Reasoning support for expressive ontology languages using a theorem prover. Zbl 1177.68179
Horrocks, Ian; Voronkov, Andrei
1
2006
Finding basic block and variable correspondence. Zbl 1141.68361
Narasamdya, Iman; Voronkov, Andrei
1
2005
Efficient instance retrieval with standard and relational path indexing. Zbl 1081.68018
Riazanov, Alexandre; Voronkov, Andrei
1
2005
Efficient checking of term ordering constraints. Zbl 1126.68577
Riazanov, Alexandre; Voronkov, Andrei
1
2004
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
Partially adaptive code trees. Zbl 0998.68155
Riazanov, Alexandre; Voronkov, Andrei
1
2000
Monadic simultaneous rigid \(E\)-unification. Zbl 0930.03007
Gurevich, Yuri; Voronkov, Andrei
1
1999
A nondeterministic polynomial-time unification algorithm for bags, sets and trees. Zbl 0942.68023
Dantsin, Evgenyi; Voronkov, Andrei
1
1999
Finding finite models in multi-sorted first-order logic. Zbl 06623520
Reger, Giles; Suda, Martin; Voronkov, Andrei
1
2016
Selecting the selection. Zbl 06623270
Hoder, Kryštof; Reger, Giles; Suda, Martin; Voronkov, Andrei
1
2016
Playing with AVATAR. Zbl 06515522
Reger, Giles; Suda, Martin; Voronkov, Andrei
5
2015
A first class Boolean sort in first-order theorem proving and TPTP. Zbl 1417.68187
Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei
2
2015
Extensional crisis and proving identity. Zbl 1448.68459
Gupta, Ashutosh; Kovács, Laura; Kragl, Bernhard; Voronkov, Andrei
1
2014
The 481 ways to split a clause and deal with propositional variables. Zbl 1382.68216
Hoder, Kryštof; Voronkov, Andrei
6
2013
Planning with effectively propositional logic. Zbl 1383.68086
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
1
2013
Playing in the grey area of proofs. Zbl 1321.68196
Hoder, Krystof; Kovacs, Laura; Voronkov, Andrei
7
2012
Translating regular expression matching into transducers. Zbl 1238.68052
Sakuma, Yuto; Minamide, Yasuhiko; Voronkov, Andrei
4
2012
EPR-based bounded model checking at word level. Zbl 1358.68190
Emmer, Moshe; Khasidashvili, Zurab; Korovin, Konstantin; Sticksel, Christoph; Voronkov, Andrei
1
2012
Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Zbl 1238.68012
Bjørner, Nikolaj (ed.); Voronkov, Andrei (ed.)
1
2012
Sine qua non for large theory reasoning. Zbl 1341.68189
Hoder, Kryštof; Voronkov, Andrei
17
2011
On transfinite Knuth-Bendix orders. Zbl 1341.68194
Kovács, Laura; Moser, Georg; Voronkov, Andrei
1
2011
Solving systems of linear inequalities by bound propagation. Zbl 1341.68193
Korovin, Konstantin; Voronkov, Andrei
1
2011
Interpolation and symbol elimination in Vampire. Zbl 1291.68348
Hoder, Kryštof; Kovács, Laura; Voronkov, Andrei
11
2010
Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128
Urban, Josef; Hoder, Krystof; Voronkov, Andrei
9
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. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Zbl 1203.68004
Clarke, Edmund M. (ed.); Voronkov, Andrei (ed.)
1
2010
Interpolation and symbol elimination. Zbl 1250.68193
Kovács, Laura; Voronkov, Andrei
11
2009
Path feasibility analysis for string-manipulating programs. Zbl 1234.68070
Bjørner, Nikolaj; Tillmann, Nikolai; Voronkov, Andrei
9
2009
Conflict resolution. Zbl 1336.68236
Korovin, Konstantin; Tsiskaridze, Nestan; Voronkov, Andrei
6
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
6
2008
Rewriting techniques and applications. 19th international conference, RTA 2008, Hagenberg, Austria, July 15–17, 2008. Proceedings. Zbl 1142.68011
Voronkov, Andrei (ed.)
2
2008
Integrating linear arithmetic into superposition calculus. Zbl 1179.03018
Korovin, Konstantin; Voronkov, Andrei
11
2007
Encodings of bounded LTL model checking in effectively propositional logic. Zbl 1213.68386
Navarro-Pérez, Juan Antonio; Voronkov, Andrei
4
2007
Perspectives of systems informatics. 6th international Andrei Ershov memorial conference, PSI 2006, Novosibirsk, Russia, June 27–30, 2006. Revised papers. Zbl 1179.68007
Virbitskaite, Irina (ed.); Voronkov, Andrei (ed.)
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
Diekert, Volker (ed.); Volkov, Mikhail V. (ed.); Voronkov, Andrei (ed.)
1
2007
Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Zbl 1136.68004
Dershowitz, Nachum (ed.); Voronkov, Andrei (ed.)
1
2007
Reasoning support for expressive ontology languages using a theorem prover. Zbl 1177.68179
Horrocks, Ian; Voronkov, Andrei
1
2006
Finding basic block and variable correspondence. Zbl 1141.68361
Narasamdya, Iman; Voronkov, Andrei
1
2005
Efficient instance retrieval with standard and relational path indexing. Zbl 1081.68018
Riazanov, Alexandre; Voronkov, Andrei
1
2005
TeMP: A temporal monodic prover. Zbl 1126.68568
Hustadt, Ullrich; Konev, Boris; Riazanov, Alexandre; Voronkov, Andrei
8
2004
Efficient checking of term ordering constraints. Zbl 1126.68577
Riazanov, Alexandre; Voronkov, Andrei
1
2004
Orienting rewrite rules with the Knuth-Bendix order. Zbl 1054.68079
Korovin, Konstantin; Voronkov, Andrei
8
2003
A logical reconstruction of reachability. Zbl 1254.68153
Rybina, Tatiana; Voronkov, Andrei
6
2003
Limited resource strategy in resolution theorem proving. Zbl 1023.68089
Riazanov, Alexandre; Voronkov, Andrei
6
2003
Complexity of some problems in modal and intuitionistic calculi. Zbl 1116.03328
Maksimova, Larisa; 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
Stratified resolution. Zbl 1024.03013
Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei
2
2003
The design and implementation of VAMPIRE. Zbl 1021.68082
Riazanov, Alexandre; Voronkov, Andrei
60
2002
Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Zbl 0993.00050
Voronkov, Andrei (ed.)
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
Robinson, Alan (ed.); Voronkov, A. (ed.)
43
2001
Term indexing. Zbl 0992.68189
Sekar, R.; Ramakrishnan, I. V.; Voronkov, Andrei
17
2001
Vampire 1. 1 (system description). Zbl 0988.68607
Riazanov, Alexandre; Voronkov, Andrei
10
2001
Term-modal logics. Zbl 0992.03026
Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei
10
2001
The inverse method. Zbl 0992.03016
Degtyarev, Anatoli; Voronkov, Andrei
9
2001
Equality reasoning in sequent-based calculi. Zbl 1011.03004
Degtyarev, Anatoli; Voronkov, Andrei
8
2001
A decision procedure for term algebras with queues. Zbl 1171.68557
Rybina, Tatiana; Voronkov, Andrei
7
2001
Algorithms, datastructures, and other issues in efficient automated deduction. Zbl 0988.68585
Voronkov, Andrei
6
2001
On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei
5
2001
Knuth-Bendix constraint solving is NP-complete. Zbl 0986.68045
Korovin, Konstantin; Voronkov, Andrei
3
2001
How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. Zbl 1171.03308
Voronkov, Andrei
2
2001
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 1049.68120
Degtyarev, Anatoli; Gurevich, Yuri; 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
1
2000
Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem. Zbl 0937.03020
Voronkov, Andrei
3
1999
Monadic simultaneous rigid \(E\)-unification. Zbl 0930.03007
Gurevich, Yuri; Voronkov, Andrei
1
1999
A nondeterministic polynomial-time unification algorithm for bags, sets and trees. Zbl 0942.68023
Dantsin, Evgenyi; Voronkov, Andrei
1
1999
What you always wanted to know about rigid \(E\)-unification. Zbl 0893.68135
Degtyarev, Anatoli; Voronkov, Andrei
8
1998
Herbrand’s theorem, automated reasoning and semantic tableaux. Zbl 0945.03553
Voronkov, Andrei
4
1998
The decidability of simultaneous rigid \(E\)-unification with one variable. Zbl 0903.03007
Degtyarev, Anatoli; Gurevich, Yuri; Narendran, Paliath; Veanes, Margus; Voronkov, Andrei
4
1998
Elimination of equality via transformation with ordering constraints. Zbl 0926.03006
Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei
3
1998
Proof search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 0921.03012
Voronkov, Andrei
3
1998
Monadic simultaneous rigid \(E\)-unification and related problems. Zbl 1401.03037
Gurevich, Yuri; Voronkov, Andrei
6
1997
The undecidability of simultaneous rigid E-unification. Zbl 0872.68173
Degtyarev, Anatoli; Voronkov, Andrei
15
1996
Herbrand’s theorem and equational reasoning: Problems and solutions. Zbl 0866.68102
Degtyarev, Anatoli; Gurevich, Yuri; Voronkov, Andrei
7
1996
Proof-search in intuitionistic logic based on constraint satisfaction. Zbl 1415.03010
Voronkov, Andrei
6
1996
Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification. Zbl 1415.03011
Voronkov, Andrei
4
1996
A note on semantics of logic programs with equality based on complete sets of \(E\)-unifiers. Zbl 0874.68058
Degtyarev, Anatoli; Voronkov, Andrei
2
1996
The anatomy of vampire. Implementing bottom-up procedures with code trees. Zbl 0838.68100
Voronkov, Andrei
10
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
3
1992
all top 5

Cited by 456 Authors

24 Voronkov, Andrei
14 Urban, Josef
10 Kaliszyk, Cezary
8 Paulson, Lawrence Charles
8 Tinelli, Cesare
7 Blanchette, Jasmin Christian
7 Bonacina, Maria Paola
7 Sutcliffe, Geoff
7 Weidenbach, Christoph
6 Benzmüller, Christoph Ewald
6 Middeldorp, Aart
5 Böhme, Sascha
5 Degtyarev, Anatoli Ivanovich
5 Reynolds, Andrew
5 Schmidt, Renate A.
5 Veanes, Margus
4 Barrett, Clark W.
4 Baumgartner, Peter
4 Brown, Chad Edward
4 de Moura, Leonardo
4 Dixon, Clare
4 Djelloul, Khalil
4 Gurevich, Yuri
4 Konev, Boris
4 Korovin, Konstantin
4 Plaisted, David Alan
4 Ranise, Silvio
4 Rümmer, Philipp
4 Sofronie-Stokkermans, Viorica
3 Backeman, Peter
3 Biere, Armin
3 Bjørner, Nikolaj S.
3 Ghilardi, Silvio
3 Goubault-Larrecq, Jean
3 Hillenbrand, Thomas
3 Hirokawa, Nao
3 Hustadt, Ullrich
3 Johansson, Moa
3 Kovács, Laura Ildikó
3 Kühlwein, Daniel
3 Lyaletski, Alexander V.
3 Lynch, Christopher A.
3 Maksimova, Larisa L’vovna
3 Meier, Andreas
3 Meng, Jia
3 Nipkow, Tobias
3 Rabe, Florian
3 Reger, Giles
3 Schulz, Stephan
3 Sorge, Volker
3 Vyskočil, Jiří
3 Winkler, Sarah
3 Woltzenlogel Paleo, Bruno
3 Zankl, Harald
2 Alama, Jesse
2 Areces, Carlos
2 Berglund, Martin
2 Bozzelli, Laura
2 Bringsjord, Selmer
2 Bruttomesso, Roberto
2 Bultan, Tevfik
2 Chaudhuri, Kaustuv
2 Chen, Shuwei
2 Cheney, James
2 Egly, Uwe
2 Färber, Michael
2 Fisher, Michael W.
2 Fontaine, Pascal
2 Furbach, Ulrich
2 Furia, Carlo Alberto
2 Galmiche, Didier
2 Ghorani, Maryam
2 Gorín, Daniel
2 He, Xingxing
2 Hoder, Kryštof
2 Horrocks, Ian
2 Ibarra, Oscar H.
2 Janičić, Predrag
2 Jovanović, Dejan
2 Kapur, Deepak
2 Kiesl, Benjamin
2 Kohlhase, Michael
2 Kruglov, Evgeniĭ Valentinovich
2 Kuncak, Viktor
2 Leroux, Jérôme
2 Liang, Tianyi
2 Liu, Jun
2 Meseguer Guaita, José
2 Meyer, Bertrand
2 Moskal, Michał
2 Motik, Boris
2 Nicolini, Enrica
2 Nieuwenhuis, Robert
2 Paskevich, Andrei
2 Peltier, Nicolas
2 Pelzer, Björn
2 Pfenning, Frank
2 Pinchinat, Sophie
2 Piskac, Ruzica
2 Rendsvig, Rasmus Kræmmer
...and 356 more Authors
all top 5

Cited in 51 Serials

48 Journal of Automated Reasoning
13 Theoretical Computer Science
13 Information and Computation
13 Journal of Applied Logic
11 Journal of Symbolic Computation
8 Artificial Intelligence
8 Formal Methods in System Design
8 Annals of Mathematics and Artificial Intelligence
7 Theory and Practice of Logic Programming
6 Studia Logica
5 Journal of Logical and Algebraic Methods in Programming
4 Formal Aspects of Computing
3 Information Processing Letters
3 ACM Transactions on Computational Logic
3 Mathematics in Computer Science
3 Logical Methods in Computer Science
2 Applied Mathematics and Computation
2 Information Sciences
2 The Journal of Symbolic Logic
2 New Generation Computing
2 Journal of Logic, Language and Information
2 Journal of Mathematical Sciences (New York)
2 Soft Computing
1 ACM Computing Surveys
1 Acta Informatica
1 Lithuanian Mathematical Journal
1 Algebra and Logic
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 Journal of Computer Science and Technology
1 MSCS. Mathematical Structures in Computer Science
1 Archive for Mathematical Logic
1 Applicable Algebra in Engineering, Communication and Computing
1 Cybernetics and Systems Analysis
1 Journal of Applied Non-Classical Logics
1 Constraints
1 Higher-Order and Symbolic Computation
1 LMS Journal of Computation and Mathematics
1 The Journal of Logic and Algebraic Programming
1 Iranian Journal of Fuzzy Systems
1 Sibirskie Èlektronnye Matematicheskie Izvestiya
1 Proceedings of the Steklov Institute of Mathematics
1 Logica Universalis
1 The Review of Symbolic Logic
1 Studies in History and Philosophy of Science. Part B. Studies in History and Philosophy of Modern Physics
1 Science China. Information Sciences
1 Revista de la Real Academia de Ciencias Exactas, Físicas y Naturales. Serie A: Matemáticas. RACSAM
1 Izvestiya Irkutskogo Gosudarstvennogo Universiteta. Seriya Matematika

Citations by Year