Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Andrei Voronkov
@article{DBLP:journals/corr/abs-2402-18954,
author = {M{\'{a}}rton Hajd{\'{u}} and
Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Giles Reger and
Andrei Voronkov},
title = {Getting Saturated with Induction},
journal = {CoRR},
volume = {abs/2402.18954},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2402.18954},
doi = {10.48550/ARXIV.2402.18954},
eprinttype = {arXiv},
eprint = {2402.18954},
timestamp = {Tue, 26 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2402-18954.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2402-18962,
author = {Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Chase Norman and
Andrei Voronkov},
title = {Program Synthesis in Saturation},
journal = {CoRR},
volume = {abs/2402.18962},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2402.18962},
doi = {10.48550/ARXIV.2402.18962},
eprinttype = {arXiv},
eprint = {2402.18962},
timestamp = {Tue, 26 Mar 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2402-18962.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HozzovaKNV23,
author = {Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Chase Norman and
Andrei Voronkov},
editor = {Brigitte Pientka and
Cesare Tinelli},
title = {Program Synthesis in Saturation},
booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on
Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14132},
pages = {307--324},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-38499-8\_18},
doi = {10.1007/978-3-031-38499-8\_18},
timestamp = {Sun, 24 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/HozzovaKNV23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/KorovinKRSV23,
author = {Konstantin Korovin and
Laura Kov{\'{a}}cs and
Giles Reger and
Johannes Schoisswohl and
Andrei Voronkov},
editor = {Sriram Sankaranarayanan and
Natasha Sharygina},
title = {{ALASCA:} Reasoning in Quantified Linear Arithmetic},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 29th International Conference, {TACAS} 2023, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2022, Paris, France, April 22-27, 2023, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {13993},
pages = {647--665},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-30823-9\_33},
doi = {10.1007/978-3-031-30823-9\_33},
timestamp = {Wed, 17 May 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/KorovinKRSV23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2023,
editor = {Ruzica Piskac and
Andrei Voronkov},
title = {{LPAR} 2023: Proceedings of 24th International Conference on Logic
for Programming, Artificial Intelligence and Reasoning, Manizales,
Colombia, 4-9th June 2023},
series = {EPiC Series in Computing},
volume = {94},
publisher = {EasyChair},
year = {2023},
url = {https://www.easychair.org/publications/volume/LPAR\_2023},
timestamp = {Wed, 12 Jul 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2023.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/HajduHKRV22,
author = {M{\'{a}}rton Hajd{\'{u}} and
Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Giles Reger and
Andrei Voronkov},
editor = {Jean{-}Fran{\c{c}}ois Raskin and
Krishnendu Chatterjee and
Laurent Doyen and
Rupak Majumdar},
title = {Getting Saturated with Induction},
booktitle = {Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger
on the Occasion of His 60th Birthday},
series = {Lecture Notes in Computer Science},
volume = {13660},
pages = {306--322},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-22337-2\_15},
doi = {10.1007/978-3-031-22337-2\_15},
timestamp = {Tue, 31 Jan 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/birthday/HajduHKRV22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/paar/HajduKRV22,
author = {M{\'{a}}rton Hajd{\'{u}} and
Laura Kov{\'{a}}cs and
Michael Rawson and
Andrei Voronkov},
editor = {Boris Konev and
Claudia Schon and
Alexander Steen},
title = {The Vampire Approach to Induction (short paper)},
booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning
Co-located with the 11th International Joint Conference on Automated
Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11 - 12, 2022},
series = {{CEUR} Workshop Proceedings},
volume = {3201},
publisher = {CEUR-WS.org},
year = {2022},
url = {https://ceur-ws.org/Vol-3201/paper9.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:34 +0100},
biburl = {https://dblp.org/rec/conf/paar/HajduKRV22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HozzovaKV21,
author = {Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Andr{\'{e}} Platzer and
Geoff Sutcliffe},
title = {Integer Induction in Saturation},
booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on
Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12699},
pages = {361--377},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-79876-5\_21},
doi = {10.1007/978-3-030-79876-5\_21},
timestamp = {Thu, 29 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/HozzovaKV21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/HajduHKV21,
author = {M{\'{a}}rton Hajd{\'{u}} and
Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
title = {Induction with Recursive Definitions in Superposition},
booktitle = {Formal Methods in Computer Aided Design, {FMCAD} 2021, New Haven,
CT, USA, October 19-22, 2021},
pages = {1--10},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4\_34},
doi = {10.34727/2021/ISBN.978-3-85448-046-4\_34},
timestamp = {Tue, 07 Dec 2021 17:02:16 +0100},
biburl = {https://dblp.org/rec/conf/fmcad/HajduHKV21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/HajduHKSV21,
author = {M{\'{a}}rton Hajd{\'{u}} and
Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Johannes Schoisswohl and
Andrei Voronkov},
editor = {Fairouz Kamareddine and
Claudio Sacerdoti Coen},
title = {Inductive Benchmarks for Automated Reasoning},
booktitle = {Intelligent Computer Mathematics - 14th International Conference,
{CICM} 2021, Timisoara, Romania, July 26-31, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12833},
pages = {124--129},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-81097-9\_9},
doi = {10.1007/978-3-030-81097-9\_9},
timestamp = {Thu, 12 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mkm/HajduHKSV21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/RegerSV21,
author = {Giles Reger and
Johannes Schoisswohl and
Andrei Voronkov},
editor = {Jan Friso Groote and
Kim Guldstrand Larsen},
title = {Making Theory Reasoning Simpler},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 27th International Conference, {TACAS} 2021, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings,
Part {II}},
series = {Lecture Notes in Computer Science},
volume = {12652},
pages = {164--180},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-72013-1\_9},
doi = {10.1007/978-3-030-72013-1\_9},
timestamp = {Fri, 14 May 2021 08:34:19 +0200},
biburl = {https://dblp.org/rec/conf/tacas/RegerSV21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/HajduHKSV20,
author = {M{\'{a}}rton Hajd{\'{u}} and
Petra Hozzov{\'{a}} and
Laura Kov{\'{a}}cs and
Johannes Schoisswohl and
Andrei Voronkov},
editor = {Christoph Benzm{\"{u}}ller and
Bruce R. Miller},
title = {Induction with Generalization in Superposition Reasoning},
booktitle = {Intelligent Computer Mathematics - 13th International Conference,
{CICM} 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12236},
pages = {123--137},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-53518-6\_8},
doi = {10.1007/978-3-030-53518-6\_8},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mkm/HajduHKSV20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RegerV19,
author = {Giles Reger and
Andrei Voronkov},
editor = {Pascal Fontaine},
title = {Induction in Saturation-Based Proof Search},
booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on
Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11716},
pages = {477--494},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-29436-6\_28},
doi = {10.1007/978-3-030-29436-6\_28},
timestamp = {Fri, 27 Dec 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/RegerV19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2019,
editor = {Nikolaj S. Bj{\o}rner and
Irina B. Virbitskaite and
Andrei Voronkov},
title = {Perspectives of System Informatics - 12th International Andrei P.
Ershov Informatics Conference, {PSI} 2019, Novosibirsk, Russia, July
2-5, 2019, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {11964},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-37487-7},
doi = {10.1007/978-3-030-37487-7},
isbn = {978-3-030-37486-0},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ershov/2019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/vampire/2019,
editor = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
title = {Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops},
series = {EPiC Series in Computing},
volume = {71},
publisher = {EasyChair},
year = {2019},
url = {https://easychair.org/publications/volume/Vampire\_2019},
timestamp = {Wed, 11 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/vampire/2019.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/KotelnikovKV18,
author = {Evgenii Kotelnikov and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani},
title = {A FOOLish Encoding of the Next State Relations of Imperative Programs},
booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {405--421},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94205-6\_27},
doi = {10.1007/978-3-319-94205-6\_27},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/KotelnikovKV18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/Voronkov18,
author = {Andrei Voronkov},
title = {Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning},
booktitle = {20th International Symposium on Symbolic and Numeric Algorithms for
Scientific Computing, {SYNASC} 2018, Timisoara, Romania, September
20-23, 2018},
pages = {18},
publisher = {{IEEE}},
year = {2018},
url = {https://doi.org/10.1109/SYNASC.2018.00015},
doi = {10.1109/SYNASC.2018.00015},
timestamp = {Wed, 16 Oct 2019 14:14:55 +0200},
biburl = {https://dblp.org/rec/conf/synasc/Voronkov18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/Reger0V18,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Dirk Beyer and
Marieke Huisman},
title = {Unification with Abstraction and Theory Instantiation in Saturation-Based
Reasoning},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 24th International Conference, {TACAS} 2018, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {10805},
pages = {3--22},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-89960-2\_1},
doi = {10.1007/978-3-319-89960-2\_1},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/tacas/Reger0V18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2017,
editor = {Alexander K. Petrenko and
Andrei Voronkov},
title = {Perspectives of System Informatics - 11th International Andrei P.
Ershov Informatics Conference, {PSI} 2017, Moscow, Russia, June 27-29,
2017, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {10742},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-74313-4},
doi = {10.1007/978-3-319-74313-4},
isbn = {978-3-319-74312-7},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ershov/2017.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/KovacsV17,
author = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Thomas Eiter and
David Sands},
title = {First-Order Interpolation and Interpolating Proof Systems},
booktitle = {LPAR-21, 21st International Conference on Logic for Programming, Artificial
Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
series = {EPiC Series in Computing},
volume = {46},
pages = {49--64},
publisher = {EasyChair},
year = {2017},
url = {https://doi.org/10.29007/1qb8},
doi = {10.29007/1QB8},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/KovacsV17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/KovacsRV17,
author = {Laura Kov{\'{a}}cs and
Simon Robillard and
Andrei Voronkov},
editor = {Giuseppe Castagna and
Andrew D. Gordon},
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},
publisher = {{ACM}},
year = {2017},
url = {https://doi.org/10.1145/3009837.3009887},
doi = {10.1145/3009837.3009887},
timestamp = {Mon, 05 Feb 2024 20:33:37 +0100},
biburl = {https://dblp.org/rec/conf/popl/KovacsRV17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/RegerSV17,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Martin Brain and
Liana Hadarean},
title = {Instantiation and Pretending to be an {SMT} Solver with Vampire},
booktitle = {Proceedings of the 15th International Workshop on Satisfiability Modulo
Theories affiliated with the International Conference on Computer-Aided
Verification {(CAV} 2017), Heidelberg, Germany, July 22 - 23, 2017},
series = {{CEUR} Workshop Proceedings},
volume = {1889},
pages = {63--75},
publisher = {CEUR-WS.org},
year = {2017},
url = {https://ceur-ws.org/Vol-1889/paper6.pdf},
timestamp = {Fri, 10 Mar 2023 16:22:48 +0100},
biburl = {https://dblp.org/rec/conf/smt/RegerSV17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tap/Reger0V17,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Sebastian Gabmeyer and
Einar Broch Johnsen},
title = {Testing a Saturation-Based Theorem Prover: Experiences and Challenges},
booktitle = {Tests and Proofs - 11th International Conference, TAP@STAF 2017, Marburg,
Germany, July 19-20, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10375},
pages = {152--161},
publisher = {Springer},
year = {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 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/tap/Reger0V17.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/Vampire\_2016},
timestamp = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/2016vampire.bib},
bibsource = {dblp computer science bibliography, https://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 = {Thu, 19 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2017iwil.bib},
bibsource = {dblp computer science bibliography, https://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},
eprinttype = {arXiv},
eprint = {1704.03391},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Reger0V17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderR0V16,
author = {Krystof Hoder and
Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Nicola Olivetti and
Ashish Tiwari},
title = {Selecting the Selection},
booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9706},
pages = {313--329},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-40229-1\_22},
doi = {10.1007/978-3-319-40229-1\_22},
timestamp = {Mon, 26 Jun 2023 20:45:22 +0200},
biburl = {https://dblp.org/rec/conf/cade/HoderR0V16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/KotelnikovKRV16,
author = {Evgenii Kotelnikov and
Laura Kov{\'{a}}cs and
Giles Reger and
Andrei Voronkov},
editor = {Jeremy Avigad and
Adam Chlipala},
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},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2854065.2854071},
doi = {10.1145/2854065.2854071},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/KotelnikovKRV16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/gcai/Reger0V16,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Christoph Benzm{\"{u}}ller and
Geoff Sutcliffe and
Ra{\'{u}}l Rojas},
title = {New Techniques in Clausal Form Generation},
booktitle = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
19 - October 2, 2016, Berlin, Germany},
series = {EPiC Series in Computing},
volume = {41},
pages = {11--23},
publisher = {EasyChair},
year = {2016},
url = {https://doi.org/10.29007/dzfz},
doi = {10.29007/DZFZ},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/gcai/Reger0V16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/gcai/RegerB0V16,
author = {Giles Reger and
Nikolaj S. Bj{\o}rner and
Martin Suda and
Andrei Voronkov},
editor = {Christoph Benzm{\"{u}}ller and
Geoff Sutcliffe and
Ra{\'{u}}l Rojas},
title = {{AVATAR} Modulo Theories},
booktitle = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
19 - October 2, 2016, Berlin, Germany},
series = {EPiC Series in Computing},
volume = {41},
pages = {39--52},
publisher = {EasyChair},
year = {2016},
url = {https://doi.org/10.29007/k6tp},
doi = {10.29007/K6TP},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/gcai/RegerB0V16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/gcai/KotelnikovK0V16,
author = {Evgenii Kotelnikov and
Laura Kov{\'{a}}cs and
Martin Suda and
Andrei Voronkov},
editor = {Christoph Benzm{\"{u}}ller and
Geoff Sutcliffe and
Ra{\'{u}}l Rojas},
title = {A Clausal Normal Form Translation for {FOOL}},
booktitle = {{GCAI} 2016. 2nd Global Conference on Artificial Intelligence, September
19 - October 2, 2016, Berlin, Germany},
series = {EPiC Series in Computing},
volume = {41},
pages = {53--71},
publisher = {EasyChair},
year = {2016},
url = {https://doi.org/10.29007/ltkk},
doi = {10.29007/LTKK},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/gcai/KotelnikovK0V16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sat/Reger0V16,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Nadia Creignou and
Daniel Le Berre},
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},
series = {Lecture Notes in Computer Science},
volume = {9710},
pages = {323--341},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-40970-2\_20},
doi = {10.1007/978-3-319-40970-2\_20},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/sat/Reger0V16.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/Vampire\_2014\_and\_2015},
timestamp = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/2014-15vampire.bib},
bibsource = {dblp computer science bibliography, https://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 = {Sun, 02 Jun 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ershov/2015.bib},
bibsource = {dblp computer science bibliography, https://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},
eprinttype = {arXiv},
eprint = {1604.08040},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Reger0V16.bib},
bibsource = {dblp computer science bibliography, https://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},
eprinttype = {arXiv},
eprint = {1604.08055},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Reger0VH16.bib},
bibsource = {dblp computer science bibliography, https://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},
eprinttype = {arXiv},
eprint = {1611.02908},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KovacsRV16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RegerTV15,
author = {Giles Reger and
Dmitry Tishkovsky and
Andrei Voronkov},
editor = {Amy P. Felty and
Aart Middeldorp},
title = {Cooperating Proof Attempts},
booktitle = {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},
pages = {339--355},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21401-6\_23},
doi = {10.1007/978-3-319-21401-6\_23},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/RegerTV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RegerSV15,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Amy P. Felty and
Aart Middeldorp},
title = {Playing with {AVATAR}},
booktitle = {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},
pages = {399--415},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21401-6\_28},
doi = {10.1007/978-3-319-21401-6\_28},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/RegerSV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/KotelnikovKV15,
author = {Evgenii Kotelnikov and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Manfred Kerber and
Jacques Carette and
Cezary Kaliszyk and
Florian Rabe and
Volker Sorge},
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},
series = {Lecture Notes in Computer Science},
volume = {9150},
pages = {71--86},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-20615-8\_5},
doi = {10.1007/978-3-319-20615-8\_5},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mkm/KotelnikovKV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2014,
editor = {Andrei Voronkov and
Irina B. 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 = {Mon, 16 Dec 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ershov/2014.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/GCAI\_2015},
timestamp = {Fri, 05 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/gcai/2015.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/LPAR-20},
timestamp = {Wed, 10 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lpar/2015s.bib},
bibsource = {dblp computer science bibliography, https://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 = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lpar/2015.bib},
bibsource = {dblp computer science bibliography, https://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},
eprinttype = {arXiv},
eprint = {1505.01682},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KotelnikovKV15.bib},
bibsource = {dblp computer science bibliography, https://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},
eprinttype = {arXiv},
eprint = {1510.04821},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KotelnikovKRV15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/atva/GuptaKKV14,
author = {Ashutosh Gupta and
Laura Kov{\'{a}}cs and
Bernhard Kragl and
Andrei Voronkov},
editor = {Franck Cassez and
Jean{-}Fran{\c{c}}ois Raskin},
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},
series = {Lecture Notes in Computer Science},
volume = {8837},
pages = {185--200},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-11936-6\_14},
doi = {10.1007/978-3-319-11936-6\_14},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/atva/GuptaKKV14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BiereDKV14,
author = {Armin Biere and
Ioan Dragan and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {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},
series = {EPiC Series in Computing},
volume = {38},
pages = {29--32},
publisher = {EasyChair},
year = {2014},
url = {https://doi.org/10.29007/5l47},
doi = {10.29007/5L47},
timestamp = {Thu, 14 Oct 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BiereDKV14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Reger0V14,
author = {Giles Reger and
Martin Suda and
Andrei Voronkov},
editor = {Laura Kov{\'{a}}cs 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},
series = {EPiC Series in Computing},
volume = {38},
pages = {70--74},
publisher = {EasyChair},
year = {2014},
url = {https://doi.org/10.29007/1ffk},
doi = {10.29007/1FFK},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/Reger0V14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/Voronkov14,
author = {Andrei Voronkov},
editor = {Armin Biere and
Roderick Bloem},
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},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {696--710},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08867-9\_46},
doi = {10.1007/978-3-319-08867-9\_46},
timestamp = {Mon, 03 Jan 2022 22:13:44 +0100},
biburl = {https://dblp.org/rec/conf/cav/Voronkov14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/kbse/Voronkov14,
author = {Andrei Voronkov},
editor = {Ivica Crnkovic and
Marsha Chechik and
Paul Gr{\"{u}}nbacher},
title = {Keynote talk: EasyChair},
booktitle = {{ACM/IEEE} International Conference on Automated Software Engineering,
{ASE} '14, Vasteras, Sweden - September 15 - 19, 2014},
pages = {3--4},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2642937.2643085},
doi = {10.1145/2642937.2643085},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/kbse/Voronkov14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/micai/BiereDKV14,
author = {Armin Biere and
Ioan Dragan and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Alexander F. Gelbukh and
F{\'{e}}lix Castro{-}Espinoza and
Sof{\'{\i}}a N. Galicia{-}Haro},
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}},
series = {Lecture Notes in Computer Science},
volume = {8856},
pages = {431--442},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-13647-9\_39},
doi = {10.1007/978-3-319-13647-9\_39},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/micai/BiereDKV14.bib},
bibsource = {dblp computer science bibliography, https://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 = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/birthday/2014howard.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2014p,
editor = {Irina B. 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 = {https://easychair.org/publications/volume/PSI\_2014},
timestamp = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ershov/2014p.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/LPAR-19},
timestamp = {Wed, 10 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lpar/2013s.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/SCSS\_2014},
timestamp = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/sycss/2014.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/KapurNVWW13,
author = {Deepak Kapur and
Robert Nieuwenhuis and
Andrei Voronkov and
Christoph Weidenbach and
Reinhard Wilhelm},
editor = {Andrei Voronkov and
Christoph Weidenbach},
title = {Harald Ganzinger's Legacy: Contributions to Logics and Programming},
booktitle = {Programming Logics - Essays in Memory of Harald Ganzinger},
series = {Lecture Notes in Computer Science},
volume = {7797},
pages = {1--18},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-37651-1\_1},
doi = {10.1007/978-3-642-37651-1\_1},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/birthday/KapurNVWW13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/PerezV13,
author = {Juan Antonio Navarro P{\'{e}}rez and
Andrei Voronkov},
editor = {Andrei Voronkov and
Christoph Weidenbach},
title = {Planning with Effectively Propositional Logic},
booktitle = {Programming Logics - Essays in Memory of Harald Ganzinger},
series = {Lecture Notes in Computer Science},
volume = {7797},
pages = {302--316},
publisher = {Springer},
year = {2013},
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:00:00 +0200},
biburl = {https://dblp.org/rec/conf/birthday/PerezV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderV13,
author = {Krystof Hoder and
Andrei Voronkov},
editor = {Maria Paola Bonacina},
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},
series = {Lecture Notes in Computer Science},
volume = {7898},
pages = {450--464},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-38574-2\_33},
doi = {10.1007/978-3-642-38574-2\_33},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/HoderV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/KovacsV13,
author = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Natasha Sharygina and
Helmut Veith},
title = {First-Order Theorem Proving and Vampire},
booktitle = {Computer Aided Verification - 25th International Conference, {CAV}
2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8044},
pages = {1--35},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39799-8\_1},
doi = {10.1007/978-3-642-39799-8\_1},
timestamp = {Wed, 07 Dec 2022 23:12:58 +0100},
biburl = {https://dblp.org/rec/conf/cav/KovacsV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/doceng/ConstantinPV13,
author = {Alexandru Constantin and
Steve Pettifer and
Andrei Voronkov},
editor = {Simone Marinai and
Kim Marriott},
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},
publisher = {{ACM}},
year = {2013},
url = {https://doi.org/10.1145/2494266.2494271},
doi = {10.1145/2494266.2494271},
timestamp = {Wed, 14 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/doceng/ConstantinPV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/micai/KovacsMV13,
author = {Laura Kov{\'{a}}cs and
Andrei Mantsivoda and
Andrei Voronkov},
editor = {F{\'{e}}lix Castro{-}Espinoza and
Alexander F. Gelbukh and
Miguel Gonz{\'{a}}lez{-}Mendoza},
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}},
series = {Lecture Notes in Computer Science},
volume = {8265},
pages = {12--23},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-45114-0\_2},
doi = {10.1007/978-3-642-45114-0\_2},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/micai/KovacsMV13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/DraganKKV13,
author = {Ioan Dragan and
Konstantin Korovin and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Nikolaj S. Bj{\o}rner and
Viorel Negru and
Tetsuo Ida and
Tudor Jebelean and
Dana Petcu and
Stephen M. Watt and
Daniela Zaharie},
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},
publisher = {{IEEE} Computer Society},
year = {2013},
url = {https://doi.org/10.1109/SYNASC.2013.30},
doi = {10.1109/SYNASC.2013.30},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/synasc/DraganKKV13.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/birthday/2013ganzinger.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/LPAR-17-short},
timestamp = {Wed, 10 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lpar/2010ys.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2013.bib},
bibsource = {dblp computer science bibliography, https://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. Appl. Log.},
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 = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/japll/SakumaMV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aplas/HoderHKV12,
author = {Krystof Hoder and
Andreas Holzer and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Ranjit Jhala and
Atsushi Igarashi},
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},
series = {Lecture Notes in Computer Science},
volume = {7705},
pages = {148--156},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-35182-2\_11},
doi = {10.1007/978-3-642-35182-2\_11},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/aplas/HoderHKV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/EmmerKKSV12,
author = {Moshe Emmer and
Zurab Khasidashvili and
Konstantin Korovin and
Christoph Sticksel and
Andrei Voronkov},
editor = {Bernhard Gramlich and
Dale Miller and
Uli Sattler},
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},
series = {Lecture Notes in Computer Science},
volume = {7364},
pages = {210--224},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-31365-3\_18},
doi = {10.1007/978-3-642-31365-3\_18},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/EmmerKKSV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/HoderKKV12,
author = {Krystof Hoder and
Zurab Khasidashvili and
Konstantin Korovin and
Andrei Voronkov},
editor = {Gianpiero Cabodi and
Satnam Singh},
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},
publisher = {{IEEE}},
year = {2012},
url = {https://ieeexplore.ieee.org/document/6462554/},
timestamp = {Mon, 09 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/HoderKKV12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/popl/HoderKV12,
author = {Krystof Hoder and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {John Field and
Michael Hicks},
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},
publisher = {{ACM}},
year = {2012},
url = {https://doi.org/10.1145/2103656.2103689},
doi = {10.1145/2103656.2103689},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/popl/HoderKV12.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://easychair.org/publications/volume/Turing-100},
timestamp = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/birthday/2012turing.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2010wing,
editor = {Andrei Voronkov and
Laura Kov{\'{a}}cs and
Nikolaj S. 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 = {https://easychair.org/publications/volume/WING\_2010},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/2010wing.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2011,
editor = {Edmund M. Clarke and
Irina B. 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 = {Mon, 16 Dec 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ershov/2011.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2012,
editor = {Nikolaj S. 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 = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2012.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://ieeexplore.ieee.org/xpl/conhome/6480928/proceeding},
isbn = {978-1-4673-5026-6},
timestamp = {Wed, 16 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/synasc/2012.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderV11,
author = {Krystof Hoder and
Andrei Voronkov},
editor = {Nikolaj S. Bj{\o}rner and
Viorica Sofronie{-}Stokkermans},
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},
series = {Lecture Notes in Computer Science},
volume = {6803},
pages = {299--314},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22438-6\_23},
doi = {10.1007/978-3-642-22438-6\_23},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/HoderV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/KorovinV11,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Nikolaj S. Bj{\o}rner and
Viorica Sofronie{-}Stokkermans},
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},
series = {Lecture Notes in Computer Science},
volume = {6803},
pages = {369--383},
publisher = {Springer},
year = {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 = {https://dblp.org/rec/conf/cade/KorovinV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/KovacsMV11,
author = {Laura Kov{\'{a}}cs and
Georg Moser and
Andrei Voronkov},
editor = {Nikolaj S. Bj{\o}rner and
Viorica Sofronie{-}Stokkermans},
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},
series = {Lecture Notes in Computer Science},
volume = {6803},
pages = {384--399},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22438-6\_29},
doi = {10.1007/978-3-642-22438-6\_29},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/KovacsMV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ershov/KorovinV11,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Edmund M. Clarke and
Irina B. Virbitskaite 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},
series = {Lecture Notes in Computer Science},
volume = {7162},
pages = {243--250},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-29709-0\_21},
doi = {10.1007/978-3-642-29709-0\_21},
timestamp = {Mon, 16 Dec 2019 13:26:25 +0100},
biburl = {https://dblp.org/rec/conf/ershov/KorovinV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ershov/KorovinTV11,
author = {Konstantin Korovin and
Nestan Tsiskaridze and
Andrei Voronkov},
editor = {Edmund M. Clarke and
Irina B. Virbitskaite 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},
series = {Lecture Notes in Computer Science},
volume = {7162},
pages = {362--376},
publisher = {Springer},
year = {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 = {https://dblp.org/rec/conf/ershov/KorovinTV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/micai/HoderKV11,
author = {Krystof Hoder and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Ildar Z. Batyrshin and
Grigori Sidorov},
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}},
series = {Lecture Notes in Computer Science},
volume = {7094},
pages = {1--15},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-25324-9\_1},
doi = {10.1007/978-3-642-25324-9\_1},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/micai/HoderKV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/HoderKV11,
author = {Krystof Hoder and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Parosh Aziz Abdulla and
K. Rustan M. Leino},
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},
series = {Lecture Notes in Computer Science},
volume = {6605},
pages = {60--64},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-19835-9\_7},
doi = {10.1007/978-3-642-19835-9\_7},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/HoderKV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/BjornerNVV11,
author = {Nikolaj S. 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 = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/dagstuhl-reports/BjornerNVV11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HoderKV10,
author = {Krystof Hoder and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {J{\"{u}}rgen Giesl and
Reiner H{\"{a}}hnle},
title = {Interpolation and Symbol Elimination in Vampire},
booktitle = {Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010,
Edinburgh, UK, July 16-19, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6173},
pages = {188--195},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14203-1\_16},
doi = {10.1007/978-3-642-14203-1\_16},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/HoderKV10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/EmmerKKV10,
author = {Moshe Emmer and
Zurab Khasidashvili and
Konstantin Korovin and
Andrei Voronkov},
editor = {Roderick Bloem and
Natasha Sharygina},
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},
publisher = {{IEEE}},
year = {2010},
url = {https://ieeexplore.ieee.org/document/5770942/},
timestamp = {Mon, 09 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/EmmerKKV10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icms/UrbanHV10,
author = {Josef Urban and
Krystof Hoder and
Andrei Voronkov},
editor = {Komei Fukuda and
Joris van der Hoeven and
Michael Joswig and
Nobuki Takayama},
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},
series = {Lecture Notes in Computer Science},
volume = {6327},
pages = {155--166},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-15582-6\_30},
doi = {10.1007/978-3-642-15582-6\_30},
timestamp = {Mon, 28 Aug 2023 21:17:32 +0200},
biburl = {https://dblp.org/rec/conf/icms/UrbanHV10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/MinamideSV10,
author = {Yasuhiko Minamide and
Yuto Sakuma and
Andrei Voronkov},
editor = {Tetsuo Ida and
Viorel Negru and
Tudor Jebelean and
Dana Petcu and
Stephen M. Watt and
Daniela Zaharie},
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},
publisher = {{IEEE} Computer Society},
year = {2010},
url = {https://doi.org/10.1109/SYNASC.2010.50},
doi = {10.1109/SYNASC.2010.50},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/synasc/MinamideSV10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/vmcai/HenzingerHKV10,
author = {Thomas A. Henzinger and
Thibaud Hottelier and
Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Gilles Barthe and
Manuel V. Hermenegildo},
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},
series = {Lecture Notes in Computer Science},
volume = {5944},
pages = {163--179},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11319-2\_14},
doi = {10.1007/978-3-642-11319-2\_14},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/vmcai/HenzingerHKV10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/wwv/Voronkov10,
author = {Andrei Voronkov},
editor = {Laura Kov{\'{a}}cs and
Temur Kutsia},
title = {EasyChair},
booktitle = {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},
pages = {2},
publisher = {EasyChair},
year = {2010},
url = {https://doi.org/10.29007/n94r},
doi = {10.29007/N94R},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/wwv/Voronkov10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/dagstuhl/2010P10161,
editor = {Nikolaj S. 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 = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/2010P10161.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2009,
editor = {Amir Pnueli and
Irina B. 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 = {Mon, 16 Dec 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ershov/2009.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2010d.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2010y.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BjornerNVV10,
author = {Nikolaj S. Bj{\o}rner and
Robert Nieuwenhuis and
Helmut Veith and
Andrei Voronkov},
editor = {Nikolaj S. 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},
series = {Dagstuhl Seminar Proceedings},
volume = {10161},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, Germany},
year = {2010},
url = {http://drops.dagstuhl.de/opus/volltexte/2010/2742/},
timestamp = {Sun, 02 Oct 2022 15:58:47 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/BjornerNVV10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BjornerNVV10a,
author = {Nikolaj S. Bj{\o}rner and
Robert Nieuwenhuis and
Helmut Veith and
Andrei Voronkov},
editor = {Nikolaj S. 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},
series = {Dagstuhl Seminar Proceedings},
volume = {10161},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik, Germany},
year = {2010},
url = {http://drops.dagstuhl.de/opus/volltexte/2010/2736/},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/BjornerNVV10a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/KovacsV09,
author = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Renate A. Schmidt},
title = {Interpolation and Symbol Elimination},
booktitle = {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},
pages = {199--213},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02959-2\_17},
doi = {10.1007/978-3-642-02959-2\_17},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/KovacsV09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cp/KorovinTV09,
author = {Konstantin Korovin and
Nestan Tsiskaridze and
Andrei Voronkov},
editor = {Ian P. Gent},
title = {Conflict Resolution},
booktitle = {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},
pages = {509--523},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04244-7\_41},
doi = {10.1007/978-3-642-04244-7\_41},
timestamp = {Tue, 14 May 2019 10:00:45 +0200},
biburl = {https://dblp.org/rec/conf/cp/KorovinTV09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fase/KovacsV09,
author = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Marsha Chechik and
Martin Wirsing},
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},
series = {Lecture Notes in Computer Science},
volume = {5503},
pages = {470--485},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-00593-0\_33},
doi = {10.1007/978-3-642-00593-0\_33},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fase/KovacsV09.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE}},
year = {2009},
url = {https://doi.org/10.1109/FMCAD.2009.5351132},
doi = {10.1109/FMCAD.2009.5351132},
timestamp = {Wed, 16 Oct 2019 14:14:56 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/KhasidashviliKV09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ki/HoderV09,
author = {Krystof Hoder and
Andrei Voronkov},
editor = {B{\"{a}}rbel Mertsching and
Marcus Hund and
Muhammad Zaheer Aziz},
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},
series = {Lecture Notes in Computer Science},
volume = {5803},
pages = {435--443},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-04617-9\_55},
doi = {10.1007/978-3-642-04617-9\_55},
timestamp = {Tue, 14 May 2019 10:00:49 +0200},
biburl = {https://dblp.org/rec/conf/ki/HoderV09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/VoronkovN09,
author = {Andrei Voronkov and
Iman Narasamdya},
editor = {Jens Palsberg and
Zhendong Su},
title = {Inter-program Properties},
booktitle = {Static Analysis, 16th International Symposium, {SAS} 2009, Los Angeles,
CA, USA, August 9-11, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5673},
pages = {343--359},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-03237-0\_23},
doi = {10.1007/978-3-642-03237-0\_23},
timestamp = {Thu, 02 Dec 2021 11:46:17 +0100},
biburl = {https://dblp.org/rec/conf/sas/VoronkovN09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/KovacsV09,
author = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
editor = {Stephen M. Watt and
Viorel Negru and
Tetsuo Ida and
Tudor Jebelean and
Dana Petcu and
Daniela Zaharie},
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},
publisher = {{IEEE} Computer Society},
year = {2009},
url = {https://doi.org/10.1109/SYNASC.2009.66},
doi = {10.1109/SYNASC.2009.66},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/synasc/KovacsV09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/synasc/Voronkov09,
author = {Andrei Voronkov},
editor = {Stephen M. Watt and
Viorel Negru and
Tetsuo Ida and
Tudor Jebelean and
Dana Petcu and
Daniela Zaharie},
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},
publisher = {{IEEE} Computer Society},
year = {2009},
url = {https://doi.org/10.1109/SYNASC.2009.65},
doi = {10.1109/SYNASC.2009.65},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/synasc/Voronkov09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BjornerTV09,
author = {Nikolaj S. Bj{\o}rner and
Nikolai Tillmann and
Andrei Voronkov},
editor = {Stefan Kowalewski and
Anna Philippou},
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},
series = {Lecture Notes in Computer Science},
volume = {5505},
pages = {307--321},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-00768-2\_27},
doi = {10.1007/978-3-642-00768-2\_27},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BjornerTV09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/PerezV08,
author = {Juan Antonio Navarro P{\'{e}}rez and
Andrei Voronkov},
editor = {Alessandro Armando and
Peter Baumgartner and
Gilles Dowek},
title = {Proof Systems for Effectively Propositional Logic},
booktitle = {Automated Reasoning, 4th International Joint Conference, {IJCAR} 2008,
Sydney, Australia, August 12-15, 2008, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5195},
pages = {426--440},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-71070-7\_36},
doi = {10.1007/978-3-540-71070-7\_36},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/PerezV08.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2008.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/rta/2008.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/PerezV07,
author = {Juan Antonio Navarro P{\'{e}}rez and
Andrei Voronkov},
editor = {Frank Pfenning},
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},
series = {Lecture Notes in Computer Science},
volume = {4603},
pages = {346--361},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73595-3\_24},
doi = {10.1007/978-3-540-73595-3\_24},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/PerezV07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/KorovinV07,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Jacques Duparc and
Thomas A. Henzinger},
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},
series = {Lecture Notes in Computer Science},
volume = {4646},
pages = {223--237},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-74915-8\_19},
doi = {10.1007/978-3-540-74915-8\_19},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/KorovinV07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sat/PerezV07,
author = {Juan Antonio Navarro P{\'{e}}rez and
Andrei Voronkov},
editor = {Jo{\~{a}}o Marques{-}Silva and
Karem A. Sakallah},
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},
series = {Lecture Notes in Computer Science},
volume = {4501},
pages = {3},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-72788-0\_2},
doi = {10.1007/978-3-540-72788-0\_2},
timestamp = {Mon, 24 Feb 2020 19:23:27 +0100},
biburl = {https://dblp.org/rec/conf/sat/PerezV07.bib},
bibsource = {dblp computer science bibliography, https://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 = {Thu, 09 Nov 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/csr/2007.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/ershov/2006,
editor = {Irina B. 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 = {Mon, 16 Dec 2019 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ershov/2006.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2007.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/adbis/JaberV06,
author = {Mohammed K. Jaber and
Andrei Voronkov},
editor = {Yannis Manolopoulos and
Jaroslav Pokorn{\'{y}} and
Timos K. Sellis},
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},
series = {Lecture Notes in Computer Science},
volume = {4152},
pages = {155--170},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11827252\_14},
doi = {10.1007/11827252\_14},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/adbis/JaberV06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/foiks/HorrocksV06,
author = {Ian Horrocks and
Andrei Voronkov},
editor = {J{\"{u}}rgen Dix and
Stephen J. Hegner},
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},
series = {Lecture Notes in Computer Science},
volume = {3861},
pages = {201--218},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11663881\_12},
doi = {10.1007/11663881\_12},
timestamp = {Tue, 12 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/foiks/HorrocksV06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icde/JaberV06,
author = {Mohammed K. Jaber and
Andrei Voronkov},
editor = {Ling Liu and
Andreas Reuter and
Kyu{-}Young Whang and
Jianjun Zhang},
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},
publisher = {{IEEE} Computer Society},
year = {2006},
url = {https://doi.org/10.1109/ICDE.2006.164},
doi = {10.1109/ICDE.2006.164},
timestamp = {Thu, 23 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/icde/JaberV06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/jelia/Voronkov06,
author = {Andrei Voronkov},
editor = {Michael Fisher and
Wiebe van der Hoek and
Boris Konev and
Alexei Lisitsa},
title = {Inconsistencies in Ontologies},
booktitle = {Logics in Artificial Intelligence, 10th European Conference, {JELIA}
2006, Liverpool, UK, September 13-15, 2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4160},
pages = {19},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11853886\_3},
doi = {10.1007/11853886\_3},
timestamp = {Fri, 03 Jun 2022 08:18:13 +0200},
biburl = {https://dblp.org/rec/conf/jelia/Voronkov06.bib},
bibsource = {dblp computer science bibliography, https://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 = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/2005P5431.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2006.bib},
bibsource = {dblp computer science bibliography, https://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 = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/RiazanovV05.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://doi.org/10.1145/1055686.1055692},
doi = {10.1145/1055686.1055692},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tocl/KorovinV05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aaai/NavarroV05,
author = {Juan Antonio Navarro P{\'{e}}rez and
Andrei Voronkov},
editor = {Manuela M. Veloso and
Subbarao Kambhampati},
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},
publisher = {{AAAI} Press / The {MIT} Press},
year = {2005},
url = {http://www.aaai.org/Library/AAAI/2005/aaai05-069.php},
timestamp = {Tue, 05 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/aaai/NavarroV05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/ChubarovV05,
author = {Dimitri Chubarov and
Andrei Voronkov},
editor = {Dieter Hutter and
Werner Stephan},
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},
series = {Lecture Notes in Computer Science},
volume = {2605},
pages = {132--138},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/978-3-540-32254-2\_8},
doi = {10.1007/978-3-540-32254-2\_8},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/birthday/ChubarovV05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mfcs/ChubarovV05,
author = {Dimitri Chubarov and
Andrei Voronkov},
editor = {Joanna Jedrzejowicz and
Andrzej Szepietowski},
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},
series = {Lecture Notes in Computer Science},
volume = {3618},
pages = {260--270},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11549345\_23},
doi = {10.1007/11549345\_23},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/mfcs/ChubarovV05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mfcs/KorovinV05,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Joanna Jedrzejowicz and
Andrzej Szepietowski},
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},
series = {Lecture Notes in Computer Science},
volume = {3618},
pages = {591--602},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11549345\_51},
doi = {10.1007/11549345\_51},
timestamp = {Thu, 25 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mfcs/KorovinV05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sas/NarasamdyaV05,
author = {Iman Narasamdya and
Andrei Voronkov},
editor = {Chris Hankin and
Igor Siveroni},
title = {Finding Basic Block and Variable Correspondence},
booktitle = {Static Analysis, 12th International Symposium, {SAS} 2005, London,
UK, September 7-9, 2005, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3672},
pages = {251--267},
publisher = {Springer},
year = {2005},
url = {https://doi.org/10.1007/11547662\_18},
doi = {10.1007/11547662\_18},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/sas/NarasamdyaV05.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2004.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2005.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderBNV05,
author = {Franz Baader and
Peter Baumgartner and
Robert Nieuwenhuis and
Andrei Voronkov},
editor = {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},
series = {Dagstuhl Seminar Proceedings},
volume = {05431},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"{u}}r Informatik
(IBFI), Schloss Dagstuhl, Germany},
year = {2005},
url = {http://drops.dagstuhl.de/opus/volltexte/2006/510},
timestamp = {Sun, 02 Oct 2022 15:58:47 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/BaaderBNV05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dagstuhl/BaaderBNV05a,
author = {Franz Baader and
Peter Baumgartner and
Robert Nieuwenhuis and
Andrei Voronkov},
editor = {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},
series = {Dagstuhl Seminar Proceedings},
volume = {05431},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"{u}}r Informatik
(IBFI), Schloss Dagstuhl, Germany},
year = {2005},
url = {http://drops.dagstuhl.de/opus/volltexte/2006/562},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/BaaderBNV05a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV04,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {David A. Basin and
Micha{\"{e}}l Rusinowitch},
title = {Efficient Checking of Term Ordering Constraints},
booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR}
2004, Cork, Ireland, July 4-8, 2004, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3097},
pages = {60--74},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/978-3-540-25984-8\_3},
doi = {10.1007/978-3-540-25984-8\_3},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/RiazanovV04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/HustadtKRV04,
author = {Ullrich Hustadt and
Boris Konev and
Alexandre Riazanov and
Andrei Voronkov},
editor = {David A. Basin and
Micha{\"{e}}l Rusinowitch},
title = {TeMP: {A} Temporal Monodic Prover},
booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR}
2004, Cork, Ireland, July 4-8, 2004, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3097},
pages = {326--330},
publisher = {Springer},
year = {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 = {https://dblp.org/rec/conf/cade/HustadtKRV04.bib},
bibsource = {dblp computer science bibliography, https://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 = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/KorovinV03.bib},
bibsource = {dblp computer science bibliography, https://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. Reason.},
volume = {30},
number = {2},
pages = {121--151},
year = {2003},
url = {https://doi.org/10.1023/A:1023260415982},
doi = {10.1023/A:1023260415982},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Voronkov03.bib},
bibsource = {dblp computer science bibliography, https://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 = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsc/DegtyarevNV03.bib},
bibsource = {dblp computer science bibliography, https://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 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jsc/RiazanovV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/KorovinV03,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Franz Baader},
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},
series = {Lecture Notes in Computer Science},
volume = {2741},
pages = {47--59},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-45085-6\_5},
doi = {10.1007/978-3-540-45085-6\_5},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/KorovinV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV03,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Franz Baader},
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},
series = {Lecture Notes in Computer Science},
volume = {2741},
pages = {380--396},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-45085-6\_34},
doi = {10.1007/978-3-540-45085-6\_34},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/RiazanovV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/MaksimovaV03,
author = {Larisa Maksimova and
Andrei Voronkov},
editor = {Matthias Baaz and
Johann A. Makowsky},
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},
series = {Lecture Notes in Computer Science},
volume = {2803},
pages = {397--412},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-45220-1\_32},
doi = {10.1007/978-3-540-45220-1\_32},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/MaksimovaV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/RybinaV03,
author = {Tatiana Rybina and
Andrei Voronkov},
editor = {Matthias Baaz and
Johann A. Makowsky},
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},
series = {Lecture Notes in Computer Science},
volume = {2803},
pages = {546--573},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-45220-1\_46},
doi = {10.1007/978-3-540-45220-1\_46},
timestamp = {Wed, 24 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/csl/RybinaV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ershov/RybinaV03,
author = {Tatiana Rybina and
Andrei Voronkov},
editor = {Manfred Broy and
Alexandre V. Zamulin},
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},
series = {Lecture Notes in Computer Science},
volume = {2890},
pages = {222--237},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/978-3-540-39866-0\_24},
doi = {10.1007/978-3-540-39866-0\_24},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/ershov/RybinaV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icalp/RybinaV03,
author = {Tatiana Rybina and
Andrei Voronkov},
editor = {Jos C. M. Baeten and
Jan Karel Lenstra and
Joachim Parrow and
Gerhard J. Woeginger},
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},
series = {Lecture Notes in Computer Science},
volume = {2719},
pages = {714--724},
publisher = {Springer},
year = {2003},
url = {https://doi.org/10.1007/3-540-45061-0\_56},
doi = {10.1007/3-540-45061-0\_56},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/icalp/RybinaV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/Voronkov03,
author = {Andrei Voronkov},
editor = {Georg Gottlob and
Toby Walsh},
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},
publisher = {Morgan Kaufmann},
year = {2003},
url = {http://ijcai.org/Proceedings/03/Papers/284.pdf},
timestamp = {Tue, 20 Aug 2019 16:18:41 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/Voronkov03.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {2003},
url = {https://doi.org/10.1109/LICS.2003.1210047},
doi = {10.1109/LICS.2003.1210047},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/KorovinV03.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2003.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://dblp.org/rec/journals/aicom/RiazanovV02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/amast/RybinaV02,
author = {Tatiana Rybina and
Andrei Voronkov},
editor = {H{\'{e}}l{\`{e}}ne Kirchner and
Christophe Ringeissen},
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},
series = {Lecture Notes in Computer Science},
volume = {2422},
pages = {489--494},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-45719-4\_33},
doi = {10.1007/3-540-45719-4\_33},
timestamp = {Tue, 14 May 2019 10:00:38 +0200},
biburl = {https://dblp.org/rec/conf/amast/RybinaV02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/RybinaV02,
author = {Tatiana Rybina and
Andrei Voronkov},
editor = {Ed Brinksma and
Kim Guldstrand Larsen},
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},
series = {Lecture Notes in Computer Science},
volume = {2404},
pages = {386--400},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-45657-0\_32},
doi = {10.1007/3-540-45657-0\_32},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
biburl = {https://dblp.org/rec/conf/cav/RybinaV02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/dlog/Voronkov02,
author = {Andrei Voronkov},
editor = {Ian Horrocks and
Sergio Tessaris},
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},
series = {{CEUR} Workshop Proceedings},
volume = {53},
publisher = {CEUR-WS.org},
year = {2002},
url = {https://ceur-ws.org/Vol-53/voronkov.ps},
timestamp = {Fri, 10 Mar 2023 16:23:16 +0100},
biburl = {https://dblp.org/rec/conf/dlog/Voronkov02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fsttcs/KorovinV02,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Manindra Agrawal and
Anil Seth},
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},
series = {Lecture Notes in Computer Science},
volume = {2556},
pages = {230--240},
publisher = {Springer},
year = {2002},
url = {https://doi.org/10.1007/3-540-36206-1\_21},
doi = {10.1007/3-540-36206-1\_21},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/fsttcs/KorovinV02.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/2002.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2002.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://arxiv.org/abs/cs/0207068},
timestamp = {Fri, 10 Jan 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/cs-LO-0207068.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://doi.org/10.1145/502807.502810},
doi = {10.1145/502807.502810},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/csur/DantsinEGV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sLogica/FittingTV01,
author = {Melvin Fitting and
Lars Thalmann and
Andrei Voronkov},
title = {Term-Modal Logics},
journal = {Stud Logica},
volume = {69},
number = {1},
pages = {133--169},
year = {2001},
url = {https://doi.org/10.1023/A:1013842612702},
doi = {10.1023/A:1013842612702},
timestamp = {Tue, 01 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sLogica/FittingTV01.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://doi.org/10.1145/371316.371494},
doi = {10.1145/371316.371494},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tocl/RybinaV01.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://doi.org/10.1145/371316.371511},
doi = {10.1145/371316.371511},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tocl/Voronkov01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov01,
author = {Andrei Voronkov},
editor = {Rajeev Gor{\'{e}} and
Alexander Leitsch and
Tobias Nipkow},
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},
series = {Lecture Notes in Computer Science},
volume = {2083},
pages = {13--28},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-45744-5\_3},
doi = {10.1007/3-540-45744-5\_3},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Voronkov01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/NieuwenhuisHRV01,
author = {Robert Nieuwenhuis and
Thomas Hillenbrand and
Alexandre Riazanov and
Andrei Voronkov},
editor = {Rajeev Gor{\'{e}} and
Alexander Leitsch and
Tobias Nipkow},
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},
series = {Lecture Notes in Computer Science},
volume = {2083},
pages = {257--271},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-45744-5\_19},
doi = {10.1007/3-540-45744-5\_19},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/NieuwenhuisHRV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV01,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Rajeev Gor{\'{e}} and
Alexander Leitsch and
Tobias Nipkow},
title = {Vampire 1.1 (System Description)},
booktitle = {Automated Reasoning, First International Joint Conference, {IJCAR}
2001, Siena, Italy, June 18-23, 2001, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {2083},
pages = {376--380},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-45744-5\_29},
doi = {10.1007/3-540-45744-5\_29},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/RiazanovV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ershov/RiazanovV01,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Dines Bj{\o}rner and
Manfred Broy and
Alexandre V. Zamulin},
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},
series = {Lecture Notes in Computer Science},
volume = {2244},
pages = {95--108},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-45575-2\_11},
doi = {10.1007/3-540-45575-2\_11},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/ershov/RiazanovV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icalp/KorovinV01,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Fernando Orejas and
Paul G. Spirakis and
Jan van Leeuwen},
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},
series = {Lecture Notes in Computer Science},
volume = {2076},
pages = {979--992},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-48224-5\_79},
doi = {10.1007/3-540-48224-5\_79},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/icalp/KorovinV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/RiazanovV01,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Bernhard Nebel},
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},
publisher = {Morgan Kaufmann},
year = {2001},
timestamp = {Tue, 20 Aug 2019 16:18:14 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/RiazanovV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/KorovinV01,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Aart Middeldorp},
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},
series = {Lecture Notes in Computer Science},
volume = {2051},
pages = {137--153},
publisher = {Springer},
year = {2001},
url = {https://doi.org/10.1007/3-540-45127-7\_12},
doi = {10.1007/3-540-45127-7\_12},
timestamp = {Tue, 14 May 2019 10:00:46 +0200},
biburl = {https://dblp.org/rec/conf/rta/KorovinV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/el/RV01/DegtyarevV01,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {John Alan Robinson and
Andrei Voronkov},
title = {The Inverse Method},
booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
pages = {179--272},
publisher = {Elsevier and {MIT} Press},
year = {2001},
url = {https://doi.org/10.1016/b978-044450813-3/50006-0},
doi = {10.1016/B978-044450813-3/50006-0},
timestamp = {Thu, 25 Jul 2019 12:26:00 +0200},
biburl = {https://dblp.org/rec/books/el/RV01/DegtyarevV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/el/RV01/DegtyarevV01a,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {John Alan Robinson and
Andrei Voronkov},
title = {Equality Reasoning in Sequent-Based Calculi},
booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
pages = {611--706},
publisher = {Elsevier and {MIT} Press},
year = {2001},
url = {https://doi.org/10.1016/b978-044450813-3/50012-6},
doi = {10.1016/B978-044450813-3/50012-6},
timestamp = {Thu, 25 Jul 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/el/RV01/DegtyarevV01a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/el/RV01/RamakrishnanSV01,
author = {I. V. Ramakrishnan and
R. Sekar and
Andrei Voronkov},
editor = {John Alan Robinson and
Andrei Voronkov},
title = {Term Indexing},
booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
pages = {1853--1964},
publisher = {Elsevier and {MIT} Press},
year = {2001},
url = {https://doi.org/10.1016/b978-044450813-3/50028-x},
doi = {10.1016/B978-044450813-3/50028-X},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/books/el/RV01/RamakrishnanSV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/el/RV01/RobinsonV01,
author = {John Alan Robinson and
Andrei Voronkov},
editor = {John Alan Robinson and
Andrei Voronkov},
title = {Preface},
booktitle = {Handbook of Automated Reasoning (in 2 volumes)},
pages = {v--vii},
publisher = {Elsevier and {MIT} Press},
year = {2001},
url = {https://doi.org/10.1016/B978-044450813-3/50000-X},
doi = {10.1016/B978-044450813-3/50000-X},
timestamp = {Thu, 25 Jul 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/el/RV01/RobinsonV01.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:books/ws/phaunRS01/DegtyarevGV01,
author = {Anatoli Degtyarev and
Yuri Gurevich and
Andrei Voronkov},
editor = {Gheorghe Paun and
Grzegorz Rozenberg and
Arto Salomaa},
title = {Herbrand's Theorem and Equational Reasoning: Problems and Solutions},
booktitle = {Current Trends in Theoretical Computer Science, Entering the 21th
Century},
pages = {303--326},
publisher = {World Scientific},
year = {2001},
timestamp = {Sat, 03 Aug 2019 22:52:51 +0200},
biburl = {https://dblp.org/rec/books/ws/phaunRS01/DegtyarevGV01.bib},
bibsource = {dblp computer science bibliography, https://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},
url = {https://www.sciencedirect.com/book/9780444508133/handbook-of-automated-reasoning},
isbn = {0-444-50813-9},
timestamp = {Thu, 25 Jul 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/el/RobinsonV01.bib},
bibsource = {dblp computer science bibliography, https://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 = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2001.bib},
bibsource = {dblp computer science bibliography, https://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 = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/DegtyarevGNVV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arw/KorovinV00,
author = {Konstantin Korovin and
Andrei Voronkov},
editor = {Hans J{\"{u}}rgen Ohlbach and
Ulrich Endriss and
Odinaldo Rodrigues and
Stefan Schlobach},
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},
series = {{CEUR} Workshop Proceedings},
volume = {32},
publisher = {CEUR-WS.org},
year = {2000},
url = {https://ceur-ws.org/Vol-32/korovin.ps.gz},
timestamp = {Fri, 10 Mar 2023 16:22:28 +0100},
biburl = {https://dblp.org/rec/conf/arw/KorovinV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arw/RiazanovV00,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Hans J{\"{u}}rgen Ohlbach and
Ulrich Endriss and
Odinaldo Rodrigues and
Stefan Schlobach},
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},
series = {{CEUR} Workshop Proceedings},
volume = {32},
publisher = {CEUR-WS.org},
year = {2000},
url = {https://ceur-ws.org/Vol-32/riazanov.ps.gz},
timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arw/RiazanovV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arw/RybinaV00,
author = {Tatiana Rybina and
Andrei Voronkov},
editor = {Hans J{\"{u}}rgen Ohlbach and
Ulrich Endriss and
Odinaldo Rodrigues and
Stefan Schlobach},
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},
series = {{CEUR} Workshop Proceedings},
volume = {32},
publisher = {CEUR-WS.org},
year = {2000},
url = {https://ceur-ws.org/Vol-32/rybina.ps.gz},
timestamp = {Fri, 10 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/arw/RybinaV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/DegtyarevV00,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {David A. McAllester},
title = {Stratified Resolution},
booktitle = {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},
pages = {365--384},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/10721959\_28},
doi = {10.1007/10721959\_28},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/DegtyarevV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/jelia/RiazanovV00,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Manuel Ojeda{-}Aciego and
Inman P. de Guzm{\'{a}}n and
Gerhard Brewka and
Lu{\'{\i}}s Moniz Pereira},
title = {Partially Adaptive Code Trees},
booktitle = {Logics in Artificial Intelligence, European Workshop, {JELIA} 2000
Malaga, Spain, September 29 - October 2, 2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1919},
pages = {209--223},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/3-540-40006-0\_15},
doi = {10.1007/3-540-40006-0\_15},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/jelia/RiazanovV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/kr/Voronkov00,
author = {Andrei Voronkov},
editor = {Anthony G. Cohn and
Fausto Giunchiglia and
Bart Selman},
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},
publisher = {Morgan Kaufmann},
year = {2000},
timestamp = {Tue, 20 Jun 2023 09:03:42 +0200},
biburl = {https://dblp.org/rec/conf/kr/Voronkov00.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {2000},
url = {https://doi.org/10.1109/LICS.2000.855776},
doi = {10.1109/LICS.2000.855776},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/RybinaV00.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {2000},
url = {https://doi.org/10.1109/LICS.2000.855777},
doi = {10.1109/LICS.2000.855777},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/KorovinV00.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {2000},
url = {https://doi.org/10.1109/LICS.2000.855787},
doi = {10.1109/LICS.2000.855787},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/Voronkov00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pods/DantsinV00,
author = {Evgeny Dantsin and
Andrei Voronkov},
editor = {Victor Vianu and
Georg Gottlob},
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},
publisher = {{ACM}},
year = {2000},
url = {https://doi.org/10.1145/335168.335218},
doi = {10.1145/335168.335218},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/pods/DantsinV00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/FittingTV00,
author = {Melvin Fitting and
Lars Thalmann and
Andrei Voronkov},
editor = {Roy Dyckhoff},
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},
series = {Lecture Notes in Computer Science},
volume = {1847},
pages = {220--236},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/10722086\_19},
doi = {10.1007/10722086\_19},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/tableaux/FittingTV00.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/2000.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://dblp.org/rec/journals/jsyml/Voronkov99.bib},
bibsource = {dblp computer science bibliography, https://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 = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/GurevichV99.bib},
bibsource = {dblp computer science bibliography, https://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 = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/Voronkov99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/RiazanovV99,
author = {Alexandre Riazanov and
Andrei Voronkov},
editor = {Harald Ganzinger},
title = {Vampire},
booktitle = {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},
pages = {292--296},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48660-7\_26},
doi = {10.1007/3-540-48660-7\_26},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/RiazanovV99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov99,
author = {Andrei Voronkov},
editor = {Harald Ganzinger},
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},
series = {Lecture Notes in Computer Science},
volume = {1632},
pages = {383--387},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48660-7\_35},
doi = {10.1007/3-540-48660-7\_35},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/Voronkov99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/DantsinV99,
author = {Evgeny Dantsin and
Andrei Voronkov},
editor = {Wolfgang Thomas},
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},
series = {Lecture Notes in Computer Science},
volume = {1578},
pages = {180--196},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-49019-1\_13},
doi = {10.1007/3-540-49019-1\_13},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fossacs/DantsinV99.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/1999.bib},
bibsource = {dblp computer science bibliography, https://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. Reason.},
volume = {20},
number = {1},
pages = {47--80},
year = {1998},
url = {https://doi.org/10.1023/A:1005996623714},
doi = {10.1023/A:1005996623714},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/DegtyarevV98.bib},
bibsource = {dblp computer science bibliography, https://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. Reason.},
volume = {21},
number = {2},
pages = {205--231},
year = {1998},
url = {https://doi.org/10.1023/A:1005934721802},
doi = {10.1023/A:1005934721802},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Voronkov98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BachmairGV98,
author = {Leo Bachmair and
Harald Ganzinger and
Andrei Voronkov},
editor = {Claude Kirchner and
H{\'{e}}l{\`{e}}ne Kirchner},
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},
series = {Lecture Notes in Computer Science},
volume = {1421},
pages = {175--190},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/BFb0054259},
doi = {10.1007/BFB0054259},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/BachmairGV98.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {1998},
url = {https://doi.org/10.1109/LICS.1998.705662},
doi = {10.1109/LICS.1998.705662},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/Voronkov98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pods/VorobyovV98,
author = {Sergei G. Vorobyov and
Andrei Voronkov},
editor = {Alberto O. Mendelzon and
Jan Paredaens},
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},
publisher = {{ACM} Press},
year = {1998},
url = {https://doi.org/10.1145/275487.275515},
doi = {10.1145/275487.275515},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/pods/VorobyovV98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/DegtyarevGNVV98,
author = {Anatoli Degtyarev and
Yuri Gurevich and
Paliath Narendran and
Margus Veanes and
Andrei Voronkov},
editor = {Tobias Nipkow},
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},
series = {Lecture Notes in Computer Science},
volume = {1379},
pages = {181--195},
publisher = {Springer},
year = {1998},
url = {https://doi.org/10.1007/BFb0052370},
doi = {10.1007/BFB0052370},
timestamp = {Sat, 05 Sep 2020 18:07:52 +0200},
biburl = {https://dblp.org/rec/conf/rta/DegtyarevGNVV98.bib},
bibsource = {dblp computer science bibliography, https://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, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/dagstuhl/1998change.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {1997},
url = {https://doi.org/10.1109/CCC.1997.612304},
doi = {10.1109/CCC.1997.612304},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/coco/DantsinEGV97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icalp/GurevichV97,
author = {Yuri Gurevich and
Andrei Voronkov},
editor = {Pierpaolo Degano and
Roberto Gorrieri and
Alberto Marchetti{-}Spaccamela},
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},
series = {Lecture Notes in Computer Science},
volume = {1256},
pages = {154--165},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-63165-8\_173},
doi = {10.1007/3-540-63165-8\_173},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/icalp/GurevichV97.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {Morgan Kaufmann},
year = {1997},
url = {http://ijcai.org/Proceedings/97-1/Papers/019.pdf},
timestamp = {Tue, 20 Aug 2019 16:17:27 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/Voronkov97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lfcs/DantsinV97,
author = {Evgeny Dantsin and
Andrei Voronkov},
editor = {Sergei I. Adian and
Anil Nerode},
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},
series = {Lecture Notes in Computer Science},
volume = {1234},
pages = {56--66},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-63045-7\_7},
doi = {10.1007/3-540-63045-7\_7},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lfcs/DantsinV97.bib},
bibsource = {dblp computer science bibliography, https://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 = {Bull. {EATCS}},
volume = {60},
pages = {78--96},
year = {1996},
timestamp = {Thu, 18 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/eatcs/DegtyarevGV96.bib},
bibsource = {dblp computer science bibliography, https://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 = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jlp/DegtyarevV96.bib},
bibsource = {dblp computer science bibliography, https://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 = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/DegtyarevV96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov96,
author = {Andrei Voronkov},
editor = {Michael A. McRobbie and
John K. Slaney},
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},
series = {Lecture Notes in Computer Science},
volume = {1104},
pages = {32--46},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61511-3\_67},
doi = {10.1007/3-540-61511-3\_67},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Voronkov96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/disco/DegtyarevV96,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {Jacques Calmet and
Carla Limongelli},
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},
series = {Lecture Notes in Computer Science},
volume = {1128},
pages = {46--60},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61697-7\_4},
doi = {10.1007/3-540-61697-7\_4},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/disco/DegtyarevV96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/elp/ArgeniusV96,
author = {Martin Argenius and
Andrei Voronkov},
editor = {Roy Dyckhoff and
Heinrich Herre and
Peter Schroeder{-}Heister},
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},
series = {Lecture Notes in Computer Science},
volume = {1050},
pages = {1--18},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-60983-0\_1},
doi = {10.1007/3-540-60983-0\_1},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/elp/ArgeniusV96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/elp/DegtyarevV96,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {Roy Dyckhoff and
Heinrich Herre and
Peter Schroeder{-}Heister},
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},
series = {Lecture Notes in Computer Science},
volume = {1050},
pages = {119--136},
publisher = {Springer},
year = {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 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/elp/DegtyarevV96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ershov/Voronkov96,
author = {Andrei Voronkov},
editor = {Dines Bj{\o}rner and
Manfred Broy and
Igor V. Pottosin},
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},
series = {Lecture Notes in Computer Science},
volume = {1181},
pages = {409--419},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-62064-8\_34},
doi = {10.1007/3-540-62064-8\_34},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/ershov/Voronkov96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/jelia/DegtyarevV96,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {Jos{\'{e}} J{\'{u}}lio Alferes and
Lu{\'{\i}}s Moniz Pereira and
Ewa Orlowska},
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},
series = {Lecture Notes in Computer Science},
volume = {1126},
pages = {50--69},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61630-6\_4},
doi = {10.1007/3-540-61630-6\_4},
timestamp = {Sat, 19 Oct 2019 20:16:50 +0200},
biburl = {https://dblp.org/rec/conf/jelia/DegtyarevV96.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {1996},
url = {https://doi.org/10.1109/LICS.1996.561466},
doi = {10.1109/LICS.1996.561466},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/DegtyarevMV96.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {{IEEE} Computer Society},
year = {1996},
url = {https://doi.org/10.1109/LICS.1996.561467},
doi = {10.1109/LICS.1996.561467},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/DegtyarevV96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/Voronkov96,
author = {Andrei Voronkov},
editor = {Pierangelo Miglioli and
Ugo Moscato and
Daniele Mundici and
Mario Ornaghi},
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},
series = {Lecture Notes in Computer Science},
volume = {1071},
pages = {312--329},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61208-4\_20},
doi = {10.1007/3-540-61208-4\_20},
timestamp = {Tue, 14 May 2019 10:00:54 +0200},
biburl = {https://dblp.org/rec/conf/tableaux/Voronkov96.bib},
bibsource = {dblp computer science bibliography, https://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 = {https://dblp.org/rec/journals/amai/Voronkov95.bib},
bibsource = {dblp computer science bibliography, https://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. Reason.},
volume = {15},
number = {2},
pages = {237--265},
year = {1995},
url = {https://doi.org/10.1007/BF00881918},
doi = {10.1007/BF00881918},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Voronkov95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/DegtyarevV95,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {Hans Kleine B{\"{u}}ning},
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},
series = {Lecture Notes in Computer Science},
volume = {1092},
pages = {178--190},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-61377-3\_38},
doi = {10.1007/3-540-61377-3\_38},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/DegtyarevV95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iclp/DegtyarevV95,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {Leon Sterling},
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},
publisher = {{MIT} Press},
year = {1995},
timestamp = {Mon, 02 Dec 2013 17:40:44 +0100},
biburl = {https://dblp.org/rec/conf/iclp/DegtyarevV95.bib},
bibsource = {dblp computer science bibliography, https://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},
publisher = {Morgan Kaufmann},
year = {1995},
url = {http://ijcai.org/Proceedings/95-1/Papers/045.pdf},
timestamp = {Tue, 20 Aug 2019 16:17:30 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/DegtyarevV95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/wocfai/DegtyarevV95,
author = {Anatoli Degtyarev and
Andrei Voronkov},
editor = {Michel De Glas and
Zdzislaw Pawlak},
title = {General Connections via Equality Elimination},
booktitle = {Proceedings of the Second World Conference on the Fundamentals of
Artificial Intelligence, {WOCFAI} 1995, 3-7 July 1995, Paris, France},
pages = {109--120},
publisher = {Angkor, 6, rue Ma{\^{\i}}tre-Albert, 75005 Paris, France},
year = {1995},
timestamp = {Tue, 30 Jul 2019 08:58:42 +0200},
biburl = {https://dblp.org/rec/conf/wocfai/DegtyarevV95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/plilp/Voronkov94,
author = {Andrei Voronkov},
editor = {Manuel V. Hermenegildo and
Jaan Penjam},
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},
series = {Lecture Notes in Computer Science},
volume = {844},
pages = {147--164},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-58402-1\_12},
doi = {10.1007/3-540-58402-1\_12},
timestamp = {Tue, 14 May 2019 10:00:35 +0200},
biburl = {https://dblp.org/rec/conf/plilp/Voronkov94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/kgc/SazonovV93,
author = {Vladimir Yu. Sazonov and
Andrei Voronkov},
editor = {Georg Gottlob and
Alexander Leitsch and
Daniele Mundici},
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},
series = {Lecture Notes in Computer Science},
volume = {713},
pages = {301--312},
publisher = {Springer},
year = {1993},
url = {https://doi.org/10.1007/BFb0022578},
doi = {10.1007/BFB0022578},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/kgc/SazonovV93.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/1993.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov92,
author = {Andrei Voronkov},
editor = {Deepak Kapur},
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},
series = {Lecture Notes in Computer Science},
volume = {607},
pages = {648--662},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-55602-8\_198},
doi = {10.1007/3-540-55602-8\_198},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Voronkov92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/iclp/Voronkov92,
author = {Andrei Voronkov},
editor = {Howard A. Blair and
V. Wiktor Marek and
Anil Nerode and
Jeffrey B. Remmel},
title = {On Computability by Logic Programs},
booktitle = {Informal Proceedings of the Workshop Structural Complexity and Recursion-theoretic
methods in Logic-Programming, Washington, DC, USA, November 13, 1992},
pages = {165},
publisher = {Mathematical Sciences Institute, Cornell University},
year = {1992},
timestamp = {Thu, 21 Jun 2018 07:36:34 +0200},
biburl = {https://dblp.org/rec/conf/iclp/Voronkov92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/istcs/Voronkov92,
author = {Andrei Voronkov},
editor = {Danny Dolev and
Zvi Galil and
Michael Rodeh},
title = {Higher Order Functions in First Order Theory},
booktitle = {Theory of Computing and Systems, ISTCS'92, Israel Symposium, Haifa,
Israel, May 1992},
series = {Lecture Notes in Computer Science},
volume = {601},
pages = {43--54},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/BFb0035165},
doi = {10.1007/BFB0035165},
timestamp = {Tue, 14 May 2019 10:00:46 +0200},
biburl = {https://dblp.org/rec/conf/istcs/Voronkov92.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/1991.bib},
bibsource = {dblp computer science bibliography, https://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 = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/1992.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/Voronkov91,
author = {Andrei Voronkov},
editor = {Egon B{\"{o}}rger and
Gerhard J{\"{a}}ger and
Hans Kleine B{\"{u}}ning and
Michael M. Richter},
title = {On Completeness of Program Synthesis Systems},
booktitle = {Computer Science Logic, 5th Workshop, {CSL} '91, Berne, Switzerland,
October 7-11, 1991, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {626},
pages = {411--418},
publisher = {Springer},
year = {1991},
url = {https://doi.org/10.1007/BFb0023785},
doi = {10.1007/BFB0023785},
timestamp = {Fri, 17 Jul 2020 16:12:45 +0200},
biburl = {https://dblp.org/rec/conf/csl/Voronkov91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/Voronkov91,
author = {Andrei Voronkov},
editor = {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},
series = {Lecture Notes in Computer Science},
volume = {592},
pages = {486--514},
publisher = {Springer},
year = {1991},
url = {https://doi.org/10.1007/3-540-55460-2\_37},
doi = {10.1007/3-540-55460-2\_37},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/Voronkov91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/pdk/BoleyMMRV91,
author = {Harold Boley and
Micha Meier and
Chris Moss and
Michael M. Richter and
Andrei Voronkov},
editor = {Harold Boley and
Michael M. Richter},
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},
series = {Lecture Notes in Computer Science},
volume = {567},
pages = {383--398},
publisher = {Springer},
year = {1991},
url = {https://doi.org/10.1007/BFb0013545},
doi = {10.1007/BFB0013545},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/pdk/BoleyMMRV91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Voronkov90,
author = {Andrei Voronkov},
editor = {Mark E. Stickel},
title = {{LISS} - The Logic Inference Search System},
booktitle = {10th International Conference on Automated Deduction, Kaiserslautern,
FRG, July 24-27, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {449},
pages = {677--678},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-52885-7\_138},
doi = {10.1007/3-540-52885-7\_138},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Voronkov90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/Voronkov90,
author = {Andrei Voronkov},
editor = {Neil D. Jones},
title = {Towards the Theory of Programming in Constructive Logic},
booktitle = {ESOP'90, 3rd European Symposium on Programming, Copenhagen, Denmark,
May 15-18, 1990, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {432},
pages = {421--435},
publisher = {Springer},
year = {1990},
url = {https://doi.org/10.1007/3-540-52592-0\_78},
doi = {10.1007/3-540-52592-0\_78},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/esop/Voronkov90.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/colog/StarchenkoV88,
author = {Sergei Starchenko and
Andrei Voronkov},
editor = {Per Martin{-}L{\"{o}}f and
Grigori Mints},
title = {On connections between classical and constructive semantics},
booktitle = {COLOG-88, International Conference on Computer Logic, Tallinn, USSR,
December 1988, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {417},
pages = {275--285},
publisher = {Springer},
year = {1988},
url = {https://doi.org/10.1007/3-540-52335-9\_59},
doi = {10.1007/3-540-52335-9\_59},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/colog/StarchenkoV88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/colog/Voronkov88,
author = {Andrei Voronkov},
editor = {Per Martin{-}L{\"{o}}f and
Grigori Mints},
title = {A proof-search method for the first-order logic},
booktitle = {COLOG-88, International Conference on Computer Logic, Tallinn, USSR,
December 1988, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {417},
pages = {327--338},
publisher = {Springer},
year = {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 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/colog/Voronkov88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fct/Voronkov87,
author = {Andrei Voronkov},
editor = {Lothar Budach and
Rais Gatic Bakharajev and
Oleg Borisovic Lipanov},
title = {Deductive Program Synthesis and Markov's Principle},
booktitle = {Fundamentals of Computation Theory, International Conference FCT'87,
Kazan, USSR, June 22-26, 1987, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {278},
pages = {479--482},
publisher = {Springer},
year = {1987},
url = {https://doi.org/10.1007/3-540-18740-5\_105},
doi = {10.1007/3-540-18740-5\_105},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/fct/Voronkov87.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-03-27 20:22 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
