The anatomy of vampire - Implementing bottom-up procedures with code trees

Andrei Voronkov

    Research output: Contribution to journalArticlepeer-review


    We present an implementation technique for a class of bottom-up logic procedures. The technique is based on code trees. It is intended to speed up most important and costly operations, such as subsumption and resolution. As an example, we consider the forward subsumption problem which is the bottleneck of many systems implementing first-order logic. To efficiently implement subsumption, we specialize subsumption algorithms at run time, using the abstract subsumption machine. The abstract subsumption machine makes subsumption-check using sequences of instructions that are similar to the WAM instructions. It gives an efficient implementation of the "clause at a time" subsumption problem. To implement subsumption on the "set at a time" basis, we combine sequences of instructions in code trees. We show that this technique yields a new way of indexing clauses. Some experimental results are given. The code trees technique may be used in various procedures, including binary resolution, hyper-resolution, UR-resolution, the inverse method, paramodulation and rewriting, OLDT-resolution, SLD-AL-resolution, bottom-up evaluation of logic programs, and disjunctive logic programs. © 1995 Kluwer Academic Publishers.
    Original languageEnglish
    Pages (from-to)237-265
    Number of pages28
    JournalJournal of Automated Reasoning
    Issue number2
    Publication statusPublished - Jun 1995


    • bottom-up algorithms
    • indexing
    • otters
    • subsumption
    • vampires


    Dive into the research topics of 'The anatomy of vampire - Implementing bottom-up procedures with code trees'. Together they form a unique fingerprint.

    Cite this