Vampire 1.1 (System Description)

Alexandre Riazanov, Andrei Voronkov

    Research output: Chapter in Book/Conference proceedingConference contribution

    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. © Springer-Verlag Berlin Heidelberg 2001.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Pages376-380
    Number of pages4
    Volume2083
    ISBN (Print)3540422544, 9783540422549
    Publication statusPublished - 2001
    Event1st International Joint Conference on Automated Reasoning, IJCAR 2001 - Siena
    Duration: 1 Jul 2001 → …

    Publication series

    NameLecture Notes in Computer Science

    Conference

    Conference1st International Joint Conference on Automated Reasoning, IJCAR 2001
    CitySiena
    Period1/07/01 → …

    Fingerprint

    Dive into the research topics of 'Vampire 1.1 (System Description)'. Together they form a unique fingerprint.

    Cite this