Abstract
Path indexing is a family of indexing techniques that can support instance retrieval, which is the core of any implementation of backward demodulation. We propose a number of powerful optimisations to standard path indexing. We also describe a novel flexible framework, called relational path indexing, that combines path indexing with relational joins. We illustrate the flexibility of relational path indexing by sketching how to adapt the scheme to instance retrieval modulo commutativity and backward subsumption on multi-literal clauses.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aho, A., Hopcroft, J., Ullmann, J.: The design and analysis of computer algorithms. Addison Wesley, Reading (1983)
Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Context trees. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 242–256. Springer, Heidelberg (2001)
Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117–131. Springer, Heidelberg (1995)
Graf, P. (ed.): Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1996)
Kapur, D., Narendran, P.: NP-completeness of the Set Unification and Matching Problems. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 489–495. Springer, Heidelberg (1986)
McCune, W.W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. Journal of Automated Reasoning 9(2), 147–167 (1992)
Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 257–271. Springer, Heidelberg (2001), see also the COMPIT homepage www.mpi-sb.mpg.de/~hillen/compit/
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 7, pp. 371–443. Elsevier Science, Amsterdam (2001)
Pugh, W.: Skip lists: A probabilistic alternative to balanced trees. Communications of the ACM 33(6), 668–676 (1990)
Ramesh, R., Ramakrishnan, I.V., Warren, D.S.: Automata-driven indexing of Prolog clauses. In: Seventh Annual ACM Symposium on Principles of Programming Languages, San Francisco, pp. 281–291 (1990)
Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)
Riazanov, A., Voronkov, A.: Efficient instance retrieval with standard and relational path indexing. Preprint CSPP-20, Department of Computer Science, University of Manchester (January 2003)
Sekar, R., Ramakrishnan, I.V., Voronkov, A.: Term indexing. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, ch. 26, pp. 1853–1964. Elsevier Science, Amsterdam (2001)
Stickel, M.: The path indexing method for indexing terms. Technical Report 473, Artificial Intelligence Center, SRI International, Menlo Park, CA (October 1989)
Suttner, C.B., Sutcliffe, G.: The TPTP problem library - v2.1.0. Technical Report JCU-CS-97/8, Department of Computer Science, James Cook University (December 15, 1997)
Voronkov, A.: The anatomy of Vampire: Implementing bottom-up procedures with code trees. Journal of Automated Reasoning 15(2), 237–265 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Riazanov, A., Voronkov, A. (2003). Efficient Instance Retrieval with Standard and Relational Path Indexing. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_34
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive