BibTeX records: Andrei Voronkov

download as .bib file

@inproceedings{DBLP:conf/lpar/KovacsV17,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {First-Order Interpolation and Interpolating Proof Systems},
  booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
               Intelligence and Reasoning, Maun, Botswana, 7-12th May 2017},
  pages     = {49--64},
  year      = {2017},
  crossref  = {DBLP:conf/lpar/2017},
  url       = {http://www.easychair.org/publications/paper/340364},
  timestamp = {Wed, 16 Aug 2017 16:30:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/KovacsV17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/KovacsRV17,
  author    = {Laura Kov{\'{a}}cs and
               Simon Robillard and
               Andrei Voronkov},
  title     = {Coming to terms with quantified reasoning},
  booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
               Programming Languages, {POPL} 2017, Paris, France, January 18-20,
               2017},
  pages     = {260--270},
  year      = {2017},
  crossref  = {DBLP:conf/popl/2017},
  url       = {http://dl.acm.org/citation.cfm?id=3009887},
  timestamp = {Wed, 28 Dec 2016 13:17:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/KovacsRV17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tap/Reger0V17,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {Testing a Saturation-Based Theorem Prover: Experiences and Challenges},
  booktitle = {Tests and Proofs - 11th International Conference, {TAP} 2017, Held
               as Part of {STAF} 2017, Marburg, Germany, July 19-20, 2017, Proceedings},
  pages     = {152--161},
  year      = {2017},
  crossref  = {DBLP:conf/tap/2017},
  url       = {https://doi.org/10.1007/978-3-319-61467-0_10},
  doi       = {10.1007/978-3-319-61467-0_10},
  timestamp = {Mon, 03 Jul 2017 15:54:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tap/Reger0V17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2016vampire,
  editor    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra,
               Portugal, July 2, 2016},
  series    = {EPiC Series in Computing},
  volume    = {44},
  publisher = {EasyChair},
  year      = {2017},
  url       = {http://www.easychair.org/publications/volume/Vampire_2016},
  timestamp = {Wed, 26 Apr 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2016vampire},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2017iwil,
  editor    = {Thomas Eiter and
               David Sands and
               Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {IWIL@LPAR 2017 Workshop and {LPAR-21} Short Presentations, Maun, Botswana,
               May 7-12, 2017},
  series    = {Kalpa Publications in Computing},
  volume    = {1},
  publisher = {EasyChair},
  year      = {2017},
  url       = {https://easychair.org/publications/volume/LPAR-21S},
  timestamp = {Tue, 27 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2017iwil},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/Reger0V17,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {Testing a Saturation-Based Theorem Prover: Experiences and Challenges
               (Extended Version)},
  journal   = {CoRR},
  volume    = {abs/1704.03391},
  year      = {2017},
  url       = {http://arxiv.org/abs/1704.03391},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/Reger0V17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderR0V16,
  author    = {Krystof Hoder and
               Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {Selecting the Selection},
  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  pages     = {313--329},
  year      = {2016},
  crossref  = {DBLP:conf/cade/2016},
  url       = {https://doi.org/10.1007/978-3-319-40229-1_22},
  doi       = {10.1007/978-3-319-40229-1_22},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/HoderR0V16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KotelnikovKRV16,
  author    = {Evgenii Kotelnikov and
               Laura Kov{\'{a}}cs and
               Giles Reger and
               Andrei Voronkov},
  title     = {The vampire and the {FOOL}},
  booktitle = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
               and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
  pages     = {37--48},
  year      = {2016},
  crossref  = {DBLP:conf/cpp/2016},
  url       = {http://doi.acm.org/10.1145/2854065.2854071},
  doi       = {10.1145/2854065.2854071},
  timestamp = {Mon, 18 Jan 2016 19:35:36 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/cpp/KotelnikovKRV16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/gcai/Reger0V16,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {New Techniques in Clausal Form Generation},
  booktitle = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
               19 - October 2, 2016, Berlin, Germany},
  pages     = {11--23},
  year      = {2016},
  crossref  = {DBLP:conf/gcai/2016},
  url       = {http://www.easychair.org/publications/paper/299799},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/gcai/Reger0V16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/gcai/RegerB0V16,
  author    = {Giles Reger and
               Nikolaj Bj{\o}rner and
               Martin Suda and
               Andrei Voronkov},
  title     = {{AVATAR} Modulo Theories},
  booktitle = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
               19 - October 2, 2016, Berlin, Germany},
  pages     = {39--52},
  year      = {2016},
  crossref  = {DBLP:conf/gcai/2016},
  url       = {http://www.easychair.org/publications/paper/299800},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/gcai/RegerB0V16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/gcai/KotelnikovK0V16,
  author    = {Evgenii Kotelnikov and
               Laura Kov{\'{a}}cs and
               Martin Suda and
               Andrei Voronkov},
  title     = {A Clausal Normal Form Translation for {FOOL}},
  booktitle = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
               19 - October 2, 2016, Berlin, Germany},
  pages     = {53--71},
  year      = {2016},
  crossref  = {DBLP:conf/gcai/2016},
  url       = {http://www.easychair.org/publications/paper/305689},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/gcai/KotelnikovK0V16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sat/Reger0V16,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {Finding Finite Models in Multi-sorted First-Order Logic},
  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th
               International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
  pages     = {323--341},
  year      = {2016},
  crossref  = {DBLP:conf/sat/2016},
  url       = {https://doi.org/10.1007/978-3-319-40970-2_20},
  doi       = {10.1007/978-3-319-40970-2_20},
  timestamp = {Tue, 23 May 2017 01:08:19 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sat/Reger0V16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2014-15vampire,
  editor    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014,
               Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany,
               August 2, 2015},
  series    = {EPiC Series in Computing},
  volume    = {38},
  publisher = {EasyChair},
  year      = {2016},
  url       = {http://www.easychair.org/publications/volume/Vampire_2014_and_2015},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2014-15vampire},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2015,
  editor    = {Manuel Mazzara and
               Andrei Voronkov},
  title     = {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},
  series    = {Lecture Notes in Computer Science},
  volume    = {9609},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-41579-6},
  doi       = {10.1007/978-3-319-41579-6},
  isbn      = {978-3-319-41578-9},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/Reger0V16,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {Finding Finite Models in Multi-Sorted First Order Logic},
  journal   = {CoRR},
  volume    = {abs/1604.08040},
  year      = {2016},
  url       = {http://arxiv.org/abs/1604.08040},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/Reger0V16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/Reger0VH16,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov and
               Krystof Hoder},
  title     = {Selecting the Selection},
  journal   = {CoRR},
  volume    = {abs/1604.08055},
  year      = {2016},
  url       = {http://arxiv.org/abs/1604.08055},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/Reger0VH16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/KovacsRV16,
  author    = {Laura Kov{\'{a}}cs and
               Simon Robillard and
               Andrei Voronkov},
  title     = {Coming to Terms with Quantified Reasoning},
  journal   = {CoRR},
  volume    = {abs/1611.02908},
  year      = {2016},
  url       = {http://arxiv.org/abs/1611.02908},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/KovacsRV16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/RegerTV15,
  author    = {Giles Reger and
               Dmitry Tishkovsky and
               Andrei Voronkov},
  title     = {Cooperating Proof Attempts},
  booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  pages     = {339--355},
  year      = {2015},
  crossref  = {DBLP:conf/cade/2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6_23},
  doi       = {10.1007/978-3-319-21401-6_23},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/RegerTV15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/RegerSV15,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {Playing with {AVATAR}},
  booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  pages     = {399--415},
  year      = {2015},
  crossref  = {DBLP:conf/cade/2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6_28},
  doi       = {10.1007/978-3-319-21401-6_28},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/RegerSV15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/mkm/KotelnikovKV15,
  author    = {Evgenii Kotelnikov and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {A First Class Boolean Sort in First-Order Theorem Proving and {TPTP}},
  booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
               2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  pages     = {71--86},
  year      = {2015},
  crossref  = {DBLP:conf/mkm/2015},
  url       = {https://doi.org/10.1007/978-3-319-20615-8_5},
  doi       = {10.1007/978-3-319-20615-8_5},
  timestamp = {Sun, 04 Jun 2017 10:10:26 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mkm/KotelnikovKV15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2014,
  editor    = {Andrei Voronkov and
               Irina Virbitskaite},
  title     = {Perspectives of System Informatics - 9th International Ershov Informatics
               Conference, {PSI} 2014, St. Petersburg, Russia, June 24-27, 2014.
               Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {8974},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-662-46823-4},
  doi       = {10.1007/978-3-662-46823-4},
  isbn      = {978-3-662-46822-7},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/gcai/2015,
  editor    = {Georg Gottlob and
               Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {Global Conference on Artificial Intelligence, {GCAI} 2015, Tbilisi,
               Georgia, October 16-19, 2015},
  series    = {EPiC Series in Computing},
  volume    = {36},
  publisher = {EasyChair},
  year      = {2015},
  url       = {http://www.easychair.org/publications/volume/GCAI_2015},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/gcai/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2015s,
  editor    = {Ansgar Fehnker and
               Annabelle McIver and
               Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {20th International Conferences on Logic for Programming, Artificial
               Intelligence and Reasoning - Short Presentations, {LPAR} 2015, Suva,
               Fiji, November 24-28, 2015},
  series    = {EPiC Series in Computing},
  volume    = {35},
  publisher = {EasyChair},
  year      = {2015},
  url       = {http://www.easychair.org/publications/volume/LPAR-20},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2015s},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2015,
  editor    = {Martin Davis and
               Ansgar Fehnker and
               Annabelle McIver and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,
               2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-662-48899-7},
  doi       = {10.1007/978-3-662-48899-7},
  isbn      = {978-3-662-48898-0},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/KotelnikovKV15,
  author    = {Evgenii Kotelnikov and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {A First Class Boolean Sort in First-Order Theorem Proving and {TPTP}},
  journal   = {CoRR},
  volume    = {abs/1505.01682},
  year      = {2015},
  url       = {http://arxiv.org/abs/1505.01682},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/KotelnikovKV15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/KotelnikovKRV15,
  author    = {Evgenii Kotelnikov and
               Laura Kov{\'{a}}cs and
               Giles Reger and
               Andrei Voronkov},
  title     = {The Vampire and the {FOOL}},
  journal   = {CoRR},
  volume    = {abs/1510.04821},
  year      = {2015},
  url       = {http://arxiv.org/abs/1510.04821},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/KotelnikovKRV15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/atva/GuptaKKV14,
  author    = {Ashutosh Gupta and
               Laura Kov{\'{a}}cs and
               Bernhard Kragl and
               Andrei Voronkov},
  title     = {Extensional Crisis and Proving Identity},
  booktitle = {Automated Technology for Verification and Analysis - 12th International
               Symposium, {ATVA} 2014, Sydney, NSW, Australia, November 3-7, 2014,
               Proceedings},
  pages     = {185--200},
  year      = {2014},
  crossref  = {DBLP:conf/atva/2014},
  url       = {https://doi.org/10.1007/978-3-319-11936-6_14},
  doi       = {10.1007/978-3-319-11936-6_14},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/atva/GuptaKKV14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/BiereDKV14,
  author    = {Armin Biere and
               Ioan Dragan and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {{SAT} solving experiments in Vampire},
  booktitle = {Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014,
               Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany,
               August 2, 2015},
  pages     = {29--32},
  year      = {2014},
  crossref  = {DBLP:conf/cade/2014-15vampire},
  url       = {http://www.easychair.org/publications/paper/181258},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/BiereDKV14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Reger0V14,
  author    = {Giles Reger and
               Martin Suda and
               Andrei Voronkov},
  title     = {The Challenges of Evaluating a New Feature in Vampire},
  booktitle = {Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014,
               Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany,
               August 2, 2015},
  pages     = {70--74},
  year      = {2014},
  crossref  = {DBLP:conf/cade/2014-15vampire},
  url       = {http://www.easychair.org/publications/paper/184298},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Reger0V14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cav/Voronkov14,
  author    = {Andrei Voronkov},
  title     = {{AVATAR:} The Architecture for First-Order Theorem Provers},
  booktitle = {Computer Aided Verification - 26th International Conference, {CAV}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 18-22, 2014. Proceedings},
  pages     = {696--710},
  year      = {2014},
  crossref  = {DBLP:conf/cav/2014},
  url       = {https://doi.org/10.1007/978-3-319-08867-9_46},
  doi       = {10.1007/978-3-319-08867-9_46},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cav/Voronkov14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/kbse/Voronkov14,
  author    = {Andrei Voronkov},
  title     = {Keynote talk: EasyChair},
  booktitle = {{ACM/IEEE} International Conference on Automated Software Engineering,
               {ASE} '14, Vasteras, Sweden - September 15 - 19, 2014},
  pages     = {3--4},
  year      = {2014},
  crossref  = {DBLP:conf/kbse/2014},
  url       = {http://doi.acm.org/10.1145/2642937.2643085},
  doi       = {10.1145/2642937.2643085},
  timestamp = {Wed, 29 Mar 2017 16:45:22 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/kbse/Voronkov14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/micai/BiereDKV14,
  author    = {Armin Biere and
               Ioan Dragan and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Experimenting with {SAT} Solvers in Vampire},
  booktitle = {Human-Inspired Computing and Its Applications - 13th Mexican International
               Conference on Artificial Intelligence, {MICAI} 2014, Tuxtla Guti{\'{e}}rrez,
               Mexico, November 16-22, 2014. Proceedings, Part {I}},
  pages     = {431--442},
  year      = {2014},
  crossref  = {DBLP:conf/micai/2014-1},
  url       = {https://doi.org/10.1007/978-3-319-13647-9_39},
  doi       = {10.1007/978-3-319-13647-9_39},
  timestamp = {Wed, 24 May 2017 08:27:28 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/micai/BiereDKV14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{DBLP:conf/birthday/2014howard,
  editor    = {Andrei Voronkov and
               Margarita V. Korovina},
  title     = {{HOWARD-60:} {A} Festschrift on the Occasion of Howard Barringer's
               60th Birthday},
  series    = {EPiC Series in Computing},
  volume    = {42},
  publisher = {EasyChair},
  year      = {2014},
  url       = {https://easychair.org/publications/volume/HOWARD-60},
  timestamp = {Wed, 16 Aug 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/2014howard},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2014p,
  editor    = {Irina Virbitskaite and
               Andrei Voronkov},
  title     = {{PSI} 2014. Ershov Informatics Conference, June 24-27, 2014, Peterhof,
               St. Petersburg, Russia, Poster Presentations},
  series    = {EPiC Series in Computing},
  volume    = {23},
  publisher = {EasyChair},
  year      = {2014},
  url       = {http://www.easychair.org/publications/?page=1895213033},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2014p},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2013s,
  editor    = {Kenneth L. McMillan and
               Aart Middeldorp and
               Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {{LPAR} 2013, 19th International Conference on Logic for Programming,
               Artificial Intelligence and Reasoning, December 12-17, 2013, Stellenbosch,
               South Africa, Short papers proceedings},
  series    = {EPiC Series in Computing},
  volume    = {26},
  publisher = {EasyChair},
  year      = {2014},
  url       = {http://www.easychair.org/publications/?page=668528027},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2013s},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sycss/2014,
  editor    = {Temur Kutsia and
               Andrei Voronkov},
  title     = {6th International Symposium on Symbolic Computation in Software Science,
               {SCSS} 2014, Gammarth, La Marsa, Tunisia, December 7-8, 2014},
  series    = {EPiC Series in Computing},
  volume    = {30},
  publisher = {EasyChair},
  year      = {2014},
  url       = {http://www.easychair.org/publications/?page=862275542},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sycss/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/birthday/KapurNVWW13,
  author    = {Deepak Kapur and
               Robert Nieuwenhuis and
               Andrei Voronkov and
               Christoph Weidenbach and
               Reinhard Wilhelm},
  title     = {Harald Ganzinger's Legacy: Contributions to Logics and Programming},
  booktitle = {Programming Logics - Essays in Memory of Harald Ganzinger},
  pages     = {1--18},
  year      = {2013},
  crossref  = {DBLP:conf/birthday/2013ganzinger},
  url       = {https://doi.org/10.1007/978-3-642-37651-1_1},
  doi       = {10.1007/978-3-642-37651-1_1},
  timestamp = {Tue, 23 May 2017 01:06:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/KapurNVWW13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/birthday/PerezV13,
  author    = {Juan Antonio Navarro P{\'{e}}rez and
               Andrei Voronkov},
  title     = {Planning with Effectively Propositional Logic},
  booktitle = {Programming Logics - Essays in Memory of Harald Ganzinger},
  pages     = {302--316},
  year      = {2013},
  crossref  = {DBLP:conf/birthday/2013ganzinger},
  url       = {https://doi.org/10.1007/978-3-642-37651-1_13},
  doi       = {10.1007/978-3-642-37651-1_13},
  timestamp = {Tue, 23 May 2017 01:06:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/PerezV13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderV13,
  author    = {Krystof Hoder and
               Andrei Voronkov},
  title     = {The 481 Ways to Split a Clause and Deal with Propositional Variables},
  booktitle = {Automated Deduction - {CADE-24} - 24th International Conference on
               Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
  pages     = {450--464},
  year      = {2013},
  crossref  = {DBLP:conf/cade/2013},
  url       = {https://doi.org/10.1007/978-3-642-38574-2_33},
  doi       = {10.1007/978-3-642-38574-2_33},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/HoderV13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cav/KovacsV13,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {First-Order Theorem Proving and Vampire},
  booktitle = {Computer Aided Verification - 25th International Conference, {CAV}
               2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  pages     = {1--35},
  year      = {2013},
  crossref  = {DBLP:conf/cav/2013},
  url       = {https://doi.org/10.1007/978-3-642-39799-8_1},
  doi       = {10.1007/978-3-642-39799-8_1},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cav/KovacsV13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/doceng/ConstantinPV13,
  author    = {Alexandru Constantin and
               Steve Pettifer and
               Andrei Voronkov},
  title     = {{PDFX:} fully-automated PDF-to-XML conversion of scientific literature},
  booktitle = {{ACM} Symposium on Document Engineering 2013, DocEng '13, Florence,
               Italy, September 10-13, 2013},
  pages     = {177--180},
  year      = {2013},
  crossref  = {DBLP:conf/doceng/2013},
  url       = {http://doi.acm.org/10.1145/2494266.2494271},
  doi       = {10.1145/2494266.2494271},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/doceng/ConstantinPV13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/micai/KovacsMV13,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Mantsivoda and
               Andrei Voronkov},
  title     = {The Inverse Method for Many-Valued Logics},
  booktitle = {Advances in Artificial Intelligence and Its Applications - 12th Mexican
               International Conference on Artificial Intelligence, {MICAI} 2013,
               Mexico City, Mexico, November 24-30, 2013, Proceedings, Part {I}},
  pages     = {12--23},
  year      = {2013},
  crossref  = {DBLP:conf/micai/2013-1},
  url       = {https://doi.org/10.1007/978-3-642-45114-0_2},
  doi       = {10.1007/978-3-642-45114-0_2},
  timestamp = {Sun, 04 Jun 2017 10:04:10 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/micai/KovacsMV13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/synasc/DraganKKV13,
  author    = {Ioan Dragan and
               Konstantin Korovin and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Bound Propagation for Arithmetic Reasoning in Vampire},
  booktitle = {15th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2013, Timisoara, Romania, September
               23-26, 2013},
  pages     = {169--176},
  year      = {2013},
  crossref  = {DBLP:conf/synasc/2013},
  url       = {https://doi.org/10.1109/SYNASC.2013.30},
  doi       = {10.1109/SYNASC.2013.30},
  timestamp = {Fri, 19 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/DraganKKV13},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/birthday/2013ganzinger,
  editor    = {Andrei Voronkov and
               Christoph Weidenbach},
  title     = {Programming Logics - Essays in Memory of Harald Ganzinger},
  series    = {Lecture Notes in Computer Science},
  volume    = {7797},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-37651-1},
  doi       = {10.1007/978-3-642-37651-1},
  isbn      = {978-3-642-37650-4},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/2013ganzinger},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2010ys,
  editor    = {Andrei Voronkov and
               Geoff Sutcliffe and
               Matthias Baaz and
               Christian G. Ferm{\"{u}}ller},
  title     = {Short papers for 17th International Conference on Logic for Programming,
               Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta,
               Indonesia, October 10-15, 2010},
  series    = {EPiC Series in Computing},
  volume    = {13},
  publisher = {EasyChair},
  year      = {2013},
  url       = {http://www.easychair.org/publications/?page=1915729019},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2010ys},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2013,
  editor    = {Kenneth L. McMillan and
               Aart Middeldorp and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning - 19th
               International Conference, LPAR-19, Stellenbosch, South Africa, December
               14-19, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8312},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-45221-5},
  doi       = {10.1007/978-3-642-45221-5},
  isbn      = {978-3-642-45220-8},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/japll/SakumaMV12,
  author    = {Yuto Sakuma and
               Yasuhiko Minamide and
               Andrei Voronkov},
  title     = {Translating regular expression matching into transducers},
  journal   = {J. Applied Logic},
  volume    = {10},
  number    = {1},
  pages     = {32--51},
  year      = {2012},
  url       = {https://doi.org/10.1016/j.jal.2011.11.003},
  doi       = {10.1016/j.jal.2011.11.003},
  timestamp = {Thu, 18 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/japll/SakumaMV12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/aplas/HoderHKV12,
  author    = {Krystof Hoder and
               Andreas Holzer and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Vinter: {A} Vampire-Based Tool for Interpolation},
  booktitle = {Programming Languages and Systems - 10th Asian Symposium, {APLAS}
               2012, Kyoto, Japan, December 11-13, 2012. Proceedings},
  pages     = {148--156},
  year      = {2012},
  crossref  = {DBLP:conf/aplas/2012},
  url       = {https://doi.org/10.1007/978-3-642-35182-2_11},
  doi       = {10.1007/978-3-642-35182-2_11},
  timestamp = {Fri, 19 May 2017 01:25:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aplas/HoderHKV12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/EmmerKKSV12,
  author    = {Moshe Emmer and
               Zurab Khasidashvili and
               Konstantin Korovin and
               Christoph Sticksel and
               Andrei Voronkov},
  title     = {EPR-Based Bounded Model Checking at Word Level},
  booktitle = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
               2012, Manchester, UK, June 26-29, 2012. Proceedings},
  pages     = {210--224},
  year      = {2012},
  crossref  = {DBLP:conf/cade/2012},
  url       = {https://doi.org/10.1007/978-3-642-31365-3_18},
  doi       = {10.1007/978-3-642-31365-3_18},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/EmmerKKSV12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/HoderKKV12,
  author    = {Krystof Hoder and
               Zurab Khasidashvili and
               Konstantin Korovin and
               Andrei Voronkov},
  title     = {Preprocessing techniques for first-order clausification},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2012, Cambridge,
               UK, October 22-25, 2012},
  pages     = {44--51},
  year      = {2012},
  crossref  = {DBLP:conf/fmcad/2012},
  url       = {http://ieeexplore.ieee.org/document/6462554/},
  timestamp = {Sat, 29 Apr 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fmcad/HoderKKV12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/popl/HoderKV12,
  author    = {Krystof Hoder and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Playing in the grey area of proofs},
  booktitle = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania,
               USA, January 22-28, 2012},
  pages     = {259--272},
  year      = {2012},
  crossref  = {DBLP:conf/popl/2012},
  url       = {http://doi.acm.org/10.1145/2103656.2103689},
  doi       = {10.1145/2103656.2103689},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/HoderKV12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/birthday/2012turing,
  editor    = {Andrei Voronkov},
  title     = {Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22-25,
               2012},
  series    = {EPiC Series in Computing},
  volume    = {10},
  publisher = {EasyChair},
  year      = {2012},
  url       = {http://www.easychair.org/publications/?page=1900403647},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/2012turing},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2010wing,
  editor    = {Andrei Voronkov and
               Laura Kov{\'{a}}cs and
               Nikolaj Bj{\o}rner},
  title     = {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},
  series    = {EPiC Series in Computing},
  volume    = {1},
  publisher = {EasyChair},
  year      = {2012},
  url       = {http://www.easychair.org/publications/?page=764134496},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2010wing},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2011,
  editor    = {Edmund M. Clarke and
               Irina Virbitskaite and
               Andrei Voronkov},
  title     = {Perspectives of Systems Informatics - 8th International Andrei Ershov
               Memorial Conference, {PSI} 2011, Novosibirsk, Russia, June 27-July
               1, 2011, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {7162},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-29709-0},
  doi       = {10.1007/978-3-642-29709-0},
  isbn      = {978-3-642-29708-3},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2012,
  editor    = {Nikolaj Bj{\o}rner and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning - 18th
               International Conference, LPAR-18, M{\'{e}}rida, Venezuela, March
               11-15, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7180},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-28717-6},
  doi       = {10.1007/978-3-642-28717-6},
  isbn      = {978-3-642-28716-9},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/synasc/2012,
  editor    = {Andrei Voronkov and
               Viorel Negru and
               Tetsuo Ida and
               Tudor Jebelean and
               Dana Petcu and
               Stephen M. Watt and
               Daniela Zaharie},
  title     = {14th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2012, Timisoara, Romania, September
               26-29, 2012},
  publisher = {{IEEE} Computer Society},
  year      = {2012},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6480928},
  isbn      = {978-1-4673-5026-6},
  timestamp = {Tue, 13 Jan 2015 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderV11,
  author    = {Krystof Hoder and
               Andrei Voronkov},
  title     = {Sine Qua Non for Large Theory Reasoning},
  booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  pages     = {299--314},
  year      = {2011},
  crossref  = {DBLP:conf/cade/2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6_23},
  doi       = {10.1007/978-3-642-22438-6_23},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/HoderV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/KorovinV11,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Solving Systems of Linear Inequalities by Bound Propagation},
  booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  pages     = {369--383},
  year      = {2011},
  crossref  = {DBLP:conf/cade/2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6_28},
  doi       = {10.1007/978-3-642-22438-6_28},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/KorovinV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/KovacsMV11,
  author    = {Laura Kov{\'{a}}cs and
               Georg Moser and
               Andrei Voronkov},
  title     = {On Transfinite Knuth-Bendix Orders},
  booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  pages     = {384--399},
  year      = {2011},
  crossref  = {DBLP:conf/cade/2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6_29},
  doi       = {10.1007/978-3-642-22438-6_29},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/KovacsMV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ershov/KorovinV11,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {GoRRiLA and Hard Reality},
  booktitle = {Perspectives of Systems Informatics - 8th International Andrei Ershov
               Memorial Conference, {PSI} 2011, Novosibirsk, Russia, June 27-July
               1, 2011, Revised Selected Papers},
  pages     = {243--250},
  year      = {2011},
  crossref  = {DBLP:conf/ershov/2011},
  url       = {https://doi.org/10.1007/978-3-642-29709-0_21},
  doi       = {10.1007/978-3-642-29709-0_21},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/KorovinV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ershov/KorovinTV11,
  author    = {Konstantin Korovin and
               Nestan Tsiskaridze and
               Andrei Voronkov},
  title     = {Implementing Conflict Resolution},
  booktitle = {Perspectives of Systems Informatics - 8th International Andrei Ershov
               Memorial Conference, {PSI} 2011, Novosibirsk, Russia, June 27-July
               1, 2011, Revised Selected Papers},
  pages     = {362--376},
  year      = {2011},
  crossref  = {DBLP:conf/ershov/2011},
  url       = {https://doi.org/10.1007/978-3-642-29709-0_31},
  doi       = {10.1007/978-3-642-29709-0_31},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/KorovinTV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/micai/HoderKV11,
  author    = {Krystof Hoder and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Case Studies on Invariant Generation Using a Saturation Theorem Prover},
  booktitle = {Advances in Artificial Intelligence - 10th Mexican International Conference
               on Artificial Intelligence, {MICAI} 2011, Puebla, Mexico, November
               26 - December 4, 2011, Proceedings, Part {I}},
  pages     = {1--15},
  year      = {2011},
  crossref  = {DBLP:conf/micai/2011-1},
  url       = {https://doi.org/10.1007/978-3-642-25324-9_1},
  doi       = {10.1007/978-3-642-25324-9_1},
  timestamp = {Wed, 24 May 2017 08:27:28 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/micai/HoderKV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tacas/HoderKV11,
  author    = {Krystof Hoder and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Invariant Generation in Vampire},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 17th International Conference, {TACAS} 2011, Held as Part of the
               Joint European Conferences on Theory and Practice of Software, {ETAPS}
               2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
  pages     = {60--64},
  year      = {2011},
  crossref  = {DBLP:conf/tacas/2011},
  url       = {https://doi.org/10.1007/978-3-642-19835-9_7},
  doi       = {10.1007/978-3-642-19835-9_7},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tacas/HoderKV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/BjornerNVV11,
  author    = {Nikolaj Bj{\o}rner and
               Robert Nieuwenhuis and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl
               Seminar 11272)},
  journal   = {Dagstuhl Reports},
  volume    = {1},
  number    = {7},
  pages     = {23--35},
  year      = {2011},
  url       = {https://doi.org/10.4230/DagRep.1.7.23},
  doi       = {10.4230/DagRep.1.7.23},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/dagstuhl-reports/BjornerNVV11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderKV10,
  author    = {Krystof Hoder and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Interpolation and Symbol Elimination in Vampire},
  booktitle = {Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010,
               Edinburgh, UK, July 16-19, 2010. Proceedings},
  pages     = {188--195},
  year      = {2010},
  crossref  = {DBLP:conf/cade/2010},
  url       = {https://doi.org/10.1007/978-3-642-14203-1_16},
  doi       = {10.1007/978-3-642-14203-1_16},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/HoderKV10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/EmmerKKV10,
  author    = {Moshe Emmer and
               Zurab Khasidashvili and
               Konstantin Korovin and
               Andrei Voronkov},
  title     = {Encoding industrial hardware verification problems into effectively
               propositional logic},
  booktitle = {Proceedings of 10th International Conference on Formal Methods in
               Computer-Aided Design, {FMCAD} 2010, Lugano, Switzerland, October
               20-23},
  pages     = {137--144},
  year      = {2010},
  crossref  = {DBLP:conf/fmcad/2010},
  url       = {http://ieeexplore.ieee.org/document/5770942/},
  timestamp = {Sun, 30 Apr 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fmcad/EmmerKKV10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icms/UrbanHV10,
  author    = {Josef Urban and
               Krystof Hoder and
               Andrei Voronkov},
  title     = {Evaluation of Automated Theorem Proving on the Mizar Mathematical
               Library},
  booktitle = {Mathematical Software - {ICMS} 2010, Third International Congress
               on Mathematical Software, Kobe, Japan, September 13-17, 2010. Proceedings},
  pages     = {155--166},
  year      = {2010},
  crossref  = {DBLP:conf/icms/2010},
  url       = {https://doi.org/10.1007/978-3-642-15582-6_30},
  doi       = {10.1007/978-3-642-15582-6_30},
  timestamp = {Sun, 04 Jun 2017 10:11:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icms/UrbanHV10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/synasc/MinamideSV10,
  author    = {Yasuhiko Minamide and
               Yuto Sakuma and
               Andrei Voronkov},
  title     = {Translating Regular Expression Matching into Transducers},
  booktitle = {12th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2010, Timisoara, Romania, 23-26 September
               2010},
  pages     = {107--115},
  year      = {2010},
  crossref  = {DBLP:conf/synasc/2010},
  url       = {https://doi.org/10.1109/SYNASC.2010.50},
  doi       = {10.1109/SYNASC.2010.50},
  timestamp = {Fri, 19 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/MinamideSV10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/HenzingerHKV10,
  author    = {Thomas A. Henzinger and
               Thibaud Hottelier and
               Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Invariant and Type Inference for Matrices},
  booktitle = {Verification, Model Checking, and Abstract Interpretation, 11th International
               Conference, {VMCAI} 2010, Madrid, Spain, January 17-19, 2010. Proceedings},
  pages     = {163--179},
  year      = {2010},
  crossref  = {DBLP:conf/vmcai/2010},
  url       = {https://doi.org/10.1007/978-3-642-11319-2_14},
  doi       = {10.1007/978-3-642-11319-2_14},
  timestamp = {Wed, 24 May 2017 08:30:31 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/vmcai/HenzingerHKV10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/wwv/Voronkov10,
  author    = {Andrei Voronkov},
  title     = {EasyChair},
  booktitle = {6th International Workshop on Automated Specification and Verification
               of Web Systems, {WWV} 2010, Vienna, Austria, July 30-31, 2010},
  pages     = {2},
  year      = {2010},
  crossref  = {DBLP:conf/wwv/2010},
  url       = {http://www.easychair.org/publications/paper/58536},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/wwv/Voronkov10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/dagstuhl/2010P10161,
  editor    = {Nikolaj Bj{\o}rner and
               Robert Nieuwenhuis and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010},
  series    = {Dagstuhl Seminar Proceedings},
  volume    = {10161},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, Germany},
  year      = {2010},
  url       = {http://drops.dagstuhl.de/portals/10161/},
  timestamp = {Thu, 09 Apr 2015 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/2010P10161},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2009,
  editor    = {Amir Pnueli and
               Irina Virbitskaite and
               Andrei Voronkov},
  title     = {Perspectives of Systems Informatics, 7th International Andrei Ershov
               Memorial Conference, {PSI} 2009, Novosibirsk, Russia, June 15-19,
               2009. Revised Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {5947},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-11486-1},
  doi       = {10.1007/978-3-642-11486-1},
  isbn      = {978-3-642-11485-4},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2010d,
  editor    = {Edmund M. Clarke and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning - 16th
               International Conference, LPAR-16, Dakar, Senegal, April 25-May 1,
               2010, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {6355},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-17511-4},
  doi       = {10.1007/978-3-642-17511-4},
  isbn      = {978-3-642-17510-7},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2010d},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2010y,
  editor    = {Christian G. Ferm{\"{u}}ller and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning - 17th
               International Conference, LPAR-17, Yogyakarta, Indonesia, October
               10-15, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6397},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-16242-8},
  doi       = {10.1007/978-3-642-16242-8},
  isbn      = {978-3-642-16241-1},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2010y},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BjornerNVV10,
  author    = {Nikolaj Bj{\o}rner and
               Robert Nieuwenhuis and
               Helmut Veith and
               Andrei Voronkov},
  title     = {10161 Abstracts Collection - Decision Procedures in Software, Hardware
               and Bioware},
  booktitle = {Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010},
  year      = {2010},
  crossref  = {DBLP:conf/dagstuhl/2010P10161},
  url       = {http://drops.dagstuhl.de/opus/volltexte/2010/2742/},
  timestamp = {Sun, 09 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/BjornerNVV10},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BjornerNVV10a,
  author    = {Nikolaj Bj{\o}rner and
               Robert Nieuwenhuis and
               Helmut Veith and
               Andrei Voronkov},
  title     = {10161 Executive Summary - Decision Procedures in Software, Hardware
               and Bioware},
  booktitle = {Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010},
  year      = {2010},
  crossref  = {DBLP:conf/dagstuhl/2010P10161},
  url       = {http://drops.dagstuhl.de/opus/volltexte/2010/2736/},
  timestamp = {Sun, 09 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/BjornerNVV10a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/KovacsV09,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Interpolation and Symbol Elimination},
  booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  pages     = {199--213},
  year      = {2009},
  crossref  = {DBLP:conf/cade/2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2_17},
  doi       = {10.1007/978-3-642-02959-2_17},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/KovacsV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cp/KorovinTV09,
  author    = {Konstantin Korovin and
               Nestan Tsiskaridze and
               Andrei Voronkov},
  title     = {Conflict Resolution},
  booktitle = {Principles and Practice of Constraint Programming - {CP} 2009, 15th
               International Conference, {CP} 2009, Lisbon, Portugal, September 20-24,
               2009, Proceedings},
  pages     = {509--523},
  year      = {2009},
  crossref  = {DBLP:conf/cp/2009},
  url       = {https://doi.org/10.1007/978-3-642-04244-7_41},
  doi       = {10.1007/978-3-642-04244-7_41},
  timestamp = {Wed, 17 May 2017 14:24:33 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cp/KorovinTV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fase/KovacsV09,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Finding Loop Invariants for Programs over Arrays Using a Theorem Prover},
  booktitle = {Fundamental Approaches to Software Engineering, 12th International
               Conference, {FASE} 2009, Held as Part of the Joint European Conferences
               on Theory and Practice of Software, {ETAPS} 2009, York, UK, March
               22-29, 2009. Proceedings},
  pages     = {470--485},
  year      = {2009},
  crossref  = {DBLP:conf/fase/2009},
  url       = {https://doi.org/10.1007/978-3-642-00593-0_33},
  doi       = {10.1007/978-3-642-00593-0_33},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fase/KovacsV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/KhasidashviliKV09,
  author    = {Zurab Khasidashvili and
               Mahmoud Kinanah and
               Andrei Voronkov},
  title     = {Verifying equivalence of memories using a first order logic theorem
               prover},
  booktitle = {Proceedings of 9th International Conference on Formal Methods in Computer-Aided
               Design, {FMCAD} 2009, 15-18 November 2009, Austin, Texas, {USA}},
  pages     = {128--135},
  year      = {2009},
  crossref  = {DBLP:conf/fmcad/2009},
  url       = {https://doi.org/10.1109/FMCAD.2009.5351132},
  doi       = {10.1109/FMCAD.2009.5351132},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fmcad/KhasidashviliKV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ki/HoderV09,
  author    = {Krystof Hoder and
               Andrei Voronkov},
  title     = {Comparing Unification Algorithms in First-Order Theorem Proving},
  booktitle = {{KI} 2009: Advances in Artificial Intelligence, 32nd Annual German
               Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings},
  pages     = {435--443},
  year      = {2009},
  crossref  = {DBLP:conf/ki/2009},
  url       = {https://doi.org/10.1007/978-3-642-04617-9_55},
  doi       = {10.1007/978-3-642-04617-9_55},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ki/HoderV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sas/VoronkovN09,
  author    = {Andrei Voronkov and
               Iman Narasamdya},
  title     = {Inter-program Properties},
  booktitle = {Static Analysis, 16th International Symposium, {SAS} 2009, Los Angeles,
               CA, USA, August 9-11, 2009. Proceedings},
  pages     = {343--359},
  year      = {2009},
  crossref  = {DBLP:conf/sas/2009},
  url       = {https://doi.org/10.1007/978-3-642-03237-0_23},
  doi       = {10.1007/978-3-642-03237-0_23},
  timestamp = {Wed, 24 May 2017 08:27:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sas/VoronkovN09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/synasc/KovacsV09,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Finding Loop Invariants for Programs over Arrays Using a Theorem Prover},
  booktitle = {11th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2009, Timisoara, Romania, September
               26-29, 2009},
  pages     = {10},
  year      = {2009},
  crossref  = {DBLP:conf/synasc/2009},
  url       = {https://doi.org/10.1109/SYNASC.2009.66},
  doi       = {10.1109/SYNASC.2009.66},
  timestamp = {Fri, 19 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/KovacsV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/synasc/Voronkov09,
  author    = {Andrei Voronkov},
  title     = {Satisfiability and Theories},
  booktitle = {11th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2009, Timisoara, Romania, September
               26-29, 2009},
  pages     = {16},
  year      = {2009},
  crossref  = {DBLP:conf/synasc/2009},
  url       = {https://doi.org/10.1109/SYNASC.2009.65},
  doi       = {10.1109/SYNASC.2009.65},
  timestamp = {Fri, 19 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/Voronkov09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BjornerTV09,
  author    = {Nikolaj Bj{\o}rner and
               Nikolai Tillmann and
               Andrei Voronkov},
  title     = {Path Feasibility Analysis for String-Manipulating Programs},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
               15th International Conference, {TACAS} 2009, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2009,
               York, UK, March 22-29, 2009. Proceedings},
  pages     = {307--321},
  year      = {2009},
  crossref  = {DBLP:conf/tacas/2009},
  url       = {https://doi.org/10.1007/978-3-642-00768-2_27},
  doi       = {10.1007/978-3-642-00768-2_27},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tacas/BjornerTV09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/PerezV08,
  author    = {Juan Antonio Navarro P{\'{e}}rez and
               Andrei Voronkov},
  title     = {Proof Systems for Effectively Propositional Logic},
  booktitle = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008,
               Sydney, Australia, August 12-15, 2008, Proceedings},
  pages     = {426--440},
  year      = {2008},
  crossref  = {DBLP:conf/cade/2008},
  url       = {https://doi.org/10.1007/978-3-540-71070-7_36},
  doi       = {10.1007/978-3-540-71070-7_36},
  timestamp = {Tue, 13 Jun 2017 10:37:55 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/PerezV08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2008,
  editor    = {Iliano Cervesato and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
               International Conference, {LPAR} 2008, Doha, Qatar, November 22-27,
               2008. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5330},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-89439-1},
  doi       = {10.1007/978-3-540-89439-1},
  isbn      = {978-3-540-89438-4},
  timestamp = {Tue, 13 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/rta/2008,
  editor    = {Andrei Voronkov},
  title     = {Rewriting Techniques and Applications, 19th International Conference,
               {RTA} 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5117},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-70590-1},
  doi       = {10.1007/978-3-540-70590-1},
  isbn      = {978-3-540-70588-8},
  timestamp = {Tue, 13 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/PerezV07,
  author    = {Juan Antonio Navarro P{\'{e}}rez and
               Andrei Voronkov},
  title     = {Encodings of Bounded {LTL} Model Checking in Effectively Propositional
               Logic},
  booktitle = {Automated Deduction - CADE-21, 21st International Conference on Automated
               Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  pages     = {346--361},
  year      = {2007},
  crossref  = {DBLP:conf/cade/2007},
  url       = {https://doi.org/10.1007/978-3-540-73595-3_24},
  doi       = {10.1007/978-3-540-73595-3_24},
  timestamp = {Fri, 02 Jun 2017 13:01:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/PerezV07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/KorovinV07,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Integrating Linear Arithmetic into Superposition Calculus},
  booktitle = {Computer Science Logic, 21st International Workshop, {CSL} 2007, 16th
               Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15,
               2007, Proceedings},
  pages     = {223--237},
  year      = {2007},
  crossref  = {DBLP:conf/csl/2007},
  url       = {https://doi.org/10.1007/978-3-540-74915-8_19},
  doi       = {10.1007/978-3-540-74915-8_19},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/KorovinV07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sat/PerezV07,
  author    = {Juan Antonio Navarro P{\'{e}}rez and
               Andrei Voronkov},
  title     = {Encodings of Problems in Effectively Propositional Logic},
  booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2007, 10th
               International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings},
  pages     = {3},
  year      = {2007},
  crossref  = {DBLP:conf/sat/2007},
  url       = {https://doi.org/10.1007/978-3-540-72788-0_2},
  doi       = {10.1007/978-3-540-72788-0_2},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sat/PerezV07},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csr/2007,
  editor    = {Volker Diekert and
               Mikhail V. Volkov and
               Andrei Voronkov},
  title     = {Computer Science - Theory and Applications, Second International Symposium
               on Computer Science in Russia, {CSR} 2007, Ekaterinburg, Russia, September
               3-7, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4649},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-74510-5},
  doi       = {10.1007/978-3-540-74510-5},
  isbn      = {978-3-540-74509-9},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csr/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2006,
  editor    = {Irina Virbitskaite and
               Andrei Voronkov},
  title     = {Perspectives of Systems Informatics, 6th International Andrei Ershov
               Memorial Conference, {PSI} 2006, Novosibirsk, Russia, June 27-30,
               2006. Revised Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {4378},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-70881-0},
  doi       = {10.1007/978-3-540-70881-0},
  isbn      = {978-3-540-70880-3},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2007,
  editor    = {Nachum Dershowitz and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 14th
               International Conference, {LPAR} 2007, Yerevan, Armenia, October 15-19,
               2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4790},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-75560-9},
  doi       = {10.1007/978-3-540-75560-9},
  isbn      = {978-3-540-75558-6},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/adbis/JaberV06,
  author    = {Mohammed K. Jaber and
               Andrei Voronkov},
  title     = {Implementation of UNIDOOR, a Deductive Object-Oriented Database System},
  booktitle = {Advances in Databases and Information Systems, 10th East European
               Conference, {ADBIS} 2006, Thessaloniki, Greece, September 3-7, 2006,
               Proceedings},
  pages     = {155--170},
  year      = {2006},
  crossref  = {DBLP:conf/adbis/2006},
  url       = {https://doi.org/10.1007/11827252_14},
  doi       = {10.1007/11827252_14},
  timestamp = {Thu, 15 Jun 2017 21:42:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/adbis/JaberV06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/foiks/HorrocksV06,
  author    = {Ian Horrocks and
               Andrei Voronkov},
  title     = {Reasoning Support for Expressive Ontology Languages Using a Theorem
               Prover},
  booktitle = {Foundations of Information and Knowledge Systems, 4th International
               Symposium, FoIKS 2006, Budapest, Hungary, February 14-17, 2006, Proceedings},
  pages     = {201--218},
  year      = {2006},
  crossref  = {DBLP:conf/foiks/2006},
  url       = {https://doi.org/10.1007/11663881_12},
  doi       = {10.1007/11663881_12},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/foiks/HorrocksV06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icde/JaberV06,
  author    = {Mohammed K. Jaber and
               Andrei Voronkov},
  title     = {{UNIDOOR:} a Deductive Object-Oriented Database Management System},
  booktitle = {Proceedings of the 22nd International Conference on Data Engineering,
               {ICDE} 2006, 3-8 April 2006, Atlanta, GA, {USA}},
  pages     = {157},
  year      = {2006},
  crossref  = {DBLP:conf/icde/2006},
  url       = {https://doi.org/10.1109/ICDE.2006.164},
  doi       = {10.1109/ICDE.2006.164},
  timestamp = {Fri, 21 Jul 2017 13:46:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icde/JaberV06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/jelia/Voronkov06,
  author    = {Andrei Voronkov},
  title     = {Inconsistencies in Ontologies},
  booktitle = {Logics in Artificial Intelligence, 10th European Conference, {JELIA}
               2006, Liverpool, UK, September 13-15, 2006, Proceedings},
  pages     = {19},
  year      = {2006},
  crossref  = {DBLP:conf/jelia/2006},
  url       = {https://doi.org/10.1007/11853886_3},
  doi       = {10.1007/11853886_3},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/jelia/Voronkov06},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/dagstuhl/2005P5431,
  editor    = {Franz Baader and
               Peter Baumgartner and
               Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {Deduction and Applications, 23.-28. October 2005},
  series    = {Dagstuhl Seminar Proceedings},
  volume    = {05431},
  publisher = {Internationales Begegnungs- und Forschungszentrum f{\"{u}}r Informatik
               (IBFI), Schloss Dagstuhl, Germany},
  year      = {2006},
  url       = {http://drops.dagstuhl.de/portals/05431/},
  timestamp = {Wed, 19 Jun 2013 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/2005P5431},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2006,
  editor    = {Miki Hermann and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
               International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
               13-17, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4246},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11916277},
  doi       = {10.1007/11916277},
  isbn      = {3-540-48281-4},
  timestamp = {Fri, 02 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/iandc/RiazanovV05,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Efficient instance retrieval with standard and relational path indexing},
  journal   = {Inf. Comput.},
  volume    = {199},
  number    = {1-2},
  pages     = {228--252},
  year      = {2005},
  url       = {https://doi.org/10.1016/j.ic.2004.10.012},
  doi       = {10.1016/j.ic.2004.10.012},
  timestamp = {Thu, 18 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/iandc/RiazanovV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/KorovinV05,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Knuth-Bendix constraint solving is NP-complete},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {6},
  number    = {2},
  pages     = {361--388},
  year      = {2005},
  url       = {http://doi.acm.org/10.1145/1055686.1055692},
  doi       = {10.1145/1055686.1055692},
  timestamp = {Thu, 09 Feb 2006 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/KorovinV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/aaai/NavarroV05,
  author    = {Juan Antonio Navarro P{\'{e}}rez and
               Andrei Voronkov},
  title     = {Generation of Hard Non-Clausal Random Satisfiability Problems},
  booktitle = {Proceedings, The Twentieth National Conference on Artificial Intelligence
               and the Seventeenth Innovative Applications of Artificial Intelligence
               Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, {USA}},
  pages     = {436--442},
  year      = {2005},
  crossref  = {DBLP:conf/aaai/2005},
  url       = {http://www.aaai.org/Library/AAAI/2005/aaai05-069.php},
  timestamp = {Mon, 10 Dec 2012 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/aaai/NavarroV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/birthday/ChubarovV05,
  author    = {Dimitri Chubarov and
               Andrei Voronkov},
  title     = {Solving First-Order Constraints over the Monadic Class},
  booktitle = {Mechanizing Mathematical Reasoning, Essays in Honor of J{\"{o}}rg
               H. Siekmann on the Occasion of His 60th Birthday},
  pages     = {132--138},
  year      = {2005},
  crossref  = {DBLP:conf/birthday/2005siekmann},
  url       = {https://doi.org/10.1007/978-3-540-32254-2_8},
  doi       = {10.1007/978-3-540-32254-2_8},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/ChubarovV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/mfcs/ChubarovV05,
  author    = {Dimitri Chubarov and
               Andrei Voronkov},
  title     = {Basis of Solutions for a System of Linear Inequalities in Integers:
               Computation and Applications},
  booktitle = {Mathematical Foundations of Computer Science 2005, 30th International
               Symposium, {MFCS} 2005, Gdansk, Poland, August 29 - September 2, 2005,
               Proceedings},
  pages     = {260--270},
  year      = {2005},
  crossref  = {DBLP:conf/mfcs/2005},
  url       = {https://doi.org/10.1007/11549345_23},
  doi       = {10.1007/11549345_23},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mfcs/ChubarovV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/mfcs/KorovinV05,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Random Databases and Threshold for Monotone Non-recursive Datalog},
  booktitle = {Mathematical Foundations of Computer Science 2005, 30th International
               Symposium, {MFCS} 2005, Gdansk, Poland, August 29 - September 2, 2005,
               Proceedings},
  pages     = {591--602},
  year      = {2005},
  crossref  = {DBLP:conf/mfcs/2005},
  url       = {https://doi.org/10.1007/11549345_51},
  doi       = {10.1007/11549345_51},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mfcs/KorovinV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/sas/NarasamdyaV05,
  author    = {Iman Narasamdya and
               Andrei Voronkov},
  title     = {Finding Basic Block and Variable Correspondence},
  booktitle = {Static Analysis, 12th International Symposium, {SAS} 2005, London,
               UK, September 7-9, 2005, Proceedings},
  pages     = {251--267},
  year      = {2005},
  crossref  = {DBLP:conf/sas/2005},
  url       = {https://doi.org/10.1007/11547662_18},
  doi       = {10.1007/11547662_18},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sas/NarasamdyaV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2004,
  editor    = {Franz Baader and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 11th
               International Conference, {LPAR} 2004, Montevideo, Uruguay, March
               14-18, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3452},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/b106931},
  doi       = {10.1007/b106931},
  isbn      = {3-540-25236-3},
  timestamp = {Tue, 30 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2004},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2005,
  editor    = {Geoff Sutcliffe and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 12th
               International Conference, {LPAR} 2005, Montego Bay, Jamaica, December
               2-6, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3835},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11591191},
  doi       = {10.1007/11591191},
  isbn      = {3-540-30553-X},
  timestamp = {Tue, 30 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderBNV05,
  author    = {Franz Baader and
               Peter Baumgartner and
               Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {05431 Executive Summary - Deduction and Applications},
  booktitle = {Deduction and Applications, 23.-28. October 2005},
  year      = {2005},
  crossref  = {DBLP:conf/dagstuhl/2005P5431},
  url       = {http://drops.dagstuhl.de/opus/volltexte/2006/510},
  timestamp = {Sun, 09 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/BaaderBNV05},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderBNV05a,
  author    = {Franz Baader and
               Peter Baumgartner and
               Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {05431 Abstracts Collection - Deduction and Applications},
  booktitle = {Deduction and Applications, 23.-28. October 2005},
  year      = {2005},
  crossref  = {DBLP:conf/dagstuhl/2005P5431},
  url       = {http://drops.dagstuhl.de/opus/volltexte/2006/562},
  timestamp = {Sun, 09 Jul 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/BaaderBNV05a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV04,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Efficient Checking of Term Ordering Constraints},
  booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR}
               2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  pages     = {60--74},
  year      = {2004},
  crossref  = {DBLP:conf/cade/2004},
  url       = {https://doi.org/10.1007/978-3-540-25984-8_3},
  doi       = {10.1007/978-3-540-25984-8_3},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/RiazanovV04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/HustadtKRV04,
  author    = {Ullrich Hustadt and
               Boris Konev and
               Alexandre Riazanov and
               Andrei Voronkov},
  title     = {TeMP: {A} Temporal Monodic Prover},
  booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR}
               2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  pages     = {326--330},
  year      = {2004},
  crossref  = {DBLP:conf/cade/2004},
  url       = {https://doi.org/10.1007/978-3-540-25984-8_23},
  doi       = {10.1007/978-3-540-25984-8_23},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/HustadtKRV04},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/iandc/KorovinV03,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Orienting rewrite rules with the Knuth-Bendix order},
  journal   = {Inf. Comput.},
  volume    = {183},
  number    = {2},
  pages     = {165--186},
  year      = {2003},
  url       = {https://doi.org/10.1016/S0890-5401(03)00021-X},
  doi       = {10.1016/S0890-5401(03)00021-X},
  timestamp = {Thu, 18 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/iandc/KorovinV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/Voronkov03,
  author    = {Andrei Voronkov},
  title     = {Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous
               Rigid E-Unification},
  journal   = {J. Autom. Reasoning},
  volume    = {30},
  number    = {2},
  pages     = {121--151},
  year      = {2003},
  url       = {https://doi.org/10.1023/A:1023260415982},
  doi       = {10.1023/A:1023260415982},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/Voronkov03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jsc/DegtyarevNV03,
  author    = {Anatoli Degtyarev and
               Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {Stratified resolution},
  journal   = {J. Symb. Comput.},
  volume    = {36},
  number    = {1-2},
  pages     = {79--99},
  year      = {2003},
  url       = {https://doi.org/10.1016/S0747-7171(03)00036-1},
  doi       = {10.1016/S0747-7171(03)00036-1},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jsc/DegtyarevNV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jsc/RiazanovV03,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Limited resource strategy in resolution theorem proving},
  journal   = {J. Symb. Comput.},
  volume    = {36},
  number    = {1-2},
  pages     = {101--115},
  year      = {2003},
  url       = {https://doi.org/10.1016/S0747-7171(03)00040-3},
  doi       = {10.1016/S0747-7171(03)00040-3},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jsc/RiazanovV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/KorovinV03,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {An AC-Compatible Knuth-Bendix Order},
  booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  pages     = {47--59},
  year      = {2003},
  crossref  = {DBLP:conf/cade/2003},
  url       = {https://doi.org/10.1007/978-3-540-45085-6_5},
  doi       = {10.1007/978-3-540-45085-6_5},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/KorovinV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV03,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Efficient Instance Retrieval with Standard and Relational Path Indexing},
  booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  pages     = {380--396},
  year      = {2003},
  crossref  = {DBLP:conf/cade/2003},
  url       = {https://doi.org/10.1007/978-3-540-45085-6_34},
  doi       = {10.1007/978-3-540-45085-6_34},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/RiazanovV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/MaksimovaV03,
  author    = {Larisa Maksimova and
               Andrei Voronkov},
  title     = {Complexity of Some Problems in Modal and Intuitionistic Calculi},
  booktitle = {Computer Science Logic, 17th International Workshop, {CSL} 2003, 12th
               Annual Conference of the EACSL, and 8th Kurt G{\"{o}}del Colloquium,
               {KGC} 2003, Vienna, Austria, August 25-30, 2003, Proceedings},
  pages     = {397--412},
  year      = {2003},
  crossref  = {DBLP:conf/csl/2003},
  url       = {https://doi.org/10.1007/978-3-540-45220-1_32},
  doi       = {10.1007/978-3-540-45220-1_32},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/MaksimovaV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/RybinaV03,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {Fast Infinite-State Model Checking in Integer-Based Systems (Invited
               Lecture)},
  booktitle = {Computer Science Logic, 17th International Workshop, {CSL} 2003, 12th
               Annual Conference of the EACSL, and 8th Kurt G{\"{o}}del Colloquium,
               {KGC} 2003, Vienna, Austria, August 25-30, 2003, Proceedings},
  pages     = {546--573},
  year      = {2003},
  crossref  = {DBLP:conf/csl/2003},
  url       = {https://doi.org/10.1007/978-3-540-45220-1_46},
  doi       = {10.1007/978-3-540-45220-1_46},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/RybinaV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ershov/RybinaV03,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {A Logical Reconstruction of Reachability},
  booktitle = {Perspectives of Systems Informatics, 5th International Andrei Ershov
               Memorial Conference, {PSI} 2003, Akademgorodok, Novosibirsk, Russia,
               July 9-12, 2003, Revised Papers},
  pages     = {222--237},
  year      = {2003},
  crossref  = {DBLP:conf/ershov/2003},
  url       = {https://doi.org/10.1007/978-3-540-39866-0_24},
  doi       = {10.1007/978-3-540-39866-0_24},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/RybinaV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icalp/RybinaV03,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {Upper Bounds for a Theory of Queues},
  booktitle = {Automata, Languages and Programming, 30th International Colloquium,
               {ICALP} 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003.
               Proceedings},
  pages     = {714--724},
  year      = {2003},
  crossref  = {DBLP:conf/icalp/2003},
  url       = {https://doi.org/10.1007/3-540-45061-0_56},
  doi       = {10.1007/3-540-45061-0_56},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/RybinaV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/Voronkov03,
  author    = {Andrei Voronkov},
  title     = {Automated Reasoning: Past Story and New Trends},
  booktitle = {IJCAI-03, Proceedings of the Eighteenth International Joint Conference
               on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003},
  pages     = {1607--1612},
  year      = {2003},
  crossref  = {DBLP:conf/ijcai/2003},
  url       = {http://ijcai.org/Proceedings/03/Papers/284.pdf},
  timestamp = {Thu, 25 Aug 2016 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/Voronkov03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/KorovinV03,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Orienting Equalities with the Knuth-Bendix Order},
  booktitle = {18th {IEEE} Symposium on Logic in Computer Science {(LICS} 2003),
               22-25 June 2003, Ottawa, Canada, Proceedings},
  pages     = {75},
  year      = {2003},
  crossref  = {DBLP:conf/lics/2003},
  url       = {https://doi.org/10.1109/LICS.2003.1210047},
  doi       = {10.1109/LICS.2003.1210047},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/KorovinV03},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2003,
  editor    = {Moshe Y. Vardi and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 10th
               International Conference, {LPAR} 2003, Almaty, Kazakhstan, September
               22-26, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2850},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b13986},
  doi       = {10.1007/b13986},
  isbn      = {3-540-20101-7},
  timestamp = {Mon, 29 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/aicom/RiazanovV02,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {The design and implementation of {VAMPIRE}},
  journal   = {{AI} Commun.},
  volume    = {15},
  number    = {2-3},
  pages     = {91--110},
  year      = {2002},
  url       = {http://content.iospress.com/articles/ai-communications/aic259},
  timestamp = {Fri, 15 May 2015 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/aicom/RiazanovV02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/amast/RybinaV02,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {{BRAIN} : Backward Reachability Analysis with Integers},
  booktitle = {Algebraic Methodology and Software Technology, 9th International Conference,
               {AMAST} 2002, Saint-Gilles-les-Bains, Reunion Island, France, September
               9-13, 2002, Proceedings},
  pages     = {489--494},
  year      = {2002},
  crossref  = {DBLP:conf/amast/2002},
  url       = {https://doi.org/10.1007/3-540-45719-4_33},
  doi       = {10.1007/3-540-45719-4_33},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/amast/RybinaV02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cav/RybinaV02,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {Using Canonical Representations of Solutions to Speed Up Infinite-State
               Model Checking},
  booktitle = {Computer Aided Verification, 14th International Conference, {CAV}
               2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
  pages     = {386--400},
  year      = {2002},
  crossref  = {DBLP:conf/cav/2002},
  url       = {https://doi.org/10.1007/3-540-45657-0_32},
  doi       = {10.1007/3-540-45657-0_32},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cav/RybinaV02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/dlog/Voronkov02,
  author    = {Andrei Voronkov},
  title     = {First-Order Theorem Provers: the Next Generation},
  booktitle = {Proceedings of the 2002 International Workshop on Description Logics
               (DL2002), Toulouse, France, April 19-21, 2002},
  year      = {2002},
  crossref  = {DBLP:conf/dlog/2002},
  url       = {http://ceur-ws.org/Vol-53/voronkov.ps},
  timestamp = {Mon, 30 May 2016 15:43:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dlog/Voronkov02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fsttcs/KorovinV02,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {The Decidability of the First-Order Theory of the Knuth-Bendix Order
               in the Case of Unary Signatures},
  booktitle = {{FST} {TCS} 2002: Foundations of Software Technology and Theoretical
               Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002,
               Proceedings},
  pages     = {230--240},
  year      = {2002},
  crossref  = {DBLP:conf/fsttcs/2002},
  url       = {https://doi.org/10.1007/3-540-36206-1_21},
  doi       = {10.1007/3-540-36206-1_21},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fsttcs/KorovinV02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2002,
  editor    = {Andrei Voronkov},
  title     = {Automated Deduction - CADE-18, 18th International Conference on Automated
               Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2392},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45620-1},
  doi       = {10.1007/3-540-45620-1},
  isbn      = {3-540-43931-5},
  timestamp = {Fri, 26 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2002,
  editor    = {Matthias Baaz and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 9th
               International Conference, {LPAR} 2002, Tbilisi, Georgia, October 14-18,
               2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2514},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-36078-6},
  doi       = {10.1007/3-540-36078-6},
  isbn      = {3-540-00010-0},
  timestamp = {Mon, 29 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/corr/cs-LO-0207068,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Knuth-Bendix constraint solving is NP-complete},
  journal   = {CoRR},
  volume    = {cs.LO/0207068},
  year      = {2002},
  url       = {http://arxiv.org/abs/cs.LO/0207068},
  timestamp = {Wed, 07 Jun 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/corr/cs-LO-0207068},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/csur/DantsinEGV01,
  author    = {Evgeny Dantsin and
               Thomas Eiter and
               Georg Gottlob and
               Andrei Voronkov},
  title     = {Complexity and expressive power of logic programming},
  journal   = {{ACM} Comput. Surv.},
  volume    = {33},
  number    = {3},
  pages     = {374--425},
  year      = {2001},
  url       = {http://doi.acm.org/10.1145/502807.502810},
  doi       = {10.1145/502807.502810},
  timestamp = {Wed, 19 Nov 2003 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/csur/DantsinEGV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/sLogica/FittingTV01,
  author    = {Melvin Fitting and
               Lars Thalmann and
               Andrei Voronkov},
  title     = {Term-Modal Logics},
  journal   = {Studia Logica},
  volume    = {69},
  number    = {1},
  pages     = {133--169},
  year      = {2001},
  url       = {https://doi.org/10.1023/A:1013842612702},
  doi       = {10.1023/A:1013842612702},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/sLogica/FittingTV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/RybinaV01,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {A decision procedure for term algebras with queues},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {2},
  number    = {2},
  pages     = {155--181},
  year      = {2001},
  url       = {http://doi.acm.org/10.1145/371316.371494},
  doi       = {10.1145/371316.371494},
  timestamp = {Fri, 21 Nov 2003 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/RybinaV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tocl/Voronkov01,
  author    = {Andrei Voronkov},
  title     = {How to optimize proof-search in modal logics: new methods of proving
               redundancy criteria for sequent calculi},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {2},
  number    = {2},
  pages     = {182--215},
  year      = {2001},
  url       = {http://doi.acm.org/10.1145/371316.371511},
  doi       = {10.1145/371316.371511},
  timestamp = {Fri, 21 Nov 2003 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/journals/tocl/Voronkov01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov01,
  author    = {Andrei Voronkov},
  title     = {Algorithms, Datastructures, and other Issues in Efficient Automated
               Deduction},
  booktitle = {Automated Reasoning, First International Joint Conference, {IJCAR}
               2001, Siena, Italy, June 18-23, 2001, Proceedings},
  pages     = {13--28},
  year      = {2001},
  crossref  = {DBLP:conf/cade/2001},
  url       = {https://doi.org/10.1007/3-540-45744-5_3},
  doi       = {10.1007/3-540-45744-5_3},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Voronkov01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisHRV01,
  author    = {Robert Nieuwenhuis and
               Thomas Hillenbrand and
               Alexandre Riazanov and
               Andrei Voronkov},
  title     = {On the Evaluation of Indexing Techniques for Theorem Proving},
  booktitle = {Automated Reasoning, First International Joint Conference, {IJCAR}
               2001, Siena, Italy, June 18-23, 2001, Proceedings},
  pages     = {257--271},
  year      = {2001},
  crossref  = {DBLP:conf/cade/2001},
  url       = {https://doi.org/10.1007/3-540-45744-5_19},
  doi       = {10.1007/3-540-45744-5_19},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/NieuwenhuisHRV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV01,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Vampire 1.1 (System Description)},
  booktitle = {Automated Reasoning, First International Joint Conference, {IJCAR}
               2001, Siena, Italy, June 18-23, 2001, Proceedings},
  pages     = {376--380},
  year      = {2001},
  crossref  = {DBLP:conf/cade/2001},
  url       = {https://doi.org/10.1007/3-540-45744-5_29},
  doi       = {10.1007/3-540-45744-5_29},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/RiazanovV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ershov/RiazanovV01,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Adaptive Saturation-Based Reasoning},
  booktitle = {Perspectives of System Informatics, 4th International Andrei Ershov
               Memorial Conference, {PSI} 2001, Akademgorodok, Novosibirsk, Russia,
               July 2-6, 2001, Revised Papers},
  pages     = {95--108},
  year      = {2001},
  crossref  = {DBLP:conf/ershov/2001},
  url       = {https://doi.org/10.1007/3-540-45575-2_11},
  doi       = {10.1007/3-540-45575-2_11},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/RiazanovV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icalp/KorovinV01,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Knuth-Bendix Constraint Solving Is NP-Complete},
  booktitle = {Automata, Languages and Programming, 28th International Colloquium,
               {ICALP} 2001, Crete, Greece, July 8-12, 2001, Proceedings},
  pages     = {979--992},
  year      = {2001},
  crossref  = {DBLP:conf/icalp/2001},
  url       = {https://doi.org/10.1007/3-540-48224-5_79},
  doi       = {10.1007/3-540-48224-5_79},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/KorovinV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/RiazanovV01,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Splitting Without Backtracking},
  booktitle = {Proceedings of the Seventeenth International Joint Conference on Artificial
               Intelligence, {IJCAI} 2001, Seattle, Washington, USA, August 4-10,
               2001},
  pages     = {611--617},
  year      = {2001},
  crossref  = {DBLP:conf/ijcai/2001},
  timestamp = {Tue, 19 Jul 2016 16:01:40 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/RiazanovV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/rta/KorovinV01,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order},
  booktitle = {Rewriting Techniques and Applications, 12th International Conference,
               {RTA} 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings},
  pages     = {137--153},
  year      = {2001},
  crossref  = {DBLP:conf/rta/2001},
  url       = {https://doi.org/10.1007/3-540-45127-7_12},
  doi       = {10.1007/3-540-45127-7_12},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/KorovinV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/el/RV01/DegtyarevV01,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {The Inverse Method},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  pages     = {179--272},
  year      = {2001},
  crossref  = {DBLP:books/el/RobinsonV01},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RV01/DegtyarevV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/el/RV01/DegtyarevV01a,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Equality Reasoning in Sequent-Based Calculi},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  pages     = {611--706},
  year      = {2001},
  crossref  = {DBLP:books/el/RobinsonV01},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RV01/DegtyarevV01a},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/el/RV01/RamakrishnanSV01,
  author    = {I. V. Ramakrishnan and
               R. C. Sekar and
               Andrei Voronkov},
  title     = {Term Indexing},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  pages     = {1853--1964},
  year      = {2001},
  crossref  = {DBLP:books/el/RobinsonV01},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RV01/RamakrishnanSV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/el/RV01/RobinsonV01,
  author    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Preface},
  booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
  year      = {2001},
  crossref  = {DBLP:books/el/RobinsonV01},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RV01/RobinsonV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{DBLP:books/ws/phaunRS01/DegtyarevGV01,
  author    = {Anatoli Degtyarev and
               Yuri Gurevich and
               Andrei Voronkov},
  title     = {Herbrand's Theorem and Equational Reasoning: Problems and Solutions},
  booktitle = {Current Trends in Theoretical Computer Science},
  pages     = {303--326},
  year      = {2001},
  timestamp = {Wed, 15 May 2002 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/books/ws/phaunRS01/DegtyarevGV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{DBLP:books/el/RobinsonV01,
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Handbook of Automated Reasoning (in 2 volumes)},
  publisher = {Elsevier and {MIT} Press},
  year      = {2001},
  isbn      = {0-444-50813-9},
  timestamp = {Wed, 29 Mar 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RobinsonV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2001,
  editor    = {Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 8th
               International Conference, {LPAR} 2001, Havana, Cuba, December 3-7,
               2001, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2250},
  publisher = {Springer},
  year      = {2001},
  url       = {https://doi.org/10.1007/3-540-45653-8},
  doi       = {10.1007/3-540-45653-8},
  isbn      = {3-540-42957-3},
  timestamp = {Fri, 26 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/DegtyarevGNVV00,
  author    = {Anatoli Degtyarev and
               Yuri Gurevich and
               Paliath Narendran and
               Margus Veanes and
               Andrei Voronkov},
  title     = {Decidability and complexity of simultaneous rigid E-unification with
               one variable and related results},
  journal   = {Theor. Comput. Sci.},
  volume    = {243},
  number    = {1-2},
  pages     = {167--184},
  year      = {2000},
  url       = {https://doi.org/10.1016/S0304-3975(98)00185-6},
  doi       = {10.1016/S0304-3975(98)00185-6},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/DegtyarevGNVV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/arw/KorovinV00,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {The Existential Theories of Term Algebras with the Knuth-Bendix Orderings
               are Decidable},
  booktitle = {Proceedings of the Seventh Workshop on Automated Reasoning, Bridging
               the Gap between Theory and Practice, King's College London, UK, 20-21
               July 2000.},
  year      = {2000},
  crossref  = {DBLP:conf/arw/2000},
  url       = {http://ceur-ws.org/Vol-32/korovin.ps.gz},
  timestamp = {Fri, 25 Aug 2017 11:19:29 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/arw/KorovinV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/arw/RiazanovV00,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {System Description: Vampire 1.0},
  booktitle = {Proceedings of the Seventh Workshop on Automated Reasoning, Bridging
               the Gap between Theory and Practice, King's College London, UK, 20-21
               July 2000.},
  year      = {2000},
  crossref  = {DBLP:conf/arw/2000},
  url       = {http://ceur-ws.org/Vol-32/riazanov.ps.gz},
  timestamp = {Fri, 25 Aug 2017 11:19:29 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/arw/RiazanovV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/arw/RybinaV00,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {A Decision Procedure for Term Algebras with Queues},
  booktitle = {Proceedings of the Seventh Workshop on Automated Reasoning, Bridging
               the Gap between Theory and Practice, King's College London, UK, 20-21
               July 2000.},
  year      = {2000},
  crossref  = {DBLP:conf/arw/2000},
  url       = {http://ceur-ws.org/Vol-32/rybina.ps.gz},
  timestamp = {Fri, 25 Aug 2017 11:19:29 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/arw/RybinaV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/DegtyarevV00,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Stratified Resolution},
  booktitle = {Automated Deduction - CADE-17, 17th International Conference on Automated
               Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
  pages     = {365--384},
  year      = {2000},
  crossref  = {DBLP:conf/cade/2000},
  url       = {https://doi.org/10.1007/10721959_28},
  doi       = {10.1007/10721959_28},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/DegtyarevV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/jelia/RiazanovV00,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Partially Adaptive Code Trees},
  booktitle = {Logics in Artificial Intelligence, European Workshop, {JELIA} 2000
               Malaga, Spain, September 29 - October 2, 2000, Proceedings},
  pages     = {209--223},
  year      = {2000},
  crossref  = {DBLP:conf/jelia/2000},
  url       = {https://doi.org/10.1007/3-540-40006-0_15},
  doi       = {10.1007/3-540-40006-0_15},
  timestamp = {Wed, 24 May 2017 15:40:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/jelia/RiazanovV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/kr/Voronkov00,
  author    = {Andrei Voronkov},
  title     = {Deciding {K} using inverse-K},
  booktitle = {{KR} 2000, Principles of Knowledge Representation and Reasoning Proceedings
               of the Seventh International Conference, Breckenridge, Colorado, USA,
               April 11-15, 2000.},
  pages     = {198--209},
  year      = {2000},
  crossref  = {DBLP:conf/kr/2000},
  timestamp = {Fri, 18 May 2012 15:03:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/kr/Voronkov00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/RybinaV00,
  author    = {Tatiana Rybina and
               Andrei Voronkov},
  title     = {A Decision Procedure for Term Algebras with Queues},
  booktitle = {15th Annual {IEEE} Symposium on Logic in Computer Science, Santa Barbara,
               California, USA, June 26-29, 2000},
  pages     = {279--290},
  year      = {2000},
  crossref  = {DBLP:conf/lics/2000},
  url       = {https://doi.org/10.1109/LICS.2000.855776},
  doi       = {10.1109/LICS.2000.855776},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/RybinaV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/KorovinV00,
  author    = {Konstantin Korovin and
               Andrei Voronkov},
  title     = {A Decision Procedure for the Existential Theory of Term Algebras with
               the Knuth-Bendix Ordering},
  booktitle = {15th Annual {IEEE} Symposium on Logic in Computer Science, Santa Barbara,
               California, USA, June 26-29, 2000},
  pages     = {291--302},
  year      = {2000},
  crossref  = {DBLP:conf/lics/2000},
  url       = {https://doi.org/10.1109/LICS.2000.855777},
  doi       = {10.1109/LICS.2000.855777},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/KorovinV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Voronkov00,
  author    = {Andrei Voronkov},
  title     = {How to Optimize Proof-Search in Modal Logics: {A} New Way of Proving
               Redundancy Criteria for Sequent Calculi},
  booktitle = {15th Annual {IEEE} Symposium on Logic in Computer Science, Santa Barbara,
               California, USA, June 26-29, 2000},
  pages     = {401--412},
  year      = {2000},
  crossref  = {DBLP:conf/lics/2000},
  url       = {https://doi.org/10.1109/LICS.2000.855787},
  doi       = {10.1109/LICS.2000.855787},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Voronkov00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pods/DantsinV00,
  author    = {Evgeny Dantsin and
               Andrei Voronkov},
  title     = {Expressive Power and Data Complexity of Query Languages for Trees
               and Lists},
  booktitle = {Proceedings of the Nineteenth {ACM} {SIGMOD-SIGACT-SIGART} Symposium
               on Principles of Database Systems, May 15-17, 2000, Dallas, Texas,
               {USA}},
  pages     = {157--165},
  year      = {2000},
  crossref  = {DBLP:conf/pods/00},
  url       = {http://doi.acm.org/10.1145/335168.335218},
  doi       = {10.1145/335168.335218},
  timestamp = {Wed, 29 Mar 2017 16:45:25 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pods/DantsinV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/FittingTV00,
  author    = {Melvin Fitting and
               Lars Thalmann and
               Andrei Voronkov},
  title     = {Term-Modal Logics},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, International
               Conference, {TABLEAUX} 2000, St Andrews, Scotland, UK, July 3-7, 2000,
               Proceedings},
  pages     = {220--236},
  year      = {2000},
  crossref  = {DBLP:conf/tableaux/2000},
  url       = {https://doi.org/10.1007/10722086_19},
  doi       = {10.1007/10722086_19},
  timestamp = {Wed, 24 May 2017 15:40:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tableaux/FittingTV00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2000,
  editor    = {Michel Parigot and
               Andrei Voronkov},
  title     = {Logic for Programming and Automated Reasoning, 7th International Conference,
               {LPAR} 2000, Reunion Island, France, November 11-12, 2000, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1955},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/3-540-44404-1},
  doi       = {10.1007/3-540-44404-1},
  timestamp = {Wed, 24 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jsyml/Voronkov99,
  author    = {Andrei Voronkov},
  title     = {The Ground-Negative Fragment of First-Order Logic Is Pi\({}^{\mbox{p}}\)\({}_{\mbox{2}}\)-Complete},
  journal   = {J. Symb. Log.},
  volume    = {64},
  number    = {3},
  pages     = {984--990},
  year      = {1999},
  url       = {https://doi.org/10.2307/2586615},
  doi       = {10.2307/2586615},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jsyml/Voronkov99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/GurevichV99,
  author    = {Yuri Gurevich and
               Andrei Voronkov},
  title     = {Monadic Simultaneous Rigid E-unification},
  journal   = {Theor. Comput. Sci.},
  volume    = {222},
  number    = {1-2},
  pages     = {133--152},
  year      = {1999},
  url       = {https://doi.org/10.1016/S0304-3975(98)00123-6},
  doi       = {10.1016/S0304-3975(98)00123-6},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/GurevichV99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/Voronkov99,
  author    = {Andrei Voronkov},
  title     = {Simultaneous Rigid E-unification and other Decision Problems Related
               to the Herbrand Theorem},
  journal   = {Theor. Comput. Sci.},
  volume    = {224},
  number    = {1-2},
  pages     = {319--352},
  year      = {1999},
  url       = {https://doi.org/10.1016/S0304-3975(98)00317-X},
  doi       = {10.1016/S0304-3975(98)00317-X},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/Voronkov99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV99,
  author    = {Alexandre Riazanov and
               Andrei Voronkov},
  title     = {Vampire},
  booktitle = {Automated Deduction - CADE-16, 16th International Conference on Automated
               Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  pages     = {292--296},
  year      = {1999},
  crossref  = {DBLP:conf/cade/1999},
  url       = {https://doi.org/10.1007/3-540-48660-7_26},
  doi       = {10.1007/3-540-48660-7_26},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/RiazanovV99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov99,
  author    = {Andrei Voronkov},
  title     = {{KK:} a theorem prover for {K}},
  booktitle = {Automated Deduction - CADE-16, 16th International Conference on Automated
               Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  pages     = {383--387},
  year      = {1999},
  crossref  = {DBLP:conf/cade/1999},
  url       = {https://doi.org/10.1007/3-540-48660-7_35},
  doi       = {10.1007/3-540-48660-7_35},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Voronkov99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/DantsinV99,
  author    = {Evgeny Dantsin and
               Andrei Voronkov},
  title     = {A Nondeterministic Polynomial-Time Unification Algorithm for Bags,
               Sets and Trees},
  booktitle = {Foundations of Software Science and Computation Structure, Second
               International Conference, FoSSaCS'99, Held as Part of the European
               Joint Conferences on the Theory and Practice of Software, ETAPS'99,
               Amsterdam, The Netherlands, March 22-28, 1999, Proceedings},
  pages     = {180--196},
  year      = {1999},
  crossref  = {DBLP:conf/fossacs/1999},
  url       = {https://doi.org/10.1007/3-540-49019-1_13},
  doi       = {10.1007/3-540-49019-1_13},
  timestamp = {Tue, 23 May 2017 14:54:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/DantsinV99},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/1999,
  editor    = {Harald Ganzinger and
               David A. McAllester and
               Andrei Voronkov},
  title     = {Logic Programming and Automated Reasoning, 6th International Conference,
               LPAR'99, Tbilisi, Georgia, September 6-10, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1705},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48242-3},
  doi       = {10.1007/3-540-48242-3},
  isbn      = {3-540-66492-0},
  timestamp = {Wed, 24 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/DegtyarevV98,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {What You Always Wanted to Know about Rigid E-Unification},
  journal   = {J. Autom. Reasoning},
  volume    = {20},
  number    = {1},
  pages     = {47--80},
  year      = {1998},
  url       = {https://doi.org/10.1023/A:1005996623714},
  doi       = {10.1023/A:1005996623714},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/DegtyarevV98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/Voronkov98,
  author    = {Andrei Voronkov},
  title     = {Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous
               Rigid \emph{E}-Unification},
  journal   = {J. Autom. Reasoning},
  volume    = {21},
  number    = {2},
  pages     = {205--231},
  year      = {1998},
  url       = {https://doi.org/10.1023/A:1005934721802},
  doi       = {10.1023/A:1005934721802},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/Voronkov98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/BachmairGV98,
  author    = {Leo Bachmair and
               Harald Ganzinger and
               Andrei Voronkov},
  title     = {Elimination of Equality via Transformation with Ordering Constraints},
  booktitle = {Automated Deduction - CADE-15, 15th International Conference on Automated
               Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},
  pages     = {175--190},
  year      = {1998},
  crossref  = {DBLP:conf/cade/1998},
  url       = {https://doi.org/10.1007/BFb0054259},
  doi       = {10.1007/BFb0054259},
  timestamp = {Tue, 23 May 2017 11:53:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/BachmairGV98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/Voronkov98,
  author    = {Andrei Voronkov},
  title     = {Herbrand's Theorem, Automated Reasoning and Semantics Tableaux},
  booktitle = {Thirteenth Annual {IEEE} Symposium on Logic in Computer Science, Indianapolis,
               Indiana, USA, June 21-24, 1998},
  pages     = {252--263},
  year      = {1998},
  crossref  = {DBLP:conf/lics/1998},
  url       = {https://doi.org/10.1109/LICS.1998.705662},
  doi       = {10.1109/LICS.1998.705662},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/Voronkov98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pods/VorobyovV98,
  author    = {Sergei G. Vorobyov and
               Andrei Voronkov},
  title     = {Complexity of Nonrecursive Logic Programs with Complex Values},
  booktitle = {Proceedings of the Seventeenth {ACM} {SIGACT-SIGMOD-SIGART} Symposium
               on Principles of Database Systems, June 1-3, 1998, Seattle, Washington,
               {USA}},
  pages     = {244--253},
  year      = {1998},
  crossref  = {DBLP:conf/pods/98},
  url       = {http://doi.acm.org/10.1145/275487.275515},
  doi       = {10.1145/275487.275515},
  timestamp = {Wed, 29 Mar 2017 16:45:24 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pods/VorobyovV98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/rta/DegtyarevGNVV98,
  author    = {Anatoli Degtyarev and
               Yuri Gurevich and
               Paliath Narendran and
               Margus Veanes and
               Andrei Voronkov},
  title     = {The Decidability of Simultaneous Rigid \emph{E}-Unification with One
               Variable},
  booktitle = {Rewriting Techniques and Applications, 9th International Conference,
               RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings},
  pages     = {181--195},
  year      = {1998},
  crossref  = {DBLP:conf/rta/1998},
  url       = {https://doi.org/10.1007/BFb0052370},
  doi       = {10.1007/BFb0052370},
  timestamp = {Tue, 23 May 2017 11:53:58 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/DegtyarevGNVV98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/dagstuhl/1998change,
  editor    = {Burkhard Freitag and
               Hendrik Decker and
               Michael Kifer and
               Andrei Voronkov},
  title     = {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},
  series    = {Lecture Notes in Computer Science},
  volume    = {1472},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0055493},
  doi       = {10.1007/BFb0055493},
  isbn      = {3-540-65305-8},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/1998change},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/coco/DantsinEGV97,
  author    = {Evgeny Dantsin and
               Thomas Eiter and
               Georg Gottlob and
               Andrei Voronkov},
  title     = {Complexity and Expressive Power of Logic Programming},
  booktitle = {Proceedings of the Twelfth Annual {IEEE} Conference on Computational
               Complexity, Ulm, Germany, June 24-27, 1997},
  pages     = {82--101},
  year      = {1997},
  crossref  = {DBLP:conf/coco/1997},
  url       = {https://doi.org/10.1109/CCC.1997.612304},
  doi       = {10.1109/CCC.1997.612304},
  timestamp = {Tue, 23 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/coco/DantsinEGV97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/icalp/GurevichV97,
  author    = {Yuri Gurevich and
               Andrei Voronkov},
  title     = {Monadic Simultaneous Rigid E-Unification and Related Problems},
  booktitle = {Automata, Languages and Programming, 24th International Colloquium,
               ICALP'97, Bologna, Italy, 7-11 July 1997, Proceedings},
  pages     = {154--165},
  year      = {1997},
  crossref  = {DBLP:conf/icalp/1997},
  url       = {https://doi.org/10.1007/3-540-63165-8_173},
  doi       = {10.1007/3-540-63165-8_173},
  timestamp = {Mon, 22 May 2017 17:11:15 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/GurevichV97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/Voronkov97,
  author    = {Andrei Voronkov},
  title     = {Strategies in Rigid-Variable Methods},
  booktitle = {Proceedings of the Fifteenth International Joint Conference on Artificial
               Intelligence, {IJCAI} 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes},
  pages     = {114--121},
  year      = {1997},
  crossref  = {DBLP:conf/ijcai/1997},
  url       = {http://ijcai.org/Proceedings/97-1/Papers/019.pdf},
  timestamp = {Tue, 19 Jul 2016 15:27:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/Voronkov97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lfcs/DantsinV97,
  author    = {Evgeny Dantsin and
               Andrei Voronkov},
  title     = {Complexity of Query Answering in Logic Databases with Complex Values},
  booktitle = {Logical Foundations of Computer Science, 4th International Symposium,
               LFCS'97, Yaroslavl, Russia, July 6-12, 1997, Proceedings},
  pages     = {56--66},
  year      = {1997},
  crossref  = {DBLP:conf/lfcs/1997},
  url       = {https://doi.org/10.1007/3-540-63045-7_7},
  doi       = {10.1007/3-540-63045-7_7},
  timestamp = {Mon, 22 May 2017 17:11:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lfcs/DantsinV97},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/eatcs/DegtyarevGV96,
  author    = {Anatoli Degtyarev and
               Yuri Gurevich and
               Andrei Voronkov},
  title     = {Herbrand's Theorem and Equational Reasoning: Problems and Solutions},
  journal   = {Bulletin of the {EATCS}},
  volume    = {60},
  pages     = {78--96},
  year      = {1996},
  timestamp = {Mon, 05 May 2003 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/eatcs/DegtyarevGV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jlp/DegtyarevV96,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {A Note on Semantics of Logic Programs with Equality Based on Complete
               Sets of E-Unifiers},
  journal   = {J. Log. Program.},
  volume    = {28},
  number    = {3},
  pages     = {207--216},
  year      = {1996},
  url       = {https://doi.org/10.1016/0743-1066(96)00049-0},
  doi       = {10.1016/0743-1066(96)00049-0},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jlp/DegtyarevV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/tcs/DegtyarevV96,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {The Undecidability of Simultaneous Rigid E-Unification},
  journal   = {Theor. Comput. Sci.},
  volume    = {166},
  number    = {1{\&}2},
  pages     = {291--300},
  year      = {1996},
  url       = {https://doi.org/10.1016/0304-3975(96)00092-8},
  doi       = {10.1016/0304-3975(96)00092-8},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/tcs/DegtyarevV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov96,
  author    = {Andrei Voronkov},
  title     = {Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous
               Rigid E-Unification},
  booktitle = {Automated Deduction - CADE-13, 13th International Conference on Automated
               Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings},
  pages     = {32--46},
  year      = {1996},
  crossref  = {DBLP:conf/cade/1996},
  url       = {https://doi.org/10.1007/3-540-61511-3_67},
  doi       = {10.1007/3-540-61511-3_67},
  timestamp = {Mon, 22 May 2017 16:14:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Voronkov96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/disco/DegtyarevV96,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Equality Elimination for the Tableau Method},
  booktitle = {Design and Implementation of Symbolic Computation Systems, International
               Symposium, {DISCO} '96, Karlsruhe, Germany, September 18-20, 1996,
               Proceedings},
  pages     = {46--60},
  year      = {1996},
  crossref  = {DBLP:conf/disco/1996},
  url       = {https://doi.org/10.1007/3-540-61697-7_4},
  doi       = {10.1007/3-540-61697-7_4},
  timestamp = {Mon, 22 May 2017 16:14:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/disco/DegtyarevV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/elp/ArgeniusV96,
  author    = {Martin Argenius and
               Andrei Voronkov},
  title     = {Semantics of Constraint Logic Programs with Bounded Quantifiers},
  booktitle = {Extensions of Logic Programming, 5th International Workshop, ELP'96,
               Leipzig, Germany, March 28-30, 1996, Proceedings},
  pages     = {1--18},
  year      = {1996},
  crossref  = {DBLP:conf/elp/1996},
  url       = {https://doi.org/10.1007/3-540-60983-0_1},
  doi       = {10.1007/3-540-60983-0_1},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/ArgeniusV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/elp/DegtyarevV96,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Handling Equality in Logic Programming via Basic Folding},
  booktitle = {Extensions of Logic Programming, 5th International Workshop, ELP'96,
               Leipzig, Germany, March 28-30, 1996, Proceedings},
  pages     = {119--136},
  year      = {1996},
  crossref  = {DBLP:conf/elp/1996},
  url       = {https://doi.org/10.1007/3-540-60983-0_8},
  doi       = {10.1007/3-540-60983-0_8},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/DegtyarevV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ershov/Voronkov96,
  author    = {Andrei Voronkov},
  title     = {Merging Relational Database Technology with Constraint Technology},
  booktitle = {Perspectives of System Informatics, Second International Andrei Ershov
               Memorial Conference, Akademgorodok, Novosibirsk, Russia, June 25-28,
               1996, Proceedings},
  pages     = {409--419},
  year      = {1996},
  crossref  = {DBLP:conf/ershov/1996},
  url       = {https://doi.org/10.1007/3-540-62064-8_34},
  doi       = {10.1007/3-540-62064-8_34},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/Voronkov96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/jelia/DegtyarevV96,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {What You Always Wanted to Know About Rigid E-Unification},
  booktitle = {Logics in Artificial Intelligence, European Workshop, {JELIA} '96,
               {\'{E}}vora, Portugal, September 30 - October 3, 1996, Proceedings},
  pages     = {50--69},
  year      = {1996},
  crossref  = {DBLP:conf/jelia/1996},
  url       = {https://doi.org/10.1007/3-540-61630-6_4},
  doi       = {10.1007/3-540-61630-6_4},
  timestamp = {Mon, 22 May 2017 16:14:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/jelia/DegtyarevV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/DegtyarevMV96,
  author    = {Anatoli Degtyarev and
               Yuri V. Matiyasevich and
               Andrei Voronkov},
  title     = {Simultaneous E-Unification and Related Algorithmic Problems},
  booktitle = {Proceedings, 11th Annual {IEEE} Symposium on Logic in Computer Science,
               New Brunswick, New Jersey, USA, July 27-30, 1996},
  pages     = {494--502},
  year      = {1996},
  crossref  = {DBLP:conf/lics/1996},
  url       = {https://doi.org/10.1109/LICS.1996.561466},
  doi       = {10.1109/LICS.1996.561466},
  timestamp = {Tue, 19 Sep 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/DegtyarevMV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lics/DegtyarevV96,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Decidability Problems for the Prenex Fragment of Intuitionistic Logic},
  booktitle = {Proceedings, 11th Annual {IEEE} Symposium on Logic in Computer Science,
               New Brunswick, New Jersey, USA, July 27-30, 1996},
  pages     = {503--512},
  year      = {1996},
  crossref  = {DBLP:conf/lics/1996},
  url       = {https://doi.org/10.1109/LICS.1996.561467},
  doi       = {10.1109/LICS.1996.561467},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lics/DegtyarevV96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/Voronkov96,
  author    = {Andrei Voronkov},
  title     = {Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction},
  booktitle = {Theorem Proving with Analytic Tableaux and Related Methods, 5th International
               Workshop, {TABLEAUX} '96, Terrasini, Palermo, Italy, May 15-17, 1996,
               Proceedings},
  pages     = {312--329},
  year      = {1996},
  crossref  = {DBLP:conf/tableaux/1996},
  url       = {https://doi.org/10.1007/3-540-61208-4_20},
  doi       = {10.1007/3-540-61208-4_20},
  timestamp = {Mon, 22 May 2017 16:14:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tableaux/Voronkov96},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/amai/Voronkov95,
  author    = {Andrei Voronkov},
  title     = {On Computability by Logic Programs},
  journal   = {Ann. Math. Artif. Intell.},
  volume    = {15},
  number    = {3-4},
  pages     = {437--456},
  year      = {1995},
  url       = {https://doi.org/10.1007/BF01536404},
  doi       = {10.1007/BF01536404},
  timestamp = {Sun, 28 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/amai/Voronkov95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/jar/Voronkov95,
  author    = {Andrei Voronkov},
  title     = {The Anatomy of Vampire Implementing Bottom-up Procedures with Code
               Trees},
  journal   = {J. Autom. Reasoning},
  volume    = {15},
  number    = {2},
  pages     = {237--265},
  year      = {1995},
  url       = {https://doi.org/10.1007/BF00881918},
  doi       = {10.1007/BF00881918},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/journals/jar/Voronkov95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/DegtyarevV95,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Simultaneous Regid E-Unification Is Undecidable},
  booktitle = {Computer Science Logic, 9th International Workshop, {CSL} '95, Annual
               Conference of the EACSL, Paderborn, Germany, September 22-29, 1995,
               Selected Papers},
  pages     = {178--190},
  year      = {1995},
  crossref  = {DBLP:conf/csl/1995},
  url       = {https://doi.org/10.1007/3-540-61377-3_38},
  doi       = {10.1007/3-540-61377-3_38},
  timestamp = {Mon, 22 May 2017 16:14:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/DegtyarevV95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/iclp/DegtyarevV95,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {A New Procedural Interpretation of Horn Clauses with Equality},
  booktitle = {Logic Programming, Proceedings of the Twelfth International Conference
               on Logic Programming, Tokyo, Japan, June 13-16, 1995},
  pages     = {565--579},
  year      = {1995},
  crossref  = {DBLP:conf/iclp/1995},
  timestamp = {Mon, 02 Dec 2013 17:40:44 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/DegtyarevV95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/DegtyarevV95,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {Equality Elimination for the Inverse Method and Extension Procedures},
  booktitle = {Proceedings of the Fourteenth International Joint Conference on Artificial
               Intelligence, {IJCAI} 95, Montr{\'{e}}al Qu{\'{e}}bec, Canada,
               August 20-25 1995, 2 Volumes},
  pages     = {342--347},
  year      = {1995},
  crossref  = {DBLP:conf/ijcai/1995},
  url       = {http://ijcai.org/Proceedings/95-1/Papers/045.pdf},
  timestamp = {Tue, 19 Jul 2016 15:06:26 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/DegtyarevV95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/wocfai/DegtyarevV95,
  author    = {Anatoli Degtyarev and
               Andrei Voronkov},
  title     = {General Connections via Equality Elimination},
  booktitle = {{WOCFAI}},
  pages     = {109--120},
  year      = {1995},
  timestamp = {Thu, 03 Jan 2002 00:00:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/wocfai/DegtyarevV95},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/plilp/Voronkov94,
  author    = {Andrei Voronkov},
  title     = {An Implementation Technique for a Class of Bottom-Up Procedures},
  booktitle = {Programming Language Implementation and Logic Programming, 6th International
               Symposium, PLILP'94, Madrid, Spain, September 14-16, 1994, Proceedings},
  pages     = {147--164},
  year      = {1994},
  crossref  = {DBLP:conf/plilp/1994},
  url       = {https://doi.org/10.1007/3-540-58402-1_12},
  doi       = {10.1007/3-540-58402-1_12},
  timestamp = {Sat, 20 May 2017 15:32:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/plilp/Voronkov94},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/kgc/SazonovV93,
  author    = {Vladimir Yu. Sazonov and
               Andrei Voronkov},
  title     = {A Construction of Typed Lambda Models Related to Feasible Computability},
  booktitle = {Computational Logic and Proof Theory, Third Kurt G{\"{o}}del
               Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, Proceedings},
  pages     = {301--312},
  year      = {1993},
  crossref  = {DBLP:conf/kgc/1993},
  url       = {https://doi.org/10.1007/BFb0022578},
  doi       = {10.1007/BFb0022578},
  timestamp = {Sat, 20 May 2017 15:32:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/kgc/SazonovV93},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/1993,
  editor    = {Andrei Voronkov},
  title     = {Logic Programming and Automated Reasoning,4th International Conference,
               LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {698},
  publisher = {Springer},
  year      = {1993},
  url       = {https://doi.org/10.1007/3-540-56944-8},
  doi       = {10.1007/3-540-56944-8},
  isbn      = {3-540-56944-8},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/1993},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov92,
  author    = {Andrei Voronkov},
  title     = {Theorem Proving in Non-Standard Logics Based on the Inverse Method},
  booktitle = {Automated Deduction - CADE-11, 11th International Conference on Automated
               Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
  pages     = {648--662},
  year      = {1992},
  crossref  = {DBLP:conf/cade/1992},
  url       = {https://doi.org/10.1007/3-540-55602-8_198},
  doi       = {10.1007/3-540-55602-8_198},
  timestamp = {Sat, 20 May 2017 15:32:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Voronkov92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/iclp/Voronkov92,
  author    = {Andrei Voronkov},
  title     = {On Computability by Logic Programs},
  booktitle = {Informal Proceedings of the Workshop Structural Complexity and Recursion-theoretic
               methods in Logic-Programming, Washington, DC, November 13, 1992},
  pages     = {165},
  year      = {1992},
  crossref  = {DBLP:conf/iclp/1992w1},
  timestamp = {Mon, 02 Dec 2013 17:40:44 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/Voronkov92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/istcs/Voronkov92,
  author    = {Andrei Voronkov},
  title     = {Higher Order Functions in First Order Theory},
  booktitle = {Theory of Computing and Systems, ISTCS'92, Israel Symposium, Haifa,
               Israel, May 1992},
  pages     = {43--54},
  year      = {1992},
  crossref  = {DBLP:conf/istcs/1992},
  url       = {https://doi.org/10.1007/BFb0035165},
  doi       = {10.1007/BFb0035165},
  timestamp = {Sat, 20 May 2017 15:32:50 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/istcs/Voronkov92},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/1991,
  editor    = {Andrei Voronkov},
  title     = {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},
  series    = {Lecture Notes in Computer Science},
  volume    = {592},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/3-540-55460-2},
  doi       = {10.1007/3-540-55460-2},
  isbn      = {3-540-55460-2},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/1992,
  editor    = {Andrei Voronkov},
  title     = {Logic Programming and Automated Reasoning,International Conference
               LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {624},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/BFb0013043},
  doi       = {10.1007/BFb0013043},
  isbn      = {3-540-55727-X},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/1992},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/csl/Voronkov91,
  author    = {Andrei Voronkov},
  title     = {On Completeness of Program Synthesis Systems},
  booktitle = {Computer Science Logic, 5th Workshop, {CSL} '91, Berne, Switzerland,
               October 7-11, 1991, Proceedings},
  pages     = {411--418},
  year      = {1991},
  crossref  = {DBLP:conf/csl/1991},
  url       = {https://doi.org/10.1007/BFb0023785},
  doi       = {10.1007/BFb0023785},
  timestamp = {Sat, 20 May 2017 15:32:50 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/Voronkov91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/lpar/Voronkov91,
  author    = {Andrei Voronkov},
  title     = {Logic Programming with Bounded Quantifiers},
  booktitle = {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},
  pages     = {486--514},
  year      = {1991},
  crossref  = {DBLP:conf/lpar/1991},
  url       = {https://doi.org/10.1007/3-540-55460-2_37},
  doi       = {10.1007/3-540-55460-2_37},
  timestamp = {Sat, 20 May 2017 15:32:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/Voronkov91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/pdk/BoleyMMRV91,
  author    = {Harold Boley and
               Micha Meier and
               Chris Moss and
               Michael M. Richter and
               Andrei Voronkov},
  title     = {Declarative and Procedural Paradigms - Do they Really Compete? (Panel)},
  booktitle = {Processing Declarative Knowledge, International Workshop PDK'91, Kaiserslautern,
               Germany, July 1-3, 1991, Proceedings},
  pages     = {383--398},
  year      = {1991},
  crossref  = {DBLP:conf/pdk/1991},
  url       = {https://doi.org/10.1007/BFb0013545},
  doi       = {10.1007/BFb0013545},
  timestamp = {Sat, 20 May 2017 15:32:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pdk/BoleyMMRV91},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov90,
  author    = {Andrei Voronkov},
  title     = {{LISS} - The Logic Inference Search System},
  booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  pages     = {677--678},
  year      = {1990},
  crossref  = {DBLP:conf/cade/1990},
  url       = {https://doi.org/10.1007/3-540-52885-7_138},
  doi       = {10.1007/3-540-52885-7_138},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/Voronkov90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/esop/Voronkov90,
  author    = {Andrei Voronkov},
  title     = {Towards the Theory of Programming in Constructive Logic},
  booktitle = {ESOP'90, 3rd European Symposium on Programming, Copenhagen, Denmark,
               May 15-18, 1990, Proceedings},
  pages     = {421--435},
  year      = {1990},
  crossref  = {DBLP:conf/esop/1990},
  url       = {https://doi.org/10.1007/3-540-52592-0_78},
  doi       = {10.1007/3-540-52592-0_78},
  timestamp = {Fri, 19 May 2017 13:10:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/Voronkov90},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/colog/StarchenkoV88,
  author    = {Sergei Starchenko and
               Andrei Voronkov},
  title     = {On connections between classical and constructive semantics},
  booktitle = {COLOG-88, International Conference on Computer Logic, Tallinn, USSR,
               December 1988, Proceedings},
  pages     = {275--285},
  year      = {1988},
  crossref  = {DBLP:conf/colog/1988},
  url       = {https://doi.org/10.1007/3-540-52335-9_59},
  doi       = {10.1007/3-540-52335-9_59},
  timestamp = {Fri, 19 May 2017 13:10:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/colog/StarchenkoV88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/colog/Voronkov88,
  author    = {Andrei Voronkov},
  title     = {A proof-search method for the first-order logic},
  booktitle = {COLOG-88, International Conference on Computer Logic, Tallinn, USSR,
               December 1988, Proceedings},
  pages     = {327--338},
  year      = {1988},
  crossref  = {DBLP:conf/colog/1988},
  url       = {https://doi.org/10.1007/3-540-52335-9_63},
  doi       = {10.1007/3-540-52335-9_63},
  timestamp = {Fri, 19 May 2017 13:10:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/colog/Voronkov88},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fct/Voronkov87,
  author    = {Andrei Voronkov},
  title     = {Deductive Program Synthesis and Markov's Principle},
  booktitle = {Fundamentals of Computation Theory, International Conference FCT'87,
               Kazan, USSR, June 22-26, 1987, Proceedings},
  pages     = {479--482},
  year      = {1987},
  crossref  = {DBLP:conf/fct/1987},
  url       = {https://doi.org/10.1007/3-540-18740-5_105},
  doi       = {10.1007/3-540-18740-5_105},
  timestamp = {Fri, 19 May 2017 13:10:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fct/Voronkov87},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/2017,
  editor    = {Thomas Eiter and
               David Sands},
  title     = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
               Intelligence and Reasoning, Maun, Botswana, 7-12th May 2017},
  series    = {EPiC Series in Computing},
  volume    = {46},
  publisher = {EasyChair},
  year      = {2017},
  url       = {http://www.easychair.org/publications/volume/LPAR-21},
  timestamp = {Wed, 16 Aug 2017 16:30:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/2017},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2017,
  editor    = {Giuseppe Castagna and
               Andrew D. Gordon},
  title     = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
               Programming Languages, {POPL} 2017, Paris, France, January 18-20,
               2017},
  publisher = {{ACM}},
  year      = {2017},
  url       = {http://doi.acm.org/10.1145/3009837},
  doi       = {10.1145/3009837},
  isbn      = {978-1-4503-4660-3},
  timestamp = {Wed, 28 Dec 2016 13:17:00 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2017},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tap/2017,
  editor    = {Sebastian Gabmeyer and
               Einar Broch Johnsen},
  title     = {Tests and Proofs - 11th International Conference, {TAP} 2017, Held
               as Part of {STAF} 2017, Marburg, Germany, July 19-20, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10375},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-61467-0},
  doi       = {10.1007/978-3-319-61467-0},
  isbn      = {978-3-319-61466-3},
  timestamp = {Mon, 03 Jul 2017 15:54:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tap/2017},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2016,
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  title     = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9706},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-40229-1},
  doi       = {10.1007/978-3-319-40229-1},
  isbn      = {978-3-319-40228-4},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cpp/2016,
  editor    = {Jeremy Avigad and
               Adam Chlipala},
  title     = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
               and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
  publisher = {{ACM}},
  year      = {2016},
  url       = {http://dl.acm.org/citation.cfm?id=2854065},
  isbn      = {978-1-4503-4127-1},
  timestamp = {Mon, 18 Jan 2016 19:35:36 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/cpp/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/gcai/2016,
  editor    = {Christoph Benzm{\"{u}}ller and
               Geoff Sutcliffe and
               Ra{\'{u}}l Rojas},
  title     = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
               19 - October 2, 2016, Berlin, Germany},
  series    = {EPiC Series in Computing},
  volume    = {41},
  publisher = {EasyChair},
  year      = {2016},
  url       = {http://www.easychair.org/publications/volume/GCAI_2016},
  timestamp = {Wed, 26 Apr 2017 13:32:16 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/gcai/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sat/2016,
  editor    = {Nadia Creignou and
               Daniel Le Berre},
  title     = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th
               International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9710},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-40970-2},
  doi       = {10.1007/978-3-319-40970-2},
  isbn      = {978-3-319-40969-6},
  timestamp = {Tue, 23 May 2017 01:08:19 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sat/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2015,
  editor    = {Amy P. Felty and
               Aart Middeldorp},
  title     = {Automated Deduction - {CADE-25} - 25th International Conference on
               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-21401-6},
  doi       = {10.1007/978-3-319-21401-6},
  isbn      = {978-3-319-21400-9},
  timestamp = {Sun, 21 May 2017 00:17:17 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/mkm/2015,
  editor    = {Manfred Kerber and
               Jacques Carette and
               Cezary Kaliszyk and
               Florian Rabe and
               Volker Sorge},
  title     = {Intelligent Computer Mathematics - International Conference, {CICM}
               2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9150},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-20615-8},
  doi       = {10.1007/978-3-319-20615-8},
  isbn      = {978-3-319-20614-1},
  timestamp = {Sun, 04 Jun 2017 10:10:26 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mkm/2015},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/atva/2014,
  editor    = {Franck Cassez and
               Jean{-}Fran{\c{c}}ois Raskin},
  title     = {Automated Technology for Verification and Analysis - 12th International
               Symposium, {ATVA} 2014, Sydney, NSW, Australia, November 3-7, 2014,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8837},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-11936-6},
  doi       = {10.1007/978-3-319-11936-6},
  isbn      = {978-3-319-11935-9},
  timestamp = {Sun, 21 May 2017 00:22:26 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/atva/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2014-15vampire,
  editor    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  title     = {Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014,
               Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany,
               August 2, 2015},
  series    = {EPiC Series in Computing},
  volume    = {38},
  publisher = {EasyChair},
  year      = {2016},
  url       = {http://www.easychair.org/publications/volume/Vampire_2014_and_2015},
  timestamp = {Thu, 16 Jun 2016 17:11:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2014-15vampire},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cav/2014,
  editor    = {Armin Biere and
               Roderick Bloem},
  title     = {Computer Aided Verification - 26th International Conference, {CAV}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 18-22, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8559},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08867-9},
  doi       = {10.1007/978-3-319-08867-9},
  isbn      = {978-3-319-08866-2},
  timestamp = {Thu, 25 May 2017 00:39:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cav/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/kbse/2014,
  editor    = {Ivica Crnkovic and
               Marsha Chechik and
               Paul Gr{\"{u}}nbacher},
  title     = {{ACM/IEEE} International Conference on Automated Software Engineering,
               {ASE} '14, Vasteras, Sweden - September 15 - 19, 2014},
  publisher = {{ACM}},
  year      = {2014},
  url       = {http://dl.acm.org/citation.cfm?id=2642937},
  isbn      = {978-1-4503-3013-8},
  timestamp = {Wed, 29 Mar 2017 16:45:22 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/kbse/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/micai/2014-1,
  editor    = {Alexander F. Gelbukh and
               F{\'{e}}lix Castro{-}Espinoza and
               Sof{\'{\i}}a N. Galicia{-}Haro},
  title     = {Human-Inspired Computing and Its Applications - 13th Mexican International
               Conference on Artificial Intelligence, {MICAI} 2014, Tuxtla Guti{\'{e}}rrez,
               Mexico, November 16-22, 2014. Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8856},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-13647-9},
  doi       = {10.1007/978-3-319-13647-9},
  isbn      = {978-3-319-13646-2},
  timestamp = {Wed, 24 May 2017 08:27:28 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/micai/2014-1},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/birthday/2013ganzinger,
  editor    = {Andrei Voronkov and
               Christoph Weidenbach},
  title     = {Programming Logics - Essays in Memory of Harald Ganzinger},
  series    = {Lecture Notes in Computer Science},
  volume    = {7797},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-37651-1},
  doi       = {10.1007/978-3-642-37651-1},
  isbn      = {978-3-642-37650-4},
  timestamp = {Tue, 23 May 2017 01:06:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/2013ganzinger},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2013,
  editor    = {Maria Paola Bonacina},
  title     = {Automated Deduction - {CADE-24} - 24th International Conference on
               Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7898},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-38574-2},
  doi       = {10.1007/978-3-642-38574-2},
  isbn      = {978-3-642-38573-5},
  timestamp = {Sun, 21 May 2017 00:17:17 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cav/2013,
  editor    = {Natasha Sharygina and
               Helmut Veith},
  title     = {Computer Aided Verification - 25th International Conference, {CAV}
               2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8044},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-39799-8},
  doi       = {10.1007/978-3-642-39799-8},
  isbn      = {978-3-642-39798-1},
  timestamp = {Thu, 25 May 2017 00:39:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cav/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/doceng/2013,
  editor    = {Simone Marinai and
               Kim Marriott},
  title     = {{ACM} Symposium on Document Engineering 2013, DocEng '13, Florence,
               Italy, September 10-13, 2013},
  publisher = {{ACM}},
  year      = {2013},
  url       = {http://dl.acm.org/citation.cfm?id=2494266},
  isbn      = {978-1-4503-1789-4},
  timestamp = {Wed, 29 Mar 2017 16:45:24 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/doceng/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/micai/2013-1,
  editor    = {F{\'{e}}lix Castro{-}Espinoza and
               Alexander F. Gelbukh and
               Miguel Gonz{\'{a}}lez{-}Mendoza},
  title     = {Advances in Artificial Intelligence and Its Applications - 12th Mexican
               International Conference on Artificial Intelligence, {MICAI} 2013,
               Mexico City, Mexico, November 24-30, 2013, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {8265},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-45114-0},
  doi       = {10.1007/978-3-642-45114-0},
  isbn      = {978-3-642-45113-3},
  timestamp = {Sun, 04 Jun 2017 10:04:10 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/micai/2013-1},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/synasc/2013,
  editor    = {Nikolaj Bj{\o}rner and
               Viorel Negru and
               Tetsuo Ida and
               Tudor Jebelean and
               Dana Petcu and
               Stephen M. Watt and
               Daniela Zaharie},
  title     = {15th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2013, Timisoara, Romania, September
               23-26, 2013},
  publisher = {{IEEE} Computer Society},
  year      = {2013},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6820820},
  isbn      = {978-1-4799-3035-7},
  timestamp = {Tue, 13 Jan 2015 18:19:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/2013},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/aplas/2012,
  editor    = {Ranjit Jhala and
               Atsushi Igarashi},
  title     = {Programming Languages and Systems - 10th Asian Symposium, {APLAS}
               2012, Kyoto, Japan, December 11-13, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7705},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-35182-2},
  doi       = {10.1007/978-3-642-35182-2},
  isbn      = {978-3-642-35181-5},
  timestamp = {Fri, 19 May 2017 01:25:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/aplas/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2012,
  editor    = {Bernhard Gramlich and
               Dale Miller and
               Uli Sattler},
  title     = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
               2012, Manchester, UK, June 26-29, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-31365-3},
  doi       = {10.1007/978-3-642-31365-3},
  isbn      = {978-3-642-31364-6},
  timestamp = {Sun, 21 May 2017 00:17:17 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2012,
  editor    = {Gianpiero Cabodi and
               Satnam Singh},
  title     = {Formal Methods in Computer-Aided Design, {FMCAD} 2012, Cambridge,
               UK, October 22-25, 2012},
  publisher = {{IEEE}},
  year      = {2012},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6450168},
  isbn      = {978-1-4673-4832-4},
  timestamp = {Wed, 17 Feb 2016 13:08:35 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/fmcad/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/popl/2012,
  editor    = {John Field and
               Michael Hicks},
  title     = {Proceedings of the 39th {ACM} {SIGPLAN-SIGACT} Symposium on Principles
               of Programming Languages, {POPL} 2012, Philadelphia, Pennsylvania,
               USA, January 22-28, 2012},
  publisher = {{ACM}},
  year      = {2012},
  url       = {http://dl.acm.org/citation.cfm?id=2103656},
  isbn      = {978-1-4503-1083-3},
  timestamp = {Tue, 22 May 2012 15:24:56 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/popl/2012},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2011,
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie{-}Stokkermans},
  title     = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6803},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6},
  doi       = {10.1007/978-3-642-22438-6},
  isbn      = {978-3-642-22437-9},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2011,
  editor    = {Edmund M. Clarke and
               Irina Virbitskaite and
               Andrei Voronkov},
  title     = {Perspectives of Systems Informatics - 8th International Andrei Ershov
               Memorial Conference, {PSI} 2011, Novosibirsk, Russia, June 27-July
               1, 2011, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {7162},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-29709-0},
  doi       = {10.1007/978-3-642-29709-0},
  isbn      = {978-3-642-29708-3},
  timestamp = {Sun, 21 May 2017 00:18:10 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/micai/2011-1,
  editor    = {Ildar Z. Batyrshin and
               Grigori Sidorov},
  title     = {Advances in Artificial Intelligence - 10th Mexican International Conference
               on Artificial Intelligence, {MICAI} 2011, Puebla, Mexico, November
               26 - December 4, 2011, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {7094},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-25324-9},
  doi       = {10.1007/978-3-642-25324-9},
  isbn      = {978-3-642-25323-2},
  timestamp = {Wed, 24 May 2017 08:27:28 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/micai/2011-1},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tacas/2011,
  editor    = {Parosh Aziz Abdulla and
               K. Rustan M. Leino},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems
               - 17th International Conference, {TACAS} 2011, Held as Part of the
               Joint European Conferences on Theory and Practice of Software, {ETAPS}
               2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6605},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-19835-9},
  doi       = {10.1007/978-3-642-19835-9},
  isbn      = {978-3-642-19834-2},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tacas/2011},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2010,
  editor    = {J{\"{u}}rgen Giesl and
               Reiner H{\"{a}}hnle},
  title     = {Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010,
               Edinburgh, UK, July 16-19, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6173},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-14203-1},
  doi       = {10.1007/978-3-642-14203-1},
  isbn      = {978-3-642-14202-4},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2010,
  editor    = {Roderick Bloem and
               Natasha Sharygina},
  title     = {Proceedings of 10th International Conference on Formal Methods in
               Computer-Aided Design, {FMCAD} 2010, Lugano, Switzerland, October
               20-23},
  publisher = {{IEEE}},
  year      = {2010},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5766311},
  isbn      = {978-1-4577-0734-6},
  timestamp = {Wed, 17 Feb 2016 13:08:35 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/fmcad/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icms/2010,
  editor    = {Komei Fukuda and
               Joris van der Hoeven and
               Michael Joswig and
               Nobuki Takayama},
  title     = {Mathematical Software - {ICMS} 2010, Third International Congress
               on Mathematical Software, Kobe, Japan, September 13-17, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6327},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-15582-6},
  doi       = {10.1007/978-3-642-15582-6},
  isbn      = {978-3-642-15581-9},
  timestamp = {Sun, 04 Jun 2017 10:11:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icms/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/synasc/2010,
  editor    = {Tetsuo Ida and
               Viorel Negru and
               Tudor Jebelean and
               Dana Petcu and
               Stephen M. Watt and
               Daniela Zaharie},
  title     = {12th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2010, Timisoara, Romania, 23-26 September
               2010},
  publisher = {{IEEE} Computer Society},
  year      = {2010},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5714592},
  isbn      = {978-0-7695-4324-6},
  timestamp = {Tue, 13 Jan 2015 18:19:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/vmcai/2010,
  editor    = {Gilles Barthe and
               Manuel V. Hermenegildo},
  title     = {Verification, Model Checking, and Abstract Interpretation, 11th International
               Conference, {VMCAI} 2010, Madrid, Spain, January 17-19, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5944},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-11319-2},
  doi       = {10.1007/978-3-642-11319-2},
  isbn      = {978-3-642-11318-5},
  timestamp = {Wed, 24 May 2017 08:30:31 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/vmcai/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/wwv/2010,
  editor    = {Laura Kov{\'{a}}cs and
               Temur Kutsia},
  title     = {6th International Workshop on Automated Specification and Verification
               of Web Systems, {WWV} 2010, Vienna, Austria, July 30-31, 2010},
  series    = {EPiC Series in Computing},
  volume    = {18},
  publisher = {EasyChair},
  year      = {2013},
  url       = {http://www.easychair.org/publications/?page=1080130689},
  timestamp = {Thu, 16 Jun 2016 17:11:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/wwv/2010},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/dagstuhl/2010P10161,
  editor    = {Nikolaj Bj{\o}rner and
               Robert Nieuwenhuis and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010},
  series    = {Dagstuhl Seminar Proceedings},
  volume    = {10161},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, Germany},
  year      = {2010},
  url       = {http://drops.dagstuhl.de/portals/10161/},
  timestamp = {Thu, 09 Apr 2015 14:44:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/2010P10161},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2009,
  editor    = {Renate A. Schmidt},
  title     = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2},
  doi       = {10.1007/978-3-642-02959-2},
  isbn      = {978-3-642-02958-5},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cp/2009,
  editor    = {Ian P. Gent},
  title     = {Principles and Practice of Constraint Programming - {CP} 2009, 15th
               International Conference, {CP} 2009, Lisbon, Portugal, September 20-24,
               2009, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5732},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-04244-7},
  doi       = {10.1007/978-3-642-04244-7},
  isbn      = {978-3-642-04243-0},
  timestamp = {Wed, 17 May 2017 14:24:33 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cp/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fase/2009,
  editor    = {Marsha Chechik and
               Martin Wirsing},
  title     = {Fundamental Approaches to Software Engineering, 12th International
               Conference, {FASE} 2009, Held as Part of the Joint European Conferences
               on Theory and Practice of Software, {ETAPS} 2009, York, UK, March
               22-29, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5503},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-00593-0},
  doi       = {10.1007/978-3-642-00593-0},
  isbn      = {978-3-642-00592-3},
  timestamp = {Thu, 25 May 2017 00:41:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fase/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2009,
  title     = {Proceedings of 9th International Conference on Formal Methods in Computer-Aided
               Design, {FMCAD} 2009, 15-18 November 2009, Austin, Texas, {USA}},
  publisher = {{IEEE}},
  year      = {2009},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5344684},
  isbn      = {978-1-4244-4966-8},
  timestamp = {Wed, 17 Feb 2016 13:08:35 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/fmcad/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ki/2009,
  editor    = {B{\"{a}}rbel Mertsching and
               Marcus Hund and
               Muhammad Zaheer Aziz},
  title     = {{KI} 2009: Advances in Artificial Intelligence, 32nd Annual German
               Conference on AI, Paderborn, Germany, September 15-18, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5803},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-04617-9},
  doi       = {10.1007/978-3-642-04617-9},
  isbn      = {978-3-642-04616-2},
  timestamp = {Thu, 25 May 2017 00:42:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ki/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sas/2009,
  editor    = {Jens Palsberg and
               Zhendong Su},
  title     = {Static Analysis, 16th International Symposium, {SAS} 2009, Los Angeles,
               CA, USA, August 9-11, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5673},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-03237-0},
  doi       = {10.1007/978-3-642-03237-0},
  isbn      = {978-3-642-03236-3},
  timestamp = {Wed, 24 May 2017 08:27:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sas/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/synasc/2009,
  editor    = {Stephen M. Watt and
               Viorel Negru and
               Tetsuo Ida and
               Tudor Jebelean and
               Dana Petcu and
               Daniela Zaharie},
  title     = {11th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2009, Timisoara, Romania, September
               26-29, 2009},
  publisher = {{IEEE} Computer Society},
  year      = {2009},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5459479},
  isbn      = {978-1-4244-5910-0},
  timestamp = {Tue, 13 Jan 2015 18:19:55 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/synasc/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tacas/2009,
  editor    = {Stefan Kowalewski and
               Anna Philippou},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems,
               15th International Conference, {TACAS} 2009, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2009,
               York, UK, March 22-29, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5505},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-00768-2},
  doi       = {10.1007/978-3-642-00768-2},
  isbn      = {978-3-642-00767-5},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tacas/2009},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2008,
  editor    = {Alessandro Armando and
               Peter Baumgartner and
               Gilles Dowek},
  title     = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008,
               Sydney, Australia, August 12-15, 2008, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5195},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-71070-7},
  doi       = {10.1007/978-3-540-71070-7},
  isbn      = {978-3-540-71069-1},
  timestamp = {Tue, 13 Jun 2017 10:37:55 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2008},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2007,
  editor    = {Frank Pfenning},
  title     = {Automated Deduction - CADE-21, 21st International Conference on Automated
               Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4603},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73595-3},
  doi       = {10.1007/978-3-540-73595-3},
  isbn      = {978-3-540-73594-6},
  timestamp = {Fri, 02 Jun 2017 13:01:06 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csl/2007,
  editor    = {Jacques Duparc and
               Thomas A. Henzinger},
  title     = {Computer Science Logic, 21st International Workshop, {CSL} 2007, 16th
               Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15,
               2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4646},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-74915-8},
  doi       = {10.1007/978-3-540-74915-8},
  isbn      = {978-3-540-74914-1},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sat/2007,
  editor    = {Jo{\~{a}}o Marques{-}Silva and
               Karem A. Sakallah},
  title     = {Theory and Applications of Satisfiability Testing - {SAT} 2007, 10th
               International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4501},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-72788-0},
  doi       = {10.1007/978-3-540-72788-0},
  isbn      = {978-3-540-72787-3},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sat/2007},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/adbis/2006,
  editor    = {Yannis Manolopoulos and
               Jaroslav Pokorn{\'{y}} and
               Timos K. Sellis},
  title     = {Advances in Databases and Information Systems, 10th East European
               Conference, {ADBIS} 2006, Thessaloniki, Greece, September 3-7, 2006,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4152},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11827252},
  doi       = {10.1007/11827252},
  isbn      = {3-540-37899-5},
  timestamp = {Thu, 15 Jun 2017 21:42:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/adbis/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/foiks/2006,
  editor    = {J{\"{u}}rgen Dix and
               Stephen J. Hegner},
  title     = {Foundations of Information and Knowledge Systems, 4th International
               Symposium, FoIKS 2006, Budapest, Hungary, February 14-17, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3861},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11663881},
  doi       = {10.1007/11663881},
  isbn      = {3-540-31782-1},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/foiks/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icde/2006,
  editor    = {Ling Liu and
               Andreas Reuter and
               Kyu{-}Young Whang and
               Jianjun Zhang},
  title     = {Proceedings of the 22nd International Conference on Data Engineering,
               {ICDE} 2006, 3-8 April 2006, Atlanta, GA, {USA}},
  publisher = {{IEEE} Computer Society},
  year      = {2006},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10757},
  isbn      = {0-7695-2570-9},
  timestamp = {Fri, 21 Jul 2017 13:46:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icde/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/jelia/2006,
  editor    = {Michael Fisher and
               Wiebe van der Hoek and
               Boris Konev and
               Alexei Lisitsa},
  title     = {Logics in Artificial Intelligence, 10th European Conference, {JELIA}
               2006, Liverpool, UK, September 13-15, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4160},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11853886},
  doi       = {10.1007/11853886},
  isbn      = {3-540-39625-X},
  timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/jelia/2006},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/aaai/2005,
  editor    = {Manuela M. Veloso and
               Subbarao Kambhampati},
  title     = {Proceedings, The Twentieth National Conference on Artificial Intelligence
               and the Seventeenth Innovative Applications of Artificial Intelligence
               Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, {USA}},
  publisher = {{AAAI} Press / The {MIT} Press},
  year      = {2005},
  isbn      = {1-57735-236-X},
  timestamp = {Mon, 26 Feb 2007 09:10:53 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/aaai/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/birthday/2005siekmann,
  editor    = {Dieter Hutter and
               Werner Stephan},
  title     = {Mechanizing Mathematical Reasoning, Essays in Honor of J{\"{o}}rg
               H. Siekmann on the Occasion of His 60th Birthday},
  series    = {Lecture Notes in Computer Science},
  volume    = {2605},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/b106663},
  doi       = {10.1007/b106663},
  isbn      = {3-540-25051-4},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/birthday/2005siekmann},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/mfcs/2005,
  editor    = {Joanna Jedrzejowicz and
               Andrzej Szepietowski},
  title     = {Mathematical Foundations of Computer Science 2005, 30th International
               Symposium, {MFCS} 2005, Gdansk, Poland, August 29 - September 2, 2005,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3618},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11549345},
  doi       = {10.1007/11549345},
  isbn      = {3-540-28702-7},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/mfcs/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/sas/2005,
  editor    = {Chris Hankin and
               Igor Siveroni},
  title     = {Static Analysis, 12th International Symposium, {SAS} 2005, London,
               UK, September 7-9, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3672},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11547662},
  doi       = {10.1007/11547662},
  isbn      = {3-540-28584-9},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/sas/2005},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/dagstuhl/2005P5431,
  editor    = {Franz Baader and
               Peter Baumgartner and
               Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {Deduction and Applications, 23.-28. October 2005},
  series    = {Dagstuhl Seminar Proceedings},
  volume    = {05431},
  publisher = {Internationales Begegnungs- und Forschungszentrum f{\"{u}}r Informatik
               (IBFI), Schloss Dagstuhl, Germany},
  year      = {2006},
  url       = {http://drops.dagstuhl.de/portals/05431/},
  timestamp = {Wed, 19 Jun 2013 12:20:40 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dagstuhl/2005P5431},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2004,
  editor    = {David A. Basin and
               Micha{\"{e}}l Rusinowitch},
  title     = {Automated Reasoning - Second International Joint Conference, {IJCAR}
               2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3097},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b98691},
  doi       = {10.1007/b98691},
  isbn      = {3-540-22345-2},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2004},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2003,
  editor    = {Franz Baader},
  title     = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2741},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b11829},
  doi       = {10.1007/b11829},
  isbn      = {3-540-40559-3},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csl/2003,
  editor    = {Matthias Baaz and
               Johann A. Makowsky},
  title     = {Computer Science Logic, 17th International Workshop, {CSL} 2003, 12th
               Annual Conference of the EACSL, and 8th Kurt G{\"{o}}del Colloquium,
               {KGC} 2003, Vienna, Austria, August 25-30, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2803},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b13224},
  doi       = {10.1007/b13224},
  isbn      = {3-540-40801-0},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2003,
  editor    = {Manfred Broy and
               Alexandre V. Zamulin},
  title     = {Perspectives of Systems Informatics, 5th International Andrei Ershov
               Memorial Conference, {PSI} 2003, Akademgorodok, Novosibirsk, Russia,
               July 9-12, 2003, Revised Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {2890},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b94823},
  doi       = {10.1007/b94823},
  isbn      = {3-540-20813-5},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icalp/2003,
  editor    = {Jos C. M. Baeten and
               Jan Karel Lenstra and
               Joachim Parrow and
               Gerhard J. Woeginger},
  title     = {Automata, Languages and Programming, 30th International Colloquium,
               {ICALP} 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003.
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2719},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/3-540-45061-0},
  doi       = {10.1007/3-540-45061-0},
  isbn      = {3-540-40493-7},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ijcai/2003,
  editor    = {Georg Gottlob and
               Toby Walsh},
  title     = {IJCAI-03, Proceedings of the Eighteenth International Joint Conference
               on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003},
  publisher = {Morgan Kaufmann},
  year      = {2003},
  url       = {http://ijcai.org/proceedings/2003},
  timestamp = {Tue, 19 Jul 2016 16:02:31 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/2003,
  title     = {18th {IEEE} Symposium on Logic in Computer Science {(LICS} 2003),
               22-25 June 2003, Ottawa, Canada, Proceedings},
  publisher = {{IEEE} Computer Society},
  year      = {2003},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8592},
  isbn      = {0-7695-1884-2},
  timestamp = {Fri, 21 Nov 2014 14:08:55 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/2003},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/amast/2002,
  editor    = {H{\'{e}}l{\`{e}}ne Kirchner and
               Christophe Ringeissen},
  title     = {Algebraic Methodology and Software Technology, 9th International Conference,
               {AMAST} 2002, Saint-Gilles-les-Bains, Reunion Island, France, September
               9-13, 2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2422},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45719-4},
  doi       = {10.1007/3-540-45719-4},
  isbn      = {3-540-44144-1},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/amast/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cav/2002,
  editor    = {Ed Brinksma and
               Kim Guldstrand Larsen},
  title     = {Computer Aided Verification, 14th International Conference, {CAV}
               2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2404},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45657-0},
  doi       = {10.1007/3-540-45657-0},
  isbn      = {3-540-43997-8},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cav/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/dlog/2002,
  editor    = {Ian Horrocks and
               Sergio Tessaris},
  title     = {Proceedings of the 2002 International Workshop on Description Logics
               (DL2002), Toulouse, France, April 19-21, 2002},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {53},
  publisher = {CEUR-WS.org},
  year      = {2002},
  url       = {http://ceur-ws.org/Vol-53},
  urn       = {urn:nbn:de:0074-53-2},
  timestamp = {Mon, 30 May 2016 15:43:43 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/dlog/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fsttcs/2002,
  editor    = {Manindra Agrawal and
               Anil Seth},
  title     = {{FST} {TCS} 2002: Foundations of Software Technology and Theoretical
               Computer Science, 22nd Conference Kanpur, India, December 12-14, 2002,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2556},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-36206-1},
  doi       = {10.1007/3-540-36206-1},
  isbn      = {3-540-00225-1},
  timestamp = {Mon, 29 May 2017 16:53:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fsttcs/2002},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2001,
  editor    = {Rajeev Gor{\'{e}} and
               Alexander Leitsch and
               Tobias Nipkow},
  title     = {Automated Reasoning, First International Joint Conference, {IJCAR}
               2001, Siena, Italy, June 18-23, 2001, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2083},
  publisher = {Springer},
  year      = {2001},
  url       = {https://doi.org/10.1007/3-540-45744-5},
  doi       = {10.1007/3-540-45744-5},
  isbn      = {3-540-42254-4},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/2001,
  editor    = {Dines Bj{\o}rner and
               Manfred Broy and
               Alexandre V. Zamulin},
  title     = {Perspectives of System Informatics, 4th International Andrei Ershov
               Memorial Conference, {PSI} 2001, Akademgorodok, Novosibirsk, Russia,
               July 2-6, 2001, Revised Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {2244},
  publisher = {Springer},
  year      = {2001},
  url       = {https://doi.org/10.1007/3-540-45575-2},
  doi       = {10.1007/3-540-45575-2},
  isbn      = {3-540-43075-X},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icalp/2001,
  editor    = {Fernando Orejas and
               Paul G. Spirakis and
               Jan van Leeuwen},
  title     = {Automata, Languages and Programming, 28th International Colloquium,
               {ICALP} 2001, Crete, Greece, July 8-12, 2001, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2076},
  publisher = {Springer},
  year      = {2001},
  url       = {https://doi.org/10.1007/3-540-48224-5},
  doi       = {10.1007/3-540-48224-5},
  isbn      = {3-540-42287-0},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ijcai/2001,
  editor    = {Bernhard Nebel},
  title     = {Proceedings of the Seventeenth International Joint Conference on Artificial
               Intelligence, {IJCAI} 2001, Seattle, Washington, USA, August 4-10,
               2001},
  publisher = {Morgan Kaufmann},
  year      = {2001},
  url       = {http://ijcai.org/proceedings/2001-1},
  isbn      = {1-55860-777-3},
  timestamp = {Tue, 19 Jul 2016 16:01:40 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/rta/2001,
  editor    = {Aart Middeldorp},
  title     = {Rewriting Techniques and Applications, 12th International Conference,
               {RTA} 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2051},
  publisher = {Springer},
  year      = {2001},
  url       = {https://doi.org/10.1007/3-540-45127-7},
  doi       = {10.1007/3-540-45127-7},
  isbn      = {3-540-42117-3},
  timestamp = {Fri, 26 May 2017 14:09:14 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/2001},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@book{DBLP:books/el/RobinsonV01,
  editor    = {John Alan Robinson and
               Andrei Voronkov},
  title     = {Handbook of Automated Reasoning (in 2 volumes)},
  publisher = {Elsevier and {MIT} Press},
  year      = {2001},
  isbn      = {0-444-50813-9},
  timestamp = {Wed, 29 Mar 2017 16:45:21 +0200},
  biburl    = {http://dblp.org/rec/bib/books/el/RobinsonV01},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/arw/2000,
  editor    = {Hans J{\"{u}}rgen Ohlbach and
               Ulrich Endriss and
               Odinaldo Rodrigues and
               Stefan Schlobach},
  title     = {Proceedings of the Seventh Workshop on Automated Reasoning, Bridging
               the Gap between Theory and Practice, King's College London, UK, 20-21
               July 2000},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {32},
  publisher = {CEUR-WS.org},
  year      = {2000},
  url       = {http://ceur-ws.org/Vol-32},
  timestamp = {Fri, 25 Aug 2017 11:19:29 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/arw/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/2000,
  editor    = {David A. McAllester},
  title     = {Automated Deduction - CADE-17, 17th International Conference on Automated
               Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1831},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/10721959},
  doi       = {10.1007/10721959},
  isbn      = {3-540-67664-3},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/jelia/2000,
  editor    = {Manuel Ojeda{-}Aciego and
               Inman P. de Guzm{\'{a}}n and
               Gerhard Brewka and
               Lu{\'{\i}}s Moniz Pereira},
  title     = {Logics in Artificial Intelligence, European Workshop, {JELIA} 2000
               Malaga, Spain, September 29 - October 2, 2000, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1919},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/3-540-40006-0},
  doi       = {10.1007/3-540-40006-0},
  isbn      = {3-540-41131-3},
  timestamp = {Wed, 24 May 2017 15:40:44 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/jelia/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/kr/2000,
  editor    = {Anthony G. Cohn and
               Fausto Giunchiglia and
               Bart Selman},
  title     = {{KR} 2000, Principles of Knowledge Representation and Reasoning Proceedings
               of the Seventh International Conference, Breckenridge, Colorado, USA,
               April 11-15, 2000},
  publisher = {Morgan Kaufmann},
  year      = {2000},
  timestamp = {Fri, 18 May 2012 15:03:00 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/kr/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/2000,
  title     = {15th Annual {IEEE} Symposium on Logic in Computer Science, Santa Barbara,
               California, USA, June 26-29, 2000},
  publisher = {{IEEE} Computer Society},
  year      = {2000},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6908},
  isbn      = {0-7695-0725-5},
  timestamp = {Fri, 21 Nov 2014 14:08:55 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pods/00,
  editor    = {Victor Vianu and
               Georg Gottlob},
  title     = {Proceedings of the Nineteenth {ACM} {SIGMOD-SIGACT-SIGART} Symposium
               on Principles of Database Systems, May 15-17, 2000, Dallas, Texas,
               {USA}},
  publisher = {{ACM}},
  year      = {2000},
  url       = {http://dl.acm.org/citation.cfm?id=335168},
  isbn      = {1-58113-214-X},
  timestamp = {Wed, 29 Mar 2017 16:45:25 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pods/00},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tableaux/2000,
  editor    = {Roy Dyckhoff},
  title     = {Automated Reasoning with Analytic Tableaux and Related Methods, International
               Conference, {TABLEAUX} 2000, St Andrews, Scotland, UK, July 3-7, 2000,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1847},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/10722086},
  doi       = {10.1007/10722086},
  isbn      = {3-540-67697-X},
  timestamp = {Wed, 24 May 2017 15:40:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tableaux/2000},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1999,
  editor    = {Harald Ganzinger},
  title     = {Automated Deduction - CADE-16, 16th International Conference on Automated
               Deduction, Trento, Italy, July 7-10, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1632},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48660-7},
  doi       = {10.1007/3-540-48660-7},
  isbn      = {3-540-66222-7},
  timestamp = {Wed, 24 May 2017 15:40:41 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fossacs/1999,
  editor    = {Wolfgang Thomas},
  title     = {Foundations of Software Science and Computation Structure, Second
               International Conference, FoSSaCS'99, Held as Part of the European
               Joint Conferences on the Theory and Practice of Software, ETAPS'99,
               Amsterdam, The Netherlands, March 22-28, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1578},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-49019-1},
  doi       = {10.1007/3-540-49019-1},
  isbn      = {3-540-65719-3},
  timestamp = {Tue, 23 May 2017 14:54:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fossacs/1999},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1998,
  editor    = {Claude Kirchner and
               H{\'{e}}l{\`{e}}ne Kirchner},
  title     = {Automated Deduction - CADE-15, 15th International Conference on Automated
               Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1421},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0054239},
  doi       = {10.1007/BFb0054239},
  isbn      = {3-540-64675-2},
  timestamp = {Tue, 23 May 2017 11:53:57 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1998},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1998,
  title     = {Thirteenth Annual {IEEE} Symposium on Logic in Computer Science, Indianapolis,
               Indiana, USA, June 21-24, 1998},
  publisher = {{IEEE} Computer Society},
  year      = {1998},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=5684},
  isbn      = {0-8186-8506-9},
  timestamp = {Fri, 21 Nov 2014 14:08:56 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1998},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pods/98,
  editor    = {Alberto O. Mendelzon and
               Jan Paredaens},
  title     = {Proceedings of the Seventeenth {ACM} {SIGACT-SIGMOD-SIGART} Symposium
               on Principles of Database Systems, June 1-3, 1998, Seattle, Washington,
               {USA}},
  publisher = {{ACM} Press},
  year      = {1998},
  url       = {http://dl.acm.org/citation.cfm?id=275487},
  isbn      = {0-89791-996-3},
  timestamp = {Wed, 29 Mar 2017 16:45:24 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pods/98},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/rta/1998,
  editor    = {Tobias Nipkow},
  title     = {Rewriting Techniques and Applications, 9th International Conference,
               RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1379},
  publisher = {Springer},
  year      = {1998},
  url       = {https://doi.org/10.1007/BFb0052355},
  doi       = {10.1007/BFb0052355},
  isbn      = {3-540-64301-X},
  timestamp = {Tue, 23 May 2017 11:53:58 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/rta/1998},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/coco/1997,
  title     = {Proceedings of the Twelfth Annual {IEEE} Conference on Computational
               Complexity, Ulm, Germany, June 24-27, 1997},
  publisher = {{IEEE} Computer Society},
  year      = {1997},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4843},
  isbn      = {0-8186-7907-7},
  timestamp = {Fri, 13 May 2016 10:33:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/coco/1997},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/icalp/1997,
  editor    = {Pierpaolo Degano and
               Roberto Gorrieri and
               Alberto Marchetti{-}Spaccamela},
  title     = {Automata, Languages and Programming, 24th International Colloquium,
               ICALP'97, Bologna, Italy, 7-11 July 1997, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1256},
  publisher = {Springer},
  year      = {1997},
  url       = {https://doi.org/10.1007/3-540-63165-8},
  doi       = {10.1007/3-540-63165-8},
  isbn      = {3-540-63165-8},
  timestamp = {Mon, 22 May 2017 17:11:15 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/icalp/1997},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ijcai/1997,
  title     = {Proceedings of the Fifteenth International Joint Conference on Artificial
               Intelligence, {IJCAI} 97, Nagoya, Japan, August 23-29, 1997, 2 Volumes},
  publisher = {Morgan Kaufmann},
  year      = {1997},
  url       = {http://ijcai.org/proceedings/1997-1},
  timestamp = {Tue, 19 Jul 2016 15:27:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/1997},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lfcs/1997,
  editor    = {Sergei I. Adian and
               Anil Nerode},
  title     = {Logical Foundations of Computer Science, 4th International Symposium,
               LFCS'97, Yaroslavl, Russia, July 6-12, 1997, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1234},
  publisher = {Springer},
  year      = {1997},
  url       = {https://doi.org/10.1007/3-540-63045-7},
  doi       = {10.1007/3-540-63045-7},
  isbn      = {3-540-63045-7},
  timestamp = {Mon, 22 May 2017 17:11:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lfcs/1997},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1996,
  editor    = {Michael A. McRobbie and
               John K. Slaney},
  title     = {Automated Deduction - CADE-13, 13th International Conference on Automated
               Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1104},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61511-3},
  doi       = {10.1007/3-540-61511-3},
  isbn      = {3-540-61511-3},
  timestamp = {Mon, 22 May 2017 16:14:03 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/disco/1996,
  editor    = {Jacques Calmet and
               Carla Limongelli},
  title     = {Design and Implementation of Symbolic Computation Systems, International
               Symposium, {DISCO} '96, Karlsruhe, Germany, September 18-20, 1996,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1128},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61697-7},
  doi       = {10.1007/3-540-61697-7},
  isbn      = {3-540-61697-7},
  timestamp = {Mon, 22 May 2017 16:14:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/disco/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/elp/1996,
  editor    = {Roy Dyckhoff and
               Heinrich Herre and
               Peter Schroeder{-}Heister},
  title     = {Extensions of Logic Programming, 5th International Workshop, ELP'96,
               Leipzig, Germany, March 28-30, 1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1050},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-60983-0},
  doi       = {10.1007/3-540-60983-0},
  isbn      = {3-540-60983-0},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/elp/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ershov/1996,
  editor    = {Dines Bj{\o}rner and
               Manfred Broy and
               Igor V. Pottosin},
  title     = {Perspectives of System Informatics, Second International Andrei Ershov
               Memorial Conference, Akademgorodok, Novosibirsk, Russia, June 25-28,
               1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1181},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-62064-8},
  doi       = {10.1007/3-540-62064-8},
  isbn      = {3-540-62064-8},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ershov/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/jelia/1996,
  editor    = {Jos{\'{e}} J{\'{u}}lio Alferes and
               Lu{\'{\i}}s Moniz Pereira and
               Ewa Orlowska},
  title     = {Logics in Artificial Intelligence, European Workshop, {JELIA} '96,
               {\'{E}}vora, Portugal, September 30 - October 3, 1996, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1126},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61630-6},
  doi       = {10.1007/3-540-61630-6},
  isbn      = {3-540-61630-6},
  timestamp = {Mon, 22 May 2017 16:14:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/jelia/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lics/1996,
  title     = {Proceedings, 11th Annual {IEEE} Symposium on Logic in Computer Science,
               New Brunswick, New Jersey, USA, July 27-30, 1996},
  publisher = {{IEEE} Computer Society},
  year      = {1996},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4265},
  isbn      = {0-8186-7463-6},
  timestamp = {Fri, 21 Nov 2014 14:08:55 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/lics/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/tableaux/1996,
  editor    = {Pierangelo Miglioli and
               Ugo Moscato and
               Daniele Mundici and
               Mario Ornaghi},
  title     = {Theorem Proving with Analytic Tableaux and Related Methods, 5th International
               Workshop, {TABLEAUX} '96, Terrasini, Palermo, Italy, May 15-17, 1996,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1071},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61208-4},
  doi       = {10.1007/3-540-61208-4},
  isbn      = {3-540-61208-4},
  timestamp = {Mon, 22 May 2017 16:14:07 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/tableaux/1996},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csl/1995,
  editor    = {Hans Kleine B{\"{u}}ning},
  title     = {Computer Science Logic, 9th International Workshop, {CSL} '95, Annual
               Conference of the EACSL, Paderborn, Germany, September 22-29, 1995,
               Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {1092},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61377-3},
  doi       = {10.1007/3-540-61377-3},
  isbn      = {3-540-61377-3},
  timestamp = {Mon, 22 May 2017 16:14:05 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/1995},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/iclp/1995,
  editor    = {Leon Sterling},
  title     = {Logic Programming, Proceedings of the Twelfth International Conference
               on Logic Programming, Tokyo, Japan, June 13-16, 1995},
  publisher = {{MIT} Press},
  year      = {1995},
  isbn      = {0-262-69177-9},
  timestamp = {Mon, 02 Dec 2013 17:40:44 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/1995},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ijcai/1995,
  title     = {Proceedings of the Fourteenth International Joint Conference on Artificial
               Intelligence, {IJCAI} 95, Montr{\'{e}}al Qu{\'{e}}bec, Canada,
               August 20-25 1995, 2 Volumes},
  publisher = {Morgan Kaufmann},
  year      = {1995},
  url       = {http://ijcai.org/proceedings/1995-1},
  timestamp = {Tue, 19 Jul 2016 15:06:26 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/ijcai/1995},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/plilp/1994,
  editor    = {Manuel V. Hermenegildo and
               Jaan Penjam},
  title     = {Programming Language Implementation and Logic Programming, 6th International
               Symposium, PLILP'94, Madrid, Spain, September 14-16, 1994, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {844},
  publisher = {Springer},
  year      = {1994},
  url       = {https://doi.org/10.1007/3-540-58402-1},
  doi       = {10.1007/3-540-58402-1},
  isbn      = {3-540-58402-1},
  timestamp = {Sat, 20 May 2017 15:32:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/plilp/1994},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/kgc/1993,
  editor    = {Georg Gottlob and
               Alexander Leitsch and
               Daniele Mundici},
  title     = {Computational Logic and Proof Theory, Third Kurt G{\"{o}}del
               Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {713},
  publisher = {Springer},
  year      = {1993},
  url       = {https://doi.org/10.1007/BFb0022546},
  doi       = {10.1007/BFb0022546},
  isbn      = {3-540-57184-1},
  timestamp = {Sat, 20 May 2017 15:32:53 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/kgc/1993},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1992,
  editor    = {Deepak Kapur},
  title     = {Automated Deduction - CADE-11, 11th International Conference on Automated
               Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {607},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/3-540-55602-8},
  doi       = {10.1007/3-540-55602-8},
  isbn      = {3-540-55602-8},
  timestamp = {Sat, 20 May 2017 15:32:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1992},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/iclp/1992w1,
  editor    = {Howard A. Blair and
               V. Wiktor Marek and
               Anil Nerode and
               Jeffrey B. Remmel},
  title     = {Informal Proceedings of the Workshop Structural Complexity and Recursion-theoretic
               methods in Logic-Programming, Washington, DC, November 13, 1992},
  publisher = {Mathematical Sciences Institute, Cornell University},
  year      = {1992},
  timestamp = {Mon, 02 Dec 2013 17:40:44 +0100},
  biburl    = {http://dblp.org/rec/bib/conf/iclp/1992w1},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/istcs/1992,
  editor    = {Danny Dolev and
               Zvi Galil and
               Michael Rodeh},
  title     = {Theory of Computing and Systems, ISTCS'92, Israel Symposium, Haifa,
               Israel, May 1992},
  series    = {Lecture Notes in Computer Science},
  volume    = {601},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/BFb0035160},
  doi       = {10.1007/BFb0035160},
  isbn      = {3-540-55553-6},
  timestamp = {Sat, 20 May 2017 15:32:50 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/istcs/1992},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/csl/1991,
  editor    = {Egon B{\"{o}}rger and
               Gerhard J{\"{a}}ger and
               Hans Kleine B{\"{u}}ning and
               Michael M. Richter},
  title     = {Computer Science Logic, 5th Workshop, {CSL} '91, Berne, Switzerland,
               October 7-11, 1991, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {626},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/BFb0023753},
  doi       = {10.1007/BFb0023753},
  isbn      = {3-540-55789-X},
  timestamp = {Sat, 20 May 2017 15:32:50 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/csl/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/lpar/1991,
  editor    = {Andrei Voronkov},
  title     = {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},
  series    = {Lecture Notes in Computer Science},
  volume    = {592},
  publisher = {Springer},
  year      = {1992},
  url       = {https://doi.org/10.1007/3-540-55460-2},
  doi       = {10.1007/3-540-55460-2},
  isbn      = {3-540-55460-2},
  timestamp = {Sat, 20 May 2017 15:32:54 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/lpar/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/pdk/1991,
  editor    = {Harold Boley and
               Michael M. Richter},
  title     = {Processing Declarative Knowledge, International Workshop PDK'91, Kaiserslautern,
               Germany, July 1-3, 1991, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {567},
  publisher = {Springer},
  year      = {1991},
  url       = {https://doi.org/10.1007/BFb0013516},
  doi       = {10.1007/BFb0013516},
  isbn      = {3-540-55033-X},
  timestamp = {Sat, 20 May 2017 15:32:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/pdk/1991},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/cade/1990,
  editor    = {Mark E. Stickel},
  title     = {10th International Conference on Automated Deduction, Kaiserslautern,
               FRG, July 24-27, 1990, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {449},
  publisher = {Springer},
  year      = {1990},
  url       = {https://doi.org/10.1007/3-540-52885-7},
  doi       = {10.1007/3-540-52885-7},
  isbn      = {3-540-52885-7},
  timestamp = {Fri, 19 May 2017 13:10:45 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/cade/1990},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/esop/1990,
  editor    = {Neil D. Jones},
  title     = {ESOP'90, 3rd European Symposium on Programming, Copenhagen, Denmark,
               May 15-18, 1990, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {432},
  publisher = {Springer},
  year      = {1990},
  url       = {https://doi.org/10.1007/3-540-52592-0},
  doi       = {10.1007/3-540-52592-0},
  isbn      = {3-540-52592-0},
  timestamp = {Fri, 19 May 2017 13:10:46 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/esop/1990},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/colog/1988,
  editor    = {Per Martin{-}L{\"{o}}f and
               Grigori Mints},
  title     = {COLOG-88, International Conference on Computer Logic, Tallinn, USSR,
               December 1988, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {417},
  publisher = {Springer},
  year      = {1990},
  url       = {https://doi.org/10.1007/3-540-52335-9},
  doi       = {10.1007/3-540-52335-9},
  isbn      = {3-540-52335-9},
  timestamp = {Fri, 19 May 2017 13:10:49 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/colog/1988},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/fct/1987,
  editor    = {Lothar Budach and
               Rais Gatic Bakharajev and
               Oleg Borisovic Lipanov},
  title     = {Fundamentals of Computation Theory, International Conference FCT'87,
               Kazan, USSR, June 22-26, 1987, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {278},
  publisher = {Springer},
  year      = {1987},
  url       = {https://doi.org/10.1007/3-540-18740-5},
  doi       = {10.1007/3-540-18740-5},
  isbn      = {3-540-18740-5},
  timestamp = {Fri, 19 May 2017 13:10:47 +0200},
  biburl    = {http://dblp.org/rec/bib/conf/fct/1987},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
maintained by Schloss Dagstuhl LZI at University of Trier