Abstract
In this abstract we describe version 1.1 of the theorem prover Vampire. We give a general description and comment on Vampire’s original features and differences with the previously described version 0.0.
From the very beginning, the main research principle of Vampire was efficiency. Vampire uses a large number of data structures for indexing terms and clauses. Efficiency is still the most distinctive feature of Vampire. Due to reimplementation of some algorithms and data structures, Vampire 1.1 is on the average considerably more efficient than Vampire 0.0.
However, the last year many efforts were invested in flexibility: several new inference and simplification rules were implemented, options for controlling the proof search process added, and new literal selection schemes designed.
For the remaining time before IJCAR 2001, we are going to concentrate on adding more flexibility to Vampire, both for experienced and inexperienced users.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT: a system for distributed quational deduction. In J. Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), volume 914 of Lecture Notes in Computer Science, pages 397–402, Kaiserslautern, 1995.
F. Baader and T. Nipkow. Term Rewriting and and All That. Cambridge University press, Cambridge, 1998.
L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science and MIT Press, 2001. To appear.
A. Degtyarev and A. Voronkov. Stratified resolution. In D. McAllester, editor, 17th International Conference on Automated Deduction (CADE-17), volume 1831 of Lecture Notes in Artificial Intelligence, pages 365–384, Pittsburgh, 2000. Springer Verlag.
Th. Hillenbrand, A. Buch, R. Vogt, and B. Löchner. Waldmeister: High-performance equational deduction. Journal of Automated Reasoning, 18(2): 265–270, 1997.
W.W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94/6, Argonne National Laboratory, January 1994.
W. Pugh. Skip lists: A probabilistic alternative to balanced trees. Communications of the ACM, 33(6):668–676, 1990.
A. Riazanov and A. Voronkov. Limited resource strategy in resolution theorem proving. Preprint CSPP-7, Department of Computer Science, University of Manchester, October 2000.
A. Riazanov and A. Voronkov. Implementing backward subsumption and search for instances with path indexing and joins. 2001. To appear.
A. Riazanov and A. Voronkov. Splitting without backtracking. Preprint CSPP-10, Department of Computer Science, University of Manchester, January 2001. Accepted to IJCAI 2001.
S. Schulz. System abstract: E 0.3. In H. Ganzinger, editor, Automated Deduction— CADE-16. 16th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 297–301, Trento, Italy, July 1999.
M. Stickel. The path indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1989.
C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topic. System description: Spass version 1.0.0. In H. Ganzinger, editor, Automated Deduction—CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 378–382, Trento, Italy, July 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Riazanov, A., Voronkov, A. (2001). Vampire 1.1. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_29
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive