MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


Substitution tree indexing

Graf, Peter

October 1994, 34 pages.

Status: available - back from printing

The performance of a theorem prover crucially depends on the speed of the basic retrieval operations, such as finding terms that are unifiable with (instances of, or more general than) a given query term. In this paper a new indexing method is presented, which outperforms traditional methods such as path indexing, discrimination tree indexing and abstraction trees. Additionally, the new index not only supports term indexing but also provides maintenance and efficient retrieval of substitutions. As confirmed in multiple experiments, substitution trees combine maximal search speed and minimal memory requirements.

  • MPI-I-94-251.pdfMPI-I-94-251.pdfMPI-I-94-251.dvi
  • Attachement: MPI-I-94-251.dvi (195 KBytes); MPI-I-94-251.pdf (231 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Graf, Peter},
  TITLE = {Substitution tree indexing},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-251},
  MONTH = {October},
  YEAR = {1994},
  ISSN = {0946-011X},