Affordable Access

Efficient instance retrieval with standard and relational path indexing

Authors
Publication Date
Disciplines
  • Mathematics

Abstract

doi:10.1016/j.ic.2004.10.012 Information and Computation 199 (2005) 228–252 www.elsevier.com/locate/ic Efficient instance retrieval with standard and relational path indexing� Alexandre Riazanov, Andrei Voronkov ∗ Department of Computer Science, University of Manchester, UK Received 1 December 2003; revised 2 September 2004 Available online 25 May 2005 Abstract Backward demodulation is a simplification technique used in saturation-based theorem proving with su- perposition 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. Keywords: Backward demodulation; Instance retrieval; Path indexing 1. Introduction Effectiveness of saturation-based theorem proving in first-order logic with equality strongly de- pends on the use of various redundancy detection and simplification techniques. In provers imple- menting the superposition or ordered paramodulation calculi (see, e.g. [9]) the most widely used simplification technique is probably demodulation, also known as term rewriting. If we have derived � This work was partially supported by grants from EPSRC. ∗ Corresponding author. Fax: +44 161 2756236. E-mail addresses: [email protected] (A. Riazanov), [email protected] (A. Voronkov). 0890-5401/$ - see front matter © 2005 Elsevier Inc. All rights reserved. doi:10.1016/j.ic.2004.10.012 A. Riazanov, A. Voronkov / Information and Computation 199 (2005) 228–252 229 a unit equality s

There are no comments yet on this publication. Be the first to share your thoughts.