Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor(s)

Author(s):

Ganzinger, Harald
Nieuwenhuis, Robert
Nivela, Pilar

dblp
dblp
dblp

Not MPG Author(s):

Nieuwenhuis, Robert
Nivela, Pilar

BibTeX cite key*:

GanzingerNieuwenhuisNivela-03-jar

Title

Title*:

Fast Term Indexing with Coded Context Trees


2003JAR.ps (371.46 KB)

Journal

Journal Title*:

Journal of Automated Reasoning

Journal's URL:

http://www-unix.mcs.anl.gov/JAR/

Download URL
for the article:

http://www.mpi-sb.mpg.de/~hg/papers/journals/2003JAR.ps

Language:

English

Publisher

Publisher's
Name:

Kluwer

Publisher's URL:

http://www.wkap.nl/

Publisher's
Address:

Dordrecht, the Netherlands

ISSN:


Vol, No, pp, Date

Volume*:

32

Number:

2

Publishing Date:

February 2004

Pages*:

103-120

Number of
VG Pages:


Page Start:

103

Page End:

120

Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) 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.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:

doi:10.1023/B:JARS.0000029963.64213.ac

Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:

@ARTICLE{GanzingerNieuwenhuisNivela-03-jar,
AUTHOR = {Ganzinger, Harald and Nieuwenhuis, Robert and Nivela, Pilar},
TITLE = {Fast Term Indexing with Coded Context Trees},
JOURNAL = {Journal of Automated Reasoning},
PUBLISHER = {Kluwer},
YEAR = {2004},
NUMBER = {2},
VOLUME = {32},
PAGES = {103--120},
ADDRESS = {Dordrecht, the Netherlands},
MONTH = {February},
}


Entry last modified by Anja Becker, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Christine Kiesel
Created
05/08/2003 12:49:19 PM
Revisions
10.
9.
8.
7.
6.
Editor(s)
Anja Becker
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Brigitta Hansen
Brigitta Hansen
Edit Dates
02.02.2005 12:31:49
06/23/2004 04:18:00 PM
06/23/2004 01:58:19 PM
01/26/2004 01:27:55 PM
01/26/2004 01:24:03 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section

View attachments here:


File Attachment Icon
2003JAR.ps