English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Context trees

Ganzinger, H., Nieuwenhuis, R., & Nivela, P. (2001). Context trees. In R. Goré, A. Leitsch, & T. Nipkow (Eds.), Automated reasoning: First International Joint Conference, IJCAR 2001 (pp. 242-256). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3209-0 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-320C-A
Genre: Conference Paper

Files

show Files
hide Files
:
_01IJCAR-1.pdf (Any fulltext), 149KB
 
File Permalink:
-
Name:
_01IJCAR-1.pdf
Description:
-
OA-Status:
Visibility:
Private
MIME-Type / Checksum:
application/pdf
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 are well-known to be crucial for the efficiency of the current state-of-the-art theorem provers. Examples are \emph{discrimination trees}, which are like tries where terms are seen as strings and common prefixes are shared, and \emph{substitution trees}, where terms keep their tree structure and all common \emph{contexts} can be shared. Here we describe a new indexing data structure, \emph{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 describe an implementation of context trees based on Curry terms and on an extension of substitution trees with equality constraints and where one does not distinguish between \emph{internal} and \emph{external} variables. Experiments with matching show that our preliminary implementation is already competitive with tightly coded current state-of-the-art implementations of the other main techniques. In particular space consumption of context trees is substantially less than for other index structures.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-122001
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519831
Other: Local-ID: C1256104005ECAFC-EB2E979F49F72498C1256AB50052FCC3-GanzingerNieuwenhuisNivela-01-ijcar
 Degree: -

Event

show
hide
Title: IJCAR 2001
Place of Event: Siena, Italy
Start-/End Date: 2001-06-18 - 2001-06-22

Legal Case

show

Project information

show

Source 1

show
hide
Title: Automated reasoning : First International Joint Conference, IJCAR 2001
Source Genre: Proceedings
 Creator(s):
Goré, Rajeev, Editor
Leitsch, Alexander, Editor
Nipkow, Tobias, Editor
Affiliations:
-
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 242 - 256 Identifier: ISBN: 3-540-42254-4

Source 2

show
hide
Title: Lecture Notes in Artificial Intelligence
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 2083 Sequence Number: - Start / End Page: - Identifier: -