Search the dblp DataBase
Andrei Voronkov :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov Complexity and Expressive Power of Logic Programming. [Citation Graph (2, 0)][DBLP ] IEEE Conference on Computational Complexity, 1997, pp:82-101 [Conf ] Evgeny Dantsin , Andrei Voronkov Expressive Power and Data Complexity of Query Languages for Trees and Lists. [Citation Graph (1, 24)][DBLP ] PODS, 2000, pp:157-165 [Conf ] Sergei G. Vorobyov , Andrei Voronkov Complexity of Nonrecursive Logic Programs with Complex Values. [Citation Graph (1, 33)][DBLP ] PODS, 1998, pp:244-253 [Conf ] Juan A. Navarro , Andrei Voronkov Generation of Hard Non-Clausal Random Satisfiability Problems. [Citation Graph (0, 0)][DBLP ] AAAI, 2005, pp:436-442 [Conf ] Mohammed K. Jaber , Andrei Voronkov Implementation of UNIDOOR, a Deductive Object-Oriented Database System. [Citation Graph (0, 0)][DBLP ] ADBIS, 2006, pp:155-170 [Conf ] Tatiana Rybina , Andrei Voronkov BRAIN : Backward Reachability Analysis with Integers. [Citation Graph (0, 0)][DBLP ] AMAST, 2002, pp:489-494 [Conf ] Dimitri Chubarov , Andrei Voronkov Solving First-Order Constraints over the Monadic Class. [Citation Graph (0, 0)][DBLP ] Mechanizing Mathematical Reasoning, 2005, pp:132-138 [Conf ] Leo Bachmair , Harald Ganzinger , Andrei Voronkov Elimination of Equality via Transformation with Ordering Constraints. [Citation Graph (0, 0)][DBLP ] CADE, 1998, pp:175-190 [Conf ] Anatoli Degtyarev , Andrei Voronkov Stratified Resolution. [Citation Graph (0, 0)][DBLP ] CADE, 2000, pp:365-384 [Conf ] Ullrich Hustadt , Boris Konev , Alexandre Riazanov , Andrei Voronkov TeMP: A Temporal Monodic Prover. [Citation Graph (0, 0)][DBLP ] IJCAR, 2004, pp:326-330 [Conf ] Konstantin Korovin , Andrei Voronkov An AC-Compatible Knuth-Bendix Order. [Citation Graph (0, 0)][DBLP ] CADE, 2003, pp:47-59 [Conf ] Robert Nieuwenhuis , Thomas Hillenbrand , Alexandre Riazanov , Andrei Voronkov On the Evaluation of Indexing Techniques for Theorem Proving. [Citation Graph (0, 0)][DBLP ] IJCAR, 2001, pp:257-271 [Conf ] Alexandre Riazanov , Andrei Voronkov Vampire 1.1 (System Description). [Citation Graph (0, 0)][DBLP ] IJCAR, 2001, pp:376-380 [Conf ] Alexandre Riazanov , Andrei Voronkov Efficient Instance Retrieval with Standard and Relational Path Indexing. [Citation Graph (0, 0)][DBLP ] CADE, 2003, pp:380-396 [Conf ] Alexandre Riazanov , Andrei Voronkov Efficient Checking of Term Ordering Constraints. [Citation Graph (0, 0)][DBLP ] IJCAR, 2004, pp:60-74 [Conf ] Alexandre Riazanov , Andrei Voronkov Vampire. [Citation Graph (0, 0)][DBLP ] CADE, 1999, pp:292-296 [Conf ] Andrei Voronkov Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. [Citation Graph (0, 0)][DBLP ] IJCAR, 2001, pp:13-28 [Conf ] Andrei Voronkov LISS - The Logic Inference Search System. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:677-678 [Conf ] Andrei Voronkov Theorem Proving in Non-Standard Logics Based on the Inverse Method. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:648-662 [Conf ] Andrei Voronkov Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] CADE, 1996, pp:32-46 [Conf ] Andrei Voronkov KK: a theorem prover for K. [Citation Graph (0, 0)][DBLP ] CADE, 1999, pp:383-387 [Conf ] Tatiana Rybina , Andrei Voronkov Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. [Citation Graph (0, 0)][DBLP ] CAV, 2002, pp:386-400 [Conf ] Sergei Starchenko , Andrei Voronkov On connections between classical and constructive semantics. [Citation Graph (0, 0)][DBLP ] Conference on Computer Logic, 1988, pp:275-285 [Conf ] Andrei Voronkov A proof-search method for the first-order logic. [Citation Graph (0, 0)][DBLP ] Conference on Computer Logic, 1988, pp:327-338 [Conf ] Anatoli Degtyarev , Andrei Voronkov Simultaneous Regid E-Unification Is Undecidable. [Citation Graph (0, 0)][DBLP ] CSL, 1995, pp:178-190 [Conf ] Larisa Maksimova , Andrei Voronkov Complexity of Some Problems in Modal and Intuitionistic Calculi. [Citation Graph (0, 0)][DBLP ] CSL, 2003, pp:397-412 [Conf ] Tatiana Rybina , Andrei Voronkov Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture). [Citation Graph (0, 0)][DBLP ] CSL, 2003, pp:546-573 [Conf ] Andrei Voronkov On Completeness of Program Synthesis Systems. [Citation Graph (0, 0)][DBLP ] CSL, 1991, pp:411-418 [Conf ] Franz Baader , Peter Baumgartner , Robert Nieuwenhuis , Andrei Voronkov 05431 Executive Summary - Deduction and Applications. [Citation Graph (0, 0)][DBLP ] Deduction and Applications, 2005, pp:- [Conf ] Franz Baader , Peter Baumgartner , Robert Nieuwenhuis , Andrei Voronkov 05431 Abstracts Collection - Deduction and Applications. [Citation Graph (0, 0)][DBLP ] Deduction and Applications, 2005, pp:- [Conf ] Anatoli Degtyarev , Andrei Voronkov Equality Elimination for the Tableau Method. [Citation Graph (0, 0)][DBLP ] DISCO, 1996, pp:46-60 [Conf ] Martin Argenius , Andrei Voronkov Semantics of Constraint Logic Programs with Bounded Quantifiers. [Citation Graph (0, 0)][DBLP ] ELP, 1996, pp:1-18 [Conf ] Anatoli Degtyarev , Andrei Voronkov Handling Equality in Logic Programming via Basic Folding. [Citation Graph (0, 0)][DBLP ] ELP, 1996, pp:119-136 [Conf ] Alexandre Riazanov , Andrei Voronkov Adaptive Saturation-Based Reasoning. [Citation Graph (0, 0)][DBLP ] Ershov Memorial Conference, 2001, pp:95-108 [Conf ] Tatiana Rybina , Andrei Voronkov A Logical Reconstruction of Reachability. [Citation Graph (0, 0)][DBLP ] Ershov Memorial Conference, 2003, pp:222-237 [Conf ] Andrei Voronkov Merging Relational Database Technology with Constraint Technology. [Citation Graph (0, 0)][DBLP ] Ershov Memorial Conference, 1996, pp:409-419 [Conf ] Andrei Voronkov Towards the Theory of Programming in Constructive Logic. [Citation Graph (0, 0)][DBLP ] ESOP, 1990, pp:421-435 [Conf ] Andrei Voronkov Deductive Program Synthesis and Markov's Principle. [Citation Graph (0, 0)][DBLP ] FCT, 1987, pp:479-482 [Conf ] Ian Horrocks , Andrei Voronkov Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. [Citation Graph (0, 0)][DBLP ] FoIKS, 2006, pp:201-218 [Conf ] Evgeny Dantsin , Andrei Voronkov A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees. [Citation Graph (0, 0)][DBLP ] FoSSaCS, 1999, pp:180-196 [Conf ] Konstantin Korovin , Andrei Voronkov The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. [Citation Graph (0, 0)][DBLP ] FSTTCS, 2002, pp:230-240 [Conf ] Yuri Gurevich , Andrei Voronkov Monadic Simultaneous Rigid E-Unification and Related Problems. [Citation Graph (0, 0)][DBLP ] ICALP, 1997, pp:154-165 [Conf ] Konstantin Korovin , Andrei Voronkov Knuth-Bendix Constraint Solving Is NP-Complete. [Citation Graph (0, 0)][DBLP ] ICALP, 2001, pp:979-992 [Conf ] Tatiana Rybina , Andrei Voronkov Upper Bounds for a Theory of Queues. [Citation Graph (0, 0)][DBLP ] ICALP, 2003, pp:714-724 [Conf ] Mohammed K. Jaber , Andrei Voronkov UNIDOOR: a Deductive Object-Oriented Database Management System. [Citation Graph (0, 0)][DBLP ] ICDE, 2006, pp:157- [Conf ] Anatoli Degtyarev , Andrei Voronkov A New Procedural Interpretation of Horn Clauses with Equality. [Citation Graph (0, 0)][DBLP ] ICLP, 1995, pp:565-579 [Conf ] Andrei Voronkov On Computability by Logic Programs. [Citation Graph (0, 0)][DBLP ] Structural Complexity and Recursion-theoretic methods in Logic-Programming, 1992, pp:165-0 [Conf ] Anatoli Degtyarev , Andrei Voronkov Equality Elimination for the Inverse Method and Extension Procedures. [Citation Graph (0, 0)][DBLP ] IJCAI, 1995, pp:342-347 [Conf ] Alexandre Riazanov , Andrei Voronkov Splitting Without Backtracking. [Citation Graph (0, 0)][DBLP ] IJCAI, 2001, pp:611-617 [Conf ] Andrei Voronkov Automated Reasoning: Past Story and New Trends. [Citation Graph (0, 0)][DBLP ] IJCAI, 2003, pp:1607-1612 [Conf ] Andrei Voronkov Strategies in Rigid-Variable Methods. [Citation Graph (0, 0)][DBLP ] IJCAI (1), 1997, pp:114-121 [Conf ] Andrei Voronkov Higher Order Functions in First Order Theory. [Citation Graph (0, 0)][DBLP ] ISTCS, 1992, pp:43-54 [Conf ] Anatoli Degtyarev , Andrei Voronkov What You Always Wanted to Know About Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] JELIA, 1996, pp:50-69 [Conf ] Alexandre Riazanov , Andrei Voronkov Partially Adaptive Code Trees. [Citation Graph (0, 0)][DBLP ] JELIA, 2000, pp:209-223 [Conf ] Andrei Voronkov Inconsistencies in Ontologies. [Citation Graph (0, 0)][DBLP ] JELIA, 2006, pp:19- [Conf ] Vladimir Yu. Sazonov , Andrei Voronkov A Construction of Typed Lambda Models Related to Feasible Computability. [Citation Graph (0, 0)][DBLP ] Kurt Gödel Colloquium, 1993, pp:301-312 [Conf ] Andrei Voronkov Deciding K using inverse-K. [Citation Graph (0, 0)][DBLP ] KR, 2000, pp:198-209 [Conf ] Evgeny Dantsin , Andrei Voronkov Complexity of Query Answering in Logic Databases with Complex Values. [Citation Graph (0, 0)][DBLP ] LFCS, 1997, pp:56-66 [Conf ] Anatoli Degtyarev , Yuri Matiyasevich , Andrei Voronkov Simultaneous E-Unification and Related Algorithmic Problems. [Citation Graph (0, 0)][DBLP ] LICS, 1996, pp:494-502 [Conf ] Anatoli Degtyarev , Andrei Voronkov Decidability Problems for the Prenex Fragment of Intuitionistic Logic. [Citation Graph (0, 0)][DBLP ] LICS, 1996, pp:503-512 [Conf ] Konstantin Korovin , Andrei Voronkov A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. [Citation Graph (0, 0)][DBLP ] LICS, 2000, pp:291-302 [Conf ] Konstantin Korovin , Andrei Voronkov Orienting Equalities with the Knuth-Bendix Order. [Citation Graph (0, 0)][DBLP ] LICS, 2003, pp:75-0 [Conf ] Tatiana Rybina , Andrei Voronkov A Decision Procedure for Term Algebras with Queues. [Citation Graph (0, 0)][DBLP ] LICS, 2000, pp:279-290 [Conf ] Andrei Voronkov How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. [Citation Graph (0, 0)][DBLP ] LICS, 2000, pp:401-412 [Conf ] Andrei Voronkov Herbrand's Theorem, Automated Reasoning and Semantics Tableaux. [Citation Graph (0, 0)][DBLP ] LICS, 1998, pp:252-263 [Conf ] Andrei Voronkov Logic Programming with Bounded Quantifiers. [Citation Graph (0, 0)][DBLP ] RCLP, 1991, pp:486-514 [Conf ] Dimitri Chubarov , Andrei Voronkov Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. [Citation Graph (0, 0)][DBLP ] MFCS, 2005, pp:260-270 [Conf ] Konstantin Korovin , Andrei Voronkov Random Databases and Threshold for Monotone Non-recursive Datalog. [Citation Graph (0, 0)][DBLP ] MFCS, 2005, pp:591-602 [Conf ] Harold Boley , Micha Meier , Chris Moss , Michael M. Richter , Andrei Voronkov Declarative and Procedural Paradigms - Do they Really Compete? (Panel). [Citation Graph (0, 0)][DBLP ] PDK, 1991, pp:383-398 [Conf ] Andrei Voronkov An Implementation Technique for a Class of Bottom-Up Procedures. [Citation Graph (0, 0)][DBLP ] PLILP, 1994, pp:147-164 [Conf ] Anatoli Degtyarev , Yuri Gurevich , Paliath Narendran , Margus Veanes , Andrei Voronkov The Decidability of Simultaneous Rigid E -Unification with One Variable. [Citation Graph (0, 0)][DBLP ] RTA, 1998, pp:181-195 [Conf ] Konstantin Korovin , Andrei Voronkov Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. [Citation Graph (0, 0)][DBLP ] RTA, 2001, pp:137-153 [Conf ] Iman Narasamdya , Andrei Voronkov Finding Basic Block and Variable Correspondence. [Citation Graph (0, 0)][DBLP ] SAS, 2005, pp:251-267 [Conf ] Melvin Fitting , Lars Thalmann , Andrei Voronkov Term-Modal Logics. [Citation Graph (0, 0)][DBLP ] TABLEAUX, 2000, pp:220-236 [Conf ] Andrei Voronkov Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction. [Citation Graph (0, 0)][DBLP ] TABLEAUX, 1996, pp:312-329 [Conf ] Anatoli Degtyarev , Andrei Voronkov General Connections via Equality Elimination. [Citation Graph (0, 0)][DBLP ] WOCFAI, 1995, pp:109-120 [Conf ] Alexandre Riazanov , Andrei Voronkov The design and implementation of VAMPIRE. [Citation Graph (0, 0)][DBLP ] AI Commun., 2002, v:15, n:2-3, pp:91-110 [Journal ] Andrei Voronkov On Computability by Logic Programs. [Citation Graph (0, 0)][DBLP ] Ann. Math. Artif. Intell., 1995, v:15, n:3-4, pp:437-456 [Journal ] Konstantin Korovin , Andrei Voronkov Knuth-Bendix constraint solving is NP-complete [Citation Graph (0, 0)][DBLP ] CoRR, 2002, v:0, n:, pp:- [Journal ] Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov Complexity and expressive power of logic programming. [Citation Graph (0, 0)][DBLP ] ACM Comput. Surv., 2001, v:33, n:3, pp:374-425 [Journal ] Anatoli Degtyarev , Yuri Gurevich , Andrei Voronkov Herbrand's Theorem and Equational Reasoning: Problems and Solutions. [Citation Graph (0, 0)][DBLP ] Bulletin of the EATCS, 1996, v:60, n:, pp:78-96 [Journal ] Konstantin Korovin , Andrei Voronkov Orienting rewrite rules with the Knuth-Bendix order. [Citation Graph (0, 0)][DBLP ] Inf. Comput., 2003, v:183, n:2, pp:165-186 [Journal ] Alexandre Riazanov , Andrei Voronkov Efficient instance retrieval with standard and relational path indexing. [Citation Graph (0, 0)][DBLP ] Inf. Comput., 2005, v:199, n:1-2, pp:228-252 [Journal ] Anatoli Degtyarev , Andrei Voronkov What You Always Wanted to Know about Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1998, v:20, n:1, pp:47-80 [Journal ] Andrei Voronkov Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2003, v:30, n:2, pp:121-151 [Journal ] Andrei Voronkov The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1995, v:15, n:2, pp:237-265 [Journal ] Andrei Voronkov Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E -Unification. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1998, v:21, n:2, pp:205-231 [Journal ] Anatoli Degtyarev , Andrei Voronkov A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers. [Citation Graph (0, 0)][DBLP ] J. Log. Program., 1996, v:28, n:3, pp:207-216 [Journal ] Anatoli Degtyarev , Robert Nieuwenhuis , Andrei Voronkov Stratified resolution. [Citation Graph (0, 0)][DBLP ] J. Symb. Comput., 2003, v:36, n:1-2, pp:79-99 [Journal ] Alexandre Riazanov , Andrei Voronkov Limited resource strategy in resolution theorem proving. [Citation Graph (0, 0)][DBLP ] J. Symb. Comput., 2003, v:36, n:1-2, pp:101-115 [Journal ] Andrei Voronkov The Ground-Negative Fragment of First-Order Logic Is Pip 2 -Complete. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 1999, v:64, n:3, pp:984-990 [Journal ] Melvin Fitting , Lars Thalmann , Andrei Voronkov Term-Modal Logics. [Citation Graph (0, 0)][DBLP ] Studia Logica, 2001, v:69, n:1, pp:133-169 [Journal ] Anatoli Degtyarev , Yuri Gurevich , Paliath Narendran , Margus Veanes , Andrei Voronkov Decidability and complexity of simultaneous rigid E-unification with one variable and related results. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2000, v:243, n:1-2, pp:167-184 [Journal ] Anatoli Degtyarev , Andrei Voronkov The Undecidability of Simultaneous Rigid E-Unification. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1996, v:166, n:1&2, pp:291-300 [Journal ] Yuri Gurevich , Andrei Voronkov Monadic Simultaneous Rigid E-unification. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1999, v:222, n:1-2, pp:133-152 [Journal ] Andrei Voronkov Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1999, v:224, n:1-2, pp:319-352 [Journal ] Konstantin Korovin , Andrei Voronkov Knuth-Bendix constraint solving is NP-complete. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2005, v:6, n:2, pp:361-388 [Journal ] Tatiana Rybina , Andrei Voronkov A decision procedure for term algebras with queues. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2001, v:2, n:2, pp:155-181 [Journal ] Andrei Voronkov How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2001, v:2, n:2, pp:182-215 [Journal ] Juan Antonio Navarro Pérez , Andrei Voronkov Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. [Citation Graph (0, 0)][DBLP ] CADE, 2007, pp:346-361 [Conf ] Konstantin Korovin , Andrei Voronkov Integrating Linear Arithmetic into Superposition Calculus. [Citation Graph (0, 0)][DBLP ] CSL, 2007, pp:223-237 [Conf ] Juan Antonio Navarro Pérez , Andrei Voronkov Encodings of Problems in Effectively Propositional Logic. [Citation Graph (0, 0)][DBLP ] SAT, 2007, pp:3- [Conf ] Proof Systems for Effectively Propositional Logic. [Citation Graph (, )][DBLP ] Interpolation and Symbol Elimination. [Citation Graph (, )][DBLP ] Interpolation and Symbol Elimination in Vampire. [Citation Graph (, )][DBLP ] Conflict Resolution. [Citation Graph (, )][DBLP ] Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. [Citation Graph (, )][DBLP ] Verifying equivalence of memories using a first order logic theorem prover. [Citation Graph (, )][DBLP ] Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. [Citation Graph (, )][DBLP ] Comparing Unification Algorithms in First-Order Theorem Proving. [Citation Graph (, )][DBLP ] Inter-program Properties. [Citation Graph (, )][DBLP ] Path Feasibility Analysis for String-Manipulating Programs. [Citation Graph (, )][DBLP ] Invariant and Type Inference for Matrices. [Citation Graph (, )][DBLP ] Search in 0.087secs, Finished in 0.091secs