Andrei Voronkov

251 papers A* 24A 41B 45C 5Misc 9Journal 37Unranked 55

Year	Rank	Type	Title / Venue / Authors
2025	A	`conf`	Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. CADE Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel
2025	A	`conf`	Partial Redundancy in Saturation. CADE Márton Hajdú, Laura Kovács, Andrei Voronkov
2025	J	`jnl`	Partial Redundancy in Saturation. CoRR Márton Hajdú, Laura Kovács, Andrei Voronkov
2025	C	`conf`	Synthesis Benchmarks for Automated Reasoning. CICM Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, Richard Steven Zilincík
2025	J	`jnl`	Synthesis Benchmarks for Automated Reasoning. CoRR Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, Richard Steven Zilincík
2025	A	`conf`	Term Ordering Diagrams. CADE Márton Hajdú, Robin Coutelier, Laura Kovács, Andrei Voronkov
2025	J	`jnl`	Term Ordering Diagrams. CoRR Márton Hajdú, Robin Coutelier, Laura Kovács, Andrei Voronkov
2025	—	`conf`	The Vampire Diary. CAV (3) Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2025	J	`jnl`	The Vampire Diary. CoRR Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
2024	J	`jnl`	Getting Saturated with Induction. CoRR Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov
2024	—	`conf`	Induction in Saturation. IJCAR (1) Laura Kovács, Petra Hozzová, Márton Hajdú, Andrei Voronkov
2024	—	`ed.`	LPAR 2024 Complementary Volume, Port Louis, Mauritius, May 26-31, 2024 LPAR Complementary Volume Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov
2024	B	`ed.`	LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024 LPAR Nikolaj S. Bjørner, Marijn Heule, Andrei Voronkov
2024	J	`jnl`	Program Synthesis in Saturation. CoRR Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov
2024	—	`conf`	Reducibility Constraints in Superposition. IJCAR (1) Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
2024	—	`conf`	Synthesis of Recursive Programs in Saturation. IJCAR (1) Petra Hozzová, Daneshvar Amrollahi, Márton Hajdú, Laura Kovács, Andrei Voronkov, Eva Maria Wagner
2023	—	`conf`	ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov
2023	B	`ed.`	LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. LPAR Ruzica Piskac, Andrei Voronkov
2023	A	`conf`	Program Synthesis in Saturation. CADE Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov
2022	—	`conf`	Getting Saturated with Induction. Principles of Systems Design Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov
2022	—	`conf`	The Vampire Approach to Induction (short paper). PAAR@IJCAR Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
2021	B	`conf`	Induction with Recursive Definitions in Superposition. FMCAD Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov
2021	C	`conf`	Inductive Benchmarks for Automated Reasoning. CICM Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov
2021	A	`conf`	Integer Induction in Saturation. CADE Petra Hozzová, Laura Kovács, Andrei Voronkov
2021	—	`conf`	Making Theory Reasoning Simpler. TACAS (2) Giles Reger, Johannes Schoisswohl, Andrei Voronkov
2020	C	`conf`	Induction with Generalization in Superposition Reasoning. CICM Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov
2019	A	`conf`	Induction in Saturation-Based Proof Search. CADE Giles Reger, Andrei Voronkov
2019	—	`ed.`	Perspectives of System Informatics - 12th International Andrei P. Ershov Informatics Conference, PSI 2019, Novosibirsk, Russia, July 2-5, 2019, Revised Selected Papers Ershov Informatics Conference Nikolaj S. Bjørner, Irina B. Virbitskaite, Andrei Voronkov
2019	—	`ed.`	Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops Vampire Laura Kovács, Andrei Voronkov
2018	A	`conf`	A FOOLish Encoding of the Next State Relations of Imperative Programs. IJCAR Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
2018	—	`ed.`	Perspectives of System Informatics - 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers Ershov Informatics Conference Alexander K. Petrenko, Andrei Voronkov
2018	Misc	`conf`	Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning. SYNASC Andrei Voronkov
2018	—	`conf`	Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS (1) Giles Reger, Martin Suda, Andrei Voronkov
2017	A*	`conf`	Coming to terms with quantified reasoning. POPL Laura Kovács, Simon Robillard, Andrei Voronkov
2017	B	`conf`	First-Order Interpolation and Interpolating Proof Systems. LPAR Laura Kovács, Andrei Voronkov
2017	—	`ed.`	IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017 LPAR (Short Presentations) Thomas Eiter, David Sands, Geoff Sutcliffe, Andrei Voronkov
2017	—	`conf`	Instantiation and Pretending to be an SMT Solver with Vampire. SMT Giles Reger, Martin Suda, Andrei Voronkov
2017	J	`jnl`	Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). CoRR Giles Reger, Martin Suda, Andrei Voronkov
2017	—	`conf`	Testing a Saturation-Based Theorem Prover: Experiences and Challenges. TAP@STAF Giles Reger, Martin Suda, Andrei Voronkov
2017	—	`ed.`	Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016. Vampire@IJCAR Laura Kovács, Andrei Voronkov
2016	—	`conf`	A Clausal Normal Form Translation for FOOL. GCAI Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
2016	—	`conf`	AVATAR Modulo Theories. GCAI Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov
2016	J	`jnl`	Coming to Terms with Quantified Reasoning. CoRR Laura Kovács, Simon Robillard, Andrei Voronkov
2016	J	`jnl`	Finding Finite Models in Multi-Sorted First Order Logic. CoRR Giles Reger, Martin Suda, Andrei Voronkov
2016	A	`conf`	Finding Finite Models in Multi-sorted First-Order Logic. SAT Giles Reger, Martin Suda, Andrei Voronkov
2016	—	`conf`	New Techniques in Clausal Form Generation. GCAI Giles Reger, Martin Suda, Andrei Voronkov
2016	—	`ed.`	Perspectives of System Informatics - 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers Ershov Memorial Conference Manuel Mazzara, Andrei Voronkov
2016	—	`ed.`	Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015 Vampire Laura Kovács, Andrei Voronkov
2016	A	`conf`	Selecting the Selection. IJCAR Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
2016	J	`jnl`	Selecting the Selection. CoRR Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder
2016	B	`conf`	The vampire and the FOOL. CPP Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov
2015	—	`ed.`	20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015. LPAR (short papers) Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, Andrei Voronkov
2015	C	`conf`	A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CICM Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
2015	J	`jnl`	A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CoRR Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
2015	A	`conf`	Cooperating Proof Attempts. CADE Giles Reger, Dmitry Tishkovsky, Andrei Voronkov
2015	—	`ed.`	Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015 GCAI Georg Gottlob, Geoff Sutcliffe, Andrei Voronkov
2015	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings LPAR Martin Davis, Ansgar Fehnker, Annabelle McIver, Andrei Voronkov
2015	—	`ed.`	Perspectives of System Informatics - 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Revised Selected Papers Ershov Memorial Conference Andrei Voronkov, Irina B. Virbitskaite
2015	A	`conf`	Playing with AVATAR. CADE Giles Reger, Martin Suda, Andrei Voronkov
2015	J	`jnl`	The Vampire and the FOOL. CoRR Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov
2014	—	`ed.`	6th International Symposium on Symbolic Computation in Software Science, SCSS 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014 SCSS Temur Kutsia, Andrei Voronkov
2014	A*	`conf`	AVATAR: The Architecture for First-Order Theorem Provers. CAV Andrei Voronkov
2014	—	`conf`	Experimenting with SAT Solvers in Vampire. MICAI (1) Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
2014	B	`conf`	Extensional Crisis and Proving Identity. ATVA Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov
2014	—	`book`	HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday Andrei Voronkov, Margarita V. Korovina
2014	A*	`conf`	Keynote talk: EasyChair. ASE Andrei Voronkov
2014	—	`ed.`	LPAR 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch, South Africa, Short papers proceedings LPAR (short papers) Kenneth L. McMillan, Aart Middeldorp, Geoff Sutcliffe, Andrei Voronkov
2014	—	`ed.`	PSI 2014. Ershov Informatics Conference, June 24-27, 2014, Peterhof, St. Petersburg, Russia, Poster Presentations Ershov Memorial Conference (Posters) Irina B. Virbitskaite, Andrei Voronkov
2014	—	`conf`	SAT solving experiments in Vampire. Vampire Workshop Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
2014	—	`conf`	The Challenges of Evaluating a New Feature in Vampire. Vampire Workshop Giles Reger, Martin Suda, Andrei Voronkov
2013	Misc	`conf`	Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov
2013	A*	`conf`	First-Order Theorem Proving and Vampire. CAV Laura Kovács, Andrei Voronkov
2013	—	`conf`	Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm
2013	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings LPAR Kenneth L. McMillan, Aart Middeldorp, Andrei Voronkov
2013	B	`conf`	PDFX: fully-automated PDF-to-XML conversion of scientific literature. ACM Symposium on Document Engineering Alexandru Constantin, Steve Pettifer, Andrei Voronkov
2013	—	`conf`	Planning with Effectively Propositional Logic. Programming Logics Juan Antonio Navarro Pérez, Andrei Voronkov
2013	—	`ed.`	Programming Logics - Essays in Memory of Harald Ganzinger Programming Logics Andrei Voronkov, Christoph Weidenbach
2013	—	`ed.`	Short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta, Indonesia, October 10-15, 2010 LPAR short papers(Yogyakarta) Andrei Voronkov, Geoff Sutcliffe, Matthias Baaz, Christian G. Fermüller
2013	A	`conf`	The 481 Ways to Split a Clause and Deal with Propositional Variables. CADE Krystof Hoder, Andrei Voronkov
2013	—	`conf`	The Inverse Method for Many-Valued Logics. MICAI (1) Laura Kovács, Andrei Mantsivoda, Andrei Voronkov
2012	Misc	`ed.`	14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, Timisoara, Romania, September 26-29, 2012 SYNASC Andrei Voronkov, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, Daniela Zaharie
2012	A	`conf`	EPR-Based Bounded Model Checking at Word Level. IJCAR Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov
2012	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings LPAR Nikolaj S. Bjørner, Andrei Voronkov
2012	—	`ed.`	Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers Ershov Memorial Conference Edmund M. Clarke, Irina B. Virbitskaite, Andrei Voronkov
2012	A*	`conf`	Playing in the grey area of proofs. POPL Krystof Hoder, Laura Kovács, Andrei Voronkov
2012	B	`conf`	Preprocessing techniques for first-order clausification. FMCAD Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
2012	—	`ed.`	Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 and Third International Workshop on Invariant Generation, WING 2010, Edinburgh, UK, July 21, 2010 WING@ETAPS/IJCAR Andrei Voronkov, Laura Kovács, Nikolaj S. Bjørner
2012	J	`jnl`	Translating regular expression matching into transducers. J. Appl. Log. Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov
2012	—	`ed.`	Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25, 2012 Turing-100 Andrei Voronkov
2012	B	`conf`	Vinter: A Vampire-Based Tool for Interpolation. APLAS Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov
2011	—	`conf`	Case Studies on Invariant Generation Using a Saturation Theorem Prover. MICAI (1) Krystof Hoder, Laura Kovács, Andrei Voronkov
2011	J	`jnl`	Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2011	—	`conf`	GoRRiLA and Hard Reality. Ershov Memorial Conference Konstantin Korovin, Andrei Voronkov
2011	—	`conf`	Implementing Conflict Resolution. Ershov Memorial Conference Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
2011	A	`conf`	Invariant Generation in Vampire. TACAS Krystof Hoder, Laura Kovács, Andrei Voronkov
2011	A	`conf`	On Transfinite Knuth-Bendix Orders. CADE Laura Kovács, Georg Moser, Andrei Voronkov
2011	A	`conf`	Sine Qua Non for Large Theory Reasoning. CADE Krystof Hoder, Andrei Voronkov
2011	A	`conf`	Solving Systems of Linear Inequalities by Bound Propagation. CADE Konstantin Korovin, Andrei Voronkov
2010	—	`conf`	10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	—	`conf`	10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	—	`ed.`	Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010 Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	—	`conf`	EasyChair. WWV Andrei Voronkov
2010	B	`conf`	Encoding industrial hardware verification problems into effectively propositional logic. FMCAD Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
2010	—	`conf`	Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. ICMS Josef Urban, Krystof Hoder, Andrei Voronkov
2010	A	`conf`	Interpolation and Symbol Elimination in Vampire. IJCAR Krystof Hoder, Laura Kovács, Andrei Voronkov
2010	B	`conf`	Invariant and Type Inference for Matrices. VMCAI Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov
2010	—	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers LPAR (Dakar) Edmund M. Clarke, Andrei Voronkov
2010	—	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings LPAR (Yogyakarta) Christian G. Fermüller, Andrei Voronkov
2010	—	`ed.`	Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers Ershov Memorial Conference Amir Pnueli, Irina B. Virbitskaite, Andrei Voronkov
2010	Misc	`conf`	Translating Regular Expression Matching into Transducers. SYNASC Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov
2009	Misc	`conf`	Comparing Unification Algorithms in First-Order Theorem Proving. KI Krystof Hoder, Andrei Voronkov
2009	A	`conf`	Conflict Resolution. CP Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
2009	B	`conf`	Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. FASE Laura Kovács, Andrei Voronkov
2009	Misc	`conf`	Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. SYNASC Laura Kovács, Andrei Voronkov
2009	B	`conf`	Inter-program Properties. SAS Andrei Voronkov, Iman Narasamdya
2009	A	`conf`	Interpolation and Symbol Elimination. CADE Laura Kovács, Andrei Voronkov
2009	A	`conf`	Path Feasibility Analysis for String-Manipulating Programs. TACAS Nikolaj S. Bjørner, Nikolai Tillmann, Andrei Voronkov
2009	Misc	`conf`	Satisfiability and Theories. SYNASC Andrei Voronkov
2009	B	`conf`	Verifying equivalence of memories using a first order logic theorem prover. FMCAD Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov
2008	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings LPAR Iliano Cervesato, Helmut Veith, Andrei Voronkov
2008	A	`conf`	Proof Systems for Effectively Propositional Logic. IJCAR Juan Antonio Navarro Pérez, Andrei Voronkov
2008	—	`ed.`	Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings RTA Andrei Voronkov
2007	Misc	`ed.`	Computer Science - Theory and Applications, Second International Symposium on Computer Science in Russia, CSR 2007, Ekaterinburg, Russia, September 3-7, 2007, Proceedings CSR Volker Diekert, Mikhail V. Volkov, Andrei Voronkov
2007	A	`conf`	Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. CADE Juan Antonio Navarro Pérez, Andrei Voronkov
2007	A	`conf`	Encodings of Problems in Effectively Propositional Logic. SAT Juan Antonio Navarro Pérez, Andrei Voronkov
2007	B	`conf`	Integrating Linear Arithmetic into Superposition Calculus. CSL Konstantin Korovin, Andrei Voronkov
2007	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings LPAR Nachum Dershowitz, Andrei Voronkov
2007	—	`ed.`	Perspectives of Systems Informatics, 6th International Andrei Ershov Memorial Conference, PSI 2006, Novosibirsk, Russia, June 27-30, 2006. Revised Papers Ershov Memorial Conference Irina B. Virbitskaite, Andrei Voronkov
2006	—	`ed.`	Deduction and Applications, 23.-28. October 2005 Deduction and Applications Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
2006	C	`conf`	Implementation of UNIDOOR, a Deductive Object-Oriented Database System. ADBIS Mohammed K. Jaber, Andrei Voronkov
2006	B	`conf`	Inconsistencies in Ontologies. JELIA Andrei Voronkov
2006	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings LPAR Miki Hermann, Andrei Voronkov
2006	—	`conf`	Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. FoIKS Ian Horrocks, Andrei Voronkov
2006	A*	`conf`	UNIDOOR: a Deductive Object-Oriented Database Management System. ICDE Mohammed K. Jaber, Andrei Voronkov
2005	—	`conf`	05431 Abstracts Collection - Deduction and Applications. Deduction and Applications Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
2005	—	`conf`	05431 Executive Summary - Deduction and Applications. Deduction and Applications Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
2005	B	`conf`	Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. MFCS Dimitri Chubarov, Andrei Voronkov
2005	J	`jnl`	Efficient instance retrieval with standard and relational path indexing. Inf. Comput. Alexandre Riazanov, Andrei Voronkov
2005	B	`conf`	Finding Basic Block and Variable Correspondence. SAS Iman Narasamdya, Andrei Voronkov
2005	A*	`conf`	Generation of Hard Non-Clausal Random Satisfiability Problems. AAAI Juan Antonio Navarro Pérez, Andrei Voronkov
2005	J	`jnl`	Knuth-Bendix constraint solving is NP-complete. ACM Trans. Comput. Log. Konstantin Korovin, Andrei Voronkov
2005	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings LPAR Franz Baader, Andrei Voronkov
2005	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings LPAR Geoff Sutcliffe, Andrei Voronkov
2005	B	`conf`	Random Databases and Threshold for Monotone Non-recursive Datalog. MFCS Konstantin Korovin, Andrei Voronkov
2005	—	`conf`	Solving First-Order Constraints over the Monadic Class. Mechanizing Mathematical Reasoning Dimitri Chubarov, Andrei Voronkov
2004	A	`conf`	Efficient Checking of Term Ordering Constraints. IJCAR Alexandre Riazanov, Andrei Voronkov
2004	A	`conf`	TeMP: A Temporal Monodic Prover. IJCAR Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov
2003	—	`conf`	A Logical Reconstruction of Reachability. Ershov Memorial Conference Tatiana Rybina, Andrei Voronkov
2003	A	`conf`	An AC-Compatible Knuth-Bendix Order. CADE Konstantin Korovin, Andrei Voronkov
2003	A*	`conf`	Automated Reasoning: Past Story and New Trends. IJCAI Andrei Voronkov
2003	B	`conf`	Complexity of Some Problems in Modal and Intuitionistic Calculi. CSL Larisa Maksimova, Andrei Voronkov
2003	A	`conf`	Efficient Instance Retrieval with Standard and Relational Path Indexing. CADE Alexandre Riazanov, Andrei Voronkov
2003	B	`conf`	Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture). CSL Tatiana Rybina, Andrei Voronkov
2003	J	`jnl`	Limited resource strategy in resolution theorem proving. J. Symb. Comput. Alexandre Riazanov, Andrei Voronkov
2003	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings LPAR Moshe Y. Vardi, Andrei Voronkov
2003	A*	`conf`	Orienting Equalities with the Knuth-Bendix Order. LICS Konstantin Korovin, Andrei Voronkov
2003	J	`jnl`	Orienting rewrite rules with the Knuth-Bendix order. Inf. Comput. Konstantin Korovin, Andrei Voronkov
2003	J	`jnl`	Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. J. Autom. Reason. Andrei Voronkov
2003	J	`jnl`	Stratified resolution. J. Symb. Comput. Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov
2003	A*	`conf`	Upper Bounds for a Theory of Queues. ICALP Tatiana Rybina, Andrei Voronkov
2002	A	`ed.`	Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings CADE Andrei Voronkov
2002	—	`conf`	BRAIN : Backward Reachability Analysis with Integers. AMAST Tatiana Rybina, Andrei Voronkov
2002	—	`conf`	First-Order Theorem Provers: the Next Generation. Description Logics Andrei Voronkov
2002	J	`jnl`	Knuth-Bendix constraint solving is NP-complete CoRR Konstantin Korovin, Andrei Voronkov
2002	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Proceedings LPAR Matthias Baaz, Andrei Voronkov
2002	—	`conf`	The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. FSTTCS Konstantin Korovin, Andrei Voronkov
2002	J	`jnl`	The design and implementation of VAMPIRE. AI Commun. Alexandre Riazanov, Andrei Voronkov
2002	A*	`conf`	Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. CAV Tatiana Rybina, Andrei Voronkov
2001	J	`jnl`	A decision procedure for term algebras with queues. ACM Trans. Comput. Log. Tatiana Rybina, Andrei Voronkov
2001	—	`conf`	Adaptive Saturation-Based Reasoning. Ershov Memorial Conference Alexandre Riazanov, Andrei Voronkov
2001	A	`conf`	Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. IJCAR Andrei Voronkov
2001	J	`jnl`	Complexity and expressive power of logic programming. ACM Comput. Surv. Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov
2001	—	`ch.`	Equality Reasoning in Sequent-Based Calculi. Handbook of Automated Reasoning Anatoli Degtyarev, Andrei Voronkov
2001	—	`book`	Handbook of Automated Reasoning (in 2 volumes) John Alan Robinson, Andrei Voronkov
2001	—	`ch.`	Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Current Trends in Theoretical Computer Science Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov
2001	J	`jnl`	How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Trans. Comput. Log. Andrei Voronkov
2001	A*	`conf`	Knuth-Bendix Constraint Solving Is NP-Complete. ICALP Konstantin Korovin, Andrei Voronkov
2001	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings LPAR Robert Nieuwenhuis, Andrei Voronkov
2001	A	`conf`	On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov
2001	—	`ch.`	Preface. Handbook of Automated Reasoning John Alan Robinson, Andrei Voronkov
2001	A*	`conf`	Splitting Without Backtracking. IJCAI Alexandre Riazanov, Andrei Voronkov
2001	—	`ch.`	Term Indexing. Handbook of Automated Reasoning I. V. Ramakrishnan, R. Sekar, Andrei Voronkov
2001	J	`jnl`	Term-Modal Logics. Stud Logica Melvin Fitting, Lars Thalmann, Andrei Voronkov
2001	—	`ch.`	The Inverse Method. Handbook of Automated Reasoning Anatoli Degtyarev, Andrei Voronkov
2001	A	`conf`	Vampire 1.1 (System Description). IJCAR Alexandre Riazanov, Andrei Voronkov
2001	—	`conf`	Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. RTA Konstantin Korovin, Andrei Voronkov
2000	—	`conf`	A Decision Procedure for Term Algebras with Queues. ARW Tatiana Rybina, Andrei Voronkov
2000	A*	`conf`	A Decision Procedure for Term Algebras with Queues. LICS Tatiana Rybina, Andrei Voronkov
2000	A*	`conf`	A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. LICS Konstantin Korovin, Andrei Voronkov
2000	J	`jnl`	Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Theor. Comput. Sci. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
2000	A*	`conf`	Deciding K using inverse-K. KR Andrei Voronkov
2000	A*	`conf`	Expressive Power and Data Complexity of Query Languages for Trees and Lists. PODS Evgeny Dantsin, Andrei Voronkov
2000	A*	`conf`	How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. LICS Andrei Voronkov
2000	B	`ed.`	Logic for Programming and Automated Reasoning, 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000, Proceedings LPAR Michel Parigot, Andrei Voronkov
2000	B	`conf`	Partially Adaptive Code Trees. JELIA Alexandre Riazanov, Andrei Voronkov
2000	A	`conf`	Stratified Resolution. CADE Anatoli Degtyarev, Andrei Voronkov
2000	—	`conf`	System Description: Vampire 1.0. ARW Alexandre Riazanov, Andrei Voronkov
2000	B	`conf`	Term-Modal Logics. TABLEAUX Melvin Fitting, Lars Thalmann, Andrei Voronkov
2000	—	`conf`	The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. ARW Konstantin Korovin, Andrei Voronkov
1999	B	`conf`	A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees. FoSSaCS Evgeny Dantsin, Andrei Voronkov
1999	A	`conf`	KK: a theorem prover for K. CADE Andrei Voronkov
1999	B	`ed.`	Logic Programming and Automated Reasoning, 6th International Conference, LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings LPAR Harald Ganzinger, David A. McAllester, Andrei Voronkov
1999	J	`jnl`	Monadic Simultaneous Rigid E-unification. Theor. Comput. Sci. Yuri Gurevich, Andrei Voronkov
1999	J	`jnl`	Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem. Theor. Comput. Sci. Andrei Voronkov
1999	J	`jnl`	The Ground-Negative Fragment of First-Order Logic Is Pi J. Symb. Log. Andrei Voronkov
1999	A	`conf`	Vampire. CADE Alexandre Riazanov, Andrei Voronkov
1998	A*	`conf`	Complexity of Nonrecursive Logic Programs with Complex Values. PODS Sergei G. Vorobyov, Andrei Voronkov
1998	A	`conf`	Elimination of Equality via Transformation with Ordering Constraints. CADE Leo Bachmair, Harald Ganzinger, Andrei Voronkov
1998	A*	`conf`	Herbrand's Theorem, Automated Reasoning and Semantics Tableaux. LICS Andrei Voronkov
1998	J	`jnl`	Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid J. Autom. Reason. Andrei Voronkov
1998	—	`conf`	The Decidability of Simultaneous Rigid RTA Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov
1998	—	`ed.`	Transactions and Change in Logic Databases, International Seminar on Logic Databases and the Meaning of Change, Schloss Dagstuhl, Germany, September 23-27, 1996 and ILPS '97 Post-Conference Workshop on (Trans)Actions and Change in Logic Programming and Deductive Databases, (DYNAMICS'97) Port Jefferson, NY, USA, October 17, 1997, Invited Surveys and Selected Papers Transactions and Change in Logic Databases Burkhard Freitag, Hendrik Decker, Michael Kifer, Andrei Voronkov
1998	J	`jnl`	What You Always Wanted to Know about Rigid E-Unification. J. Autom. Reason. Anatoli Degtyarev, Andrei Voronkov
1997	A	`conf`	Complexity and Expressive Power of Logic Programming. CCC Evgeny Dantsin, Thomas Eiter, Georg Gottlob, Andrei Voronkov
1997	Misc	`conf`	Complexity of Query Answering in Logic Databases with Complex Values. LFCS Evgeny Dantsin, Andrei Voronkov
1997	A*	`conf`	Monadic Simultaneous Rigid E-Unification and Related Problems. ICALP Yuri Gurevich, Andrei Voronkov
1997	—	`conf`	Strategies in Rigid-Variable Methods. IJCAI (1) Andrei Voronkov
1996	J	`jnl`	A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers. J. Log. Program. Anatoli Degtyarev, Andrei Voronkov
1996	A*	`conf`	Decidability Problems for the Prenex Fragment of Intuitionistic Logic. LICS Anatoli Degtyarev, Andrei Voronkov
1996	—	`conf`	Equality Elimination for the Tableau Method. DISCO Anatoli Degtyarev, Andrei Voronkov
1996	—	`conf`	Handling Equality in Logic Programming via Basic Folding. ELP Anatoli Degtyarev, Andrei Voronkov
1996	J	`jnl`	Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Bull. EATCS Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov
1996	—	`conf`	Merging Relational Database Technology with Constraint Technology. Ershov Memorial Conference Andrei Voronkov
1996	B	`conf`	Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction. TABLEAUX Andrei Voronkov
1996	A	`conf`	Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. CADE Andrei Voronkov
1996	—	`conf`	Semantics of Constraint Logic Programs with Bounded Quantifiers. ELP Martin Argenius, Andrei Voronkov
1996	A*	`conf`	Simultaneous E-Unification and Related Algorithmic Problems. LICS Anatoli Degtyarev, Yuri V. Matiyasevich, Andrei Voronkov
1996	J	`jnl`	The Undecidability of Simultaneous Rigid E-Unification. Theor. Comput. Sci. Anatoli Degtyarev, Andrei Voronkov
1996	B	`conf`	What You Always Wanted to Know About Rigid E-Unification. JELIA Anatoli Degtyarev, Andrei Voronkov
1995	B	`conf`	A New Procedural Interpretation of Horn Clauses with Equality. ICLP Anatoli Degtyarev, Andrei Voronkov
1995	A*	`conf`	Equality Elimination for the Inverse Method and Extension Procedures. IJCAI Anatoli Degtyarev, Andrei Voronkov
1995	—	`conf`	General Connections via Equality Elimination. WOCFAI Anatoli Degtyarev, Andrei Voronkov
1995	J	`jnl`	On Computability by Logic Programs. Ann. Math. Artif. Intell. Andrei Voronkov
1995	B	`conf`	Simultaneous Regid E-Unification Is Undecidable. CSL Anatoli Degtyarev, Andrei Voronkov
1995	J	`jnl`	The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees. J. Autom. Reason. Andrei Voronkov
1994	—	`conf`	An Implementation Technique for a Class of Bottom-Up Procedures. PLILP Andrei Voronkov
1993	—	`conf`	A Construction of Typed Lambda Models Related to Feasible Computability. Kurt Gödel Colloquium Vladimir Yu. Sazonov, Andrei Voronkov
1993	B	`ed.`	Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings LPAR Andrei Voronkov
1992	—	`conf`	Higher Order Functions in First Order Theory. ISTCS Andrei Voronkov
1992	B	`ed.`	Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings LPAR Andrei Voronkov
1992	—	`ed.`	Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990 - Second Russian Conference on Logic Programming, St. Petersburg, Russia, September 11-16, 1991, Proceedings RCLP Andrei Voronkov
1992	—	`conf`	On Computability by Logic Programs. Structural Complexity and Recursion-theoretic methods in Logic-Programming Andrei Voronkov
1992	A	`conf`	Theorem Proving in Non-Standard Logics Based on the Inverse Method. CADE Andrei Voronkov
1991	—	`conf`	Declarative and Procedural Paradigms - Do they Really Compete? (Panel). PDK Harold Boley, Micha Meier, Chris Moss, Michael M. Richter, Andrei Voronkov
1991	—	`conf`	Logic Programming with Bounded Quantifiers. RCLP Andrei Voronkov
1991	B	`conf`	On Completeness of Program Synthesis Systems. CSL Andrei Voronkov
1990	A	`conf`	LISS - The Logic Inference Search System. CADE Andrei Voronkov
1990	A	`conf`	Towards the Theory of Programming in Constructive Logic. ESOP Andrei Voronkov
1988	—	`conf`	A proof-search method for the first-order logic. Conference on Computer Logic Andrei Voronkov
1988	—	`conf`	On connections between classical and constructive semantics. Conference on Computer Logic Sergei Starchenko, Andrei Voronkov
1987	B	`conf`	Deductive Program Synthesis and Markov's Principle. FCT Andrei Voronkov