@article{riazanov2002,
	title = {The design and implementation of VAMPIRE.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {AI Commun.},
	number = {2-3},
	pages = {91-110},
	url = {http://dblp.uni-trier.de/db/journals/aicom/aicom15.html#RiazanovV02},
	volume = {15},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/27383ce7fb56c880f52243294ad01421d/daks},
	description = {dblp},
	ee = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0921-7126&volume=15&issue=2&spage=91}, date = {2003-11-27},
	keywords = {first-order reasoning }
}

@article{journals/corr/abs-0802-2127,
	title = {New Implementation Framework for Saturation-Based Reasoning},
	author = {Alexandre Riazanov},
	journal = {CoRR},
	note = {informal publication},
	url = {http://dblp.uni-trier.de/db/journals/corr/corr0802.html#abs-0802-2127},
	volume = {abs/0802.2127},
	year = {2008},
	biburl = {http://www.bibsonomy.org/bibtex/29c58163ac0eb6919981c19bf924c9f5b/dblp},
	description = {dblp},
	ee = {http://arxiv.org/abs/0802.2127}, date = {2008-03-03},
	keywords = {dblp }
}

@article{riazanov2002,
	title = {The design and implementation of VAMPIRE.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {AI Commun.},
	number = {2-3},
	pages = {91-110},
	url = {http://dblp.uni-trier.de/db/journals/aicom/aicom15.html#RiazanovV02},
	volume = {15},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/27383ce7fb56c880f52243294ad01421d/thau},
	description = {dblp},
	ee = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0921-7126&volume=15&issue=2&spage=91}, date = {2003-11-27},
	keywords = {first-order reasoning }
}

@article{journals/iandc/RiazanovV05,
	title = {Efficient instance retrieval with standard and relational path indexing.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {Inf. Comput.},
	number = {1-2},
	pages = {228-252},
	url = {http://dblp.uni-trier.de/db/journals/iandc/iandc199.html#RiazanovV05},
	volume = {199},
	year = {2005},
	biburl = {http://www.bibsonomy.org/bibtex/2cbb4c451cab8eeb28118584fd1da1a03/dblp},
	description = {dblp},
	ee = {http://dx.doi.org/10.1016/j.ic.2004.10.012}, date = {2006-02-22},
	keywords = {dblp }
}

@inproceedings{conf/semweb/TsarkovRBH04,
	title = {Using Vampire to Reason with OWL.},
	author = {Dmitry Tsarkov and Alexandre Riazanov and Sean Bechhofer and Ian Horrocks},
	booktitle = {International Semantic Web Conference},
	crossref = {conf/semweb/2004},
	editor = {Sheila A. McIlraith and Dimitris Plexousakis and Frank van Harmelen},
	pages = {471-485},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/semweb/iswc2004.html#TsarkovRBH04},
	volume = {3298},
	year = {2004},
	biburl = {http://www.bibsonomy.org/bibtex/2b7e8bcc624d2b498c32927d06699fd72/dblp},
	description = {dblp},
	ee = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3298&spage=471}, isbn = {3-540-23798-4}, date = {2004-11-10},
	keywords = {dblp }
}

@inproceedings{conf/cade/RiazanovV04,
	title = {Efficient Checking of Term Ordering Constraints.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	booktitle = {IJCAR},
	crossref = {conf/cade/2004},
	editor = {David A. Basin and Michaël Rusinowitch},
	pages = {60-74},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/cade/ijcar2004.html#RiazanovV04},
	volume = {3097},
	year = {2004},
	biburl = {http://www.bibsonomy.org/bibtex/232e05e67ac92a2e6fc10ba82901499f0/dblp},
	description = {dblp},
	ee = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3097&spage=60}, isbn = {3-540-22345-2}, date = {2004-06-09},
	keywords = {dblp }
}

@inproceedings{conf/cade/HustadtKRV04,
	title = {TeMP: A Temporal Monodic Prover.},
	author = {Ullrich Hustadt and Boris Konev and Alexandre Riazanov and Andrei Voronkov},
	booktitle = {IJCAR},
	crossref = {conf/cade/2004},
	editor = {David A. Basin and Michaël Rusinowitch},
	pages = {326-330},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/cade/ijcar2004.html#HustadtKRV04},
	volume = {3097},
	year = {2004},
	biburl = {http://www.bibsonomy.org/bibtex/203eb3d45574df23d4504e50226fcf5cc/dblp},
	description = {dblp},
	ee = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3097&spage=326}, isbn = {3-540-22345-2}, date = {2004-06-09},
	keywords = {dblp }
}

@inproceedings{conf/cade/RiazanovV03,
	title = {Efficient Instance Retrieval with Standard and Relational Path Indexing.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	booktitle = {CADE},
	crossref = {conf/cade/2003},
	editor = {Franz Baader},
	pages = {380-396},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/cade/cade2003.html#RiazanovV03},
	volume = {2741},
	year = {2003},
	biburl = {http://www.bibsonomy.org/bibtex/287a609fdee76a527a9ac56bcc048cf0c/dblp},
	description = {dblp},
	ee = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2741&spage=380}, isbn = {3-540-40559-3}, date = {2003-12-19},
	keywords = {dblp }
}

@article{journals/aicom/RiazanovV02,
	title = {The design and implementation of VAMPIRE.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {AI Commun.},
	number = {2-3},
	pages = {91-110},
	url = {http://dblp.uni-trier.de/db/journals/aicom/aicom15.html#RiazanovV02},
	volume = {15},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/27383ce7fb56c880f52243294ad01421d/dblp},
	description = {dblp},
	ee = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0921-7126&volume=15&issue=2&spage=91}, date = {2003-11-27},
	keywords = {dblp }
}

@article{journals/jsc/RiazanovV03,
	title = {Limited resource strategy in resolution theorem proving.},
	author = {Alexandre Riazanov and Andrei Voronkov},
	journal = {J. Symb. Comput.},
	number = {1-2},
	pages = {101-115},
	url = {http://dblp.uni-trier.de/db/journals/jsc/jsc36.html#RiazanovV03},
	volume = {36},
	year = {2003},
	biburl = {http://www.bibsonomy.org/bibtex/26a841a080de376c52a785fb2f3b2381f/dblp},
	description = {dblp},
	ee = {http://dx.doi.org/10.1016/S0747-7171(03)00040-3}, date = {2003-11-19},
	keywords = {dblp }
}