English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Fast Term Indexing with Coded Context Trees

Ganzinger, H., Nieuwenhuis, R., & Nivela, P. (2004). Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning, 32, 103-120.

Item is

Files

show Files
hide Files
:
2003JAR.ps (Any fulltext), 372KB
 
File Permalink:
-
Name:
2003JAR.ps
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/postscript
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Ganzinger, Harald1, Author           
Nieuwenhuis, Robert1, Author           
Nivela, Pilar1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: Indexing data structures have a crucial impact on the performance of automated theorem provers. Examples are discrimination trees, which are like tries where terms are seen as strings and common prefixes are shared, and substitution trees, where terms keep their tree structure and all common contexts can be shared. Here we describe a new indexing data structure, called context trees, where, by means of a limited kind of context variables, also common subterms can be shared, even if they occur below different function symbols. Apart from introducing the concept, we also provide evidence for its practical value. We show how context trees can be implemented by means of abstract machine instructions. Experiments with matching benchmarks show that our implementation is competitive with tightly coded current state-of-the-art implementations of the other main techniques. In particular space consumption of context trees is significantly less than for other index structures.

Details

show
hide
Language(s): eng - English
 Dates: 2005-02-022004
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: Peer
 Identifiers: eDoc: 231252
Other: Local-ID: C1256104005ECAFC-B0EF8A197F4BBBE400256D20003B728C-GanzingerNieuwenhuisNivela-03-jar
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: Journal of Automated Reasoning
Source Genre: Journal
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 32 Sequence Number: - Start / End Page: 103 - 120 Identifier: -