Journal article
Bounded-overhead caching for definite-clause theorem proving
Journal of automated reasoning, Vol.11(1), pp.83-113
1993
DOI: 10.1007/BF00881901
Abstract
In this paper we describe the design of an effective caching mechanism for resource-limited, definite-clause theorem-proving systems. Previous work in adapting caches for theorem proving relies on the use of unlimited-size caches. We show how unlimited-size caches are unsuitable in application contexts where resource-limited theorem provers are used to solve multiple problems from a single problem distribution. We introduce bounded-overhead caches, that is, those caches that contain at most a fixed number of entries and entail a fixed amount of overhead per lookup, and we examine cache design issues for bounded-overhead caches. Finally, we present an empirical evaluation of bounded-overhead cache performance, relying on a specially designed experimental methodology that separates hardware-dependent, implementation-dependent, and domain-dependent effects. © 1993 Kluwer Academic Publishers.
Details
- Title: Subtitle
- Bounded-overhead caching for definite-clause theorem proving
- Creators
- Alberto Segre - Cornell UniversityDaniel Scharstein - Cornell University
- Resource Type
- Journal article
- Publication Details
- Journal of automated reasoning, Vol.11(1), pp.83-113
- DOI
- 10.1007/BF00881901
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- Language
- English
- Date published
- 1993
- Academic Unit
- Nursing; Fraternal Order of Eagles Diabetes Research Center; Computer Science
- Record Identifier
- 9984259487202771
Metrics
5 Record Views