Efficient instance retrieval with standard and relational path indexing

Alexandre Riazanov, Andrei Voronkov

    Research output: Contribution to journalArticlepeer-review


    Backward demodulation is a simplification technique used in saturation-based theorem proving with superposition and ordered paramodulation. It requires instance retrieval, i.e., search for instances of some term in a typically large set of terms. Path indexing is a family of indexing techniques that can be used to solve this problem efficiently. We propose a number of powerful optimisations to standard path indexing. We also describe a novel framework that combines path indexing with relational joins. The main advantage of the proposed scheme is flexibility, which we illustrate by sketching how to adapt the scheme to instance retrieval modulo commutativity and backward subsumption on multi-literal clauses. © 2005 Elsevier Inc. All rights reserved.
    Original languageEnglish
    Pages (from-to)228-252
    Number of pages24
    JournalInformation and Computation
    Issue number1-2
    Publication statusPublished - 25 May 2005


    • Backward demodulation
    • Instance retrieval
    • Path indexing


    Dive into the research topics of 'Efficient instance retrieval with standard and relational path indexing'. Together they form a unique fingerprint.

    Cite this