Publications: Journal Article: Fast Term Indexing with Coded Context Trees

Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

Options:

Goto entry point

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
Attachment(s):	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

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

Attachment Section

2003JAR.ps

2003JAR.ps