Access the full text.
Sign up today, get DeepDyve free for 14 days.
Loading next page...
/lp/springer-journals/bounded-overhead-caching-for-definite-clause-theorem-proving-uczmoRcglW
References (48)
-
(1980)
An outlook on truth maintenance', Memo 551 -
D. McDermott (1991)
A General Framework for Reason MaintenanceArtif. Intell., 50
-
(1992)
Segre&Scharstein November -
(1991)
Learning Howt oP lan -
D. Plaisted (1988)
Non-Horn clause logic programming without contrapositivesJournal of Automated Reasoning, 4
-
S. Dietrich (1987)
Extension Tables: Memo Relations in Logic Programming -
(1992)
Memoing for logic programs', Communications of the Association for Computing Machinery -
M. Ginsberg, W. Harvey (1990)
Iterative BroadeningArtif. Intell., 55
-
D. Warren (1992)
Memoing for logic programsCommun. ACM, 35
-
C. Elkan (1989)
Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving -
D. Patterson, J. Hennessy (1969)
Computer Architecture: A Quantitative Approach -
E. KorfRichard (1985)
Depth-first iterative-deepening: an optimal admissible tree searchArtificial Intelligence
-
J. Doyle (1977)
Truth Maintenance Systems for Problem Solving -
K. Bergqvist, R. Säljö (2004)
Learning to Plan -
G. Sussman (1973)
A Computational Model of Skill Acquisition -
(1992)
Iterative broadening', Artificial Intelligence -
A. Segre (1988)
Machine Learning of Robot Assembly Plans -
(1991)
Technical note: a critical look at experimental evaluations of EBL', Machine Learning -
C. Elkan (1990)
Incremental, Approximate Planning -
A. M. Segre, C. Elkan, A. Russell (1991)
Technical note: a critical look at experimental evaluations of EBLMachine Learning, 6
-
A. M. Segre, J. Turney (1993)
Machine Learning Methods for Planning -
T. Nicholson (1989)
“All the right moves” -
(1991)
A general framework for reasong maintenance -
H. Tamaki, Taisuke Sato (1986)
OLD Resolution with Tabulation -
D. Michie (1968)
“Memo” Functions and Machine LearningNature, 218
-
(1989)
SEPIA: an experiment in integrated planning and improvisation -
David McAllester (1982)
Reasoning Utility Package User's Manual, Version One -
(1991)
A robust methodology for experimental evaluations of speedup learning -
A. M. Segre, C. Elkan, D. Scharstein, G. Gordon, A. Russell (1993)
Machine Learning: Induction, Analogy, and Discovery -
Steven Minton (1988)
Quantitative Results Concerning the Utility of Explanation-based LearningArtif. Intell., 42
-
(1993)
Adaptive inference', in Machine Learning: Induction, Analogy, and Discovery, S -
D. S. Warren (1992)
Memoing for logic programsCommunications of the Association for Computing Machinery, 35
-
Jack Mostow, D. Cohen (1985)
Automating Program Speedup by Deciding What to Cache -
David Slate, L. Atkin (1988)
Chess 4.5-The Northwestern University chess program -
Alberto Segre, J. Turney (1993)
Planning, Acting, and Learning in a Dynamic Domain -
(1990)
A provably complete family of EBL algorithms -
Alberto Segre, J. Turney (1992)
SEPIA: a resource-bounded adaptive agent -
Alberto Segre (1992)
On Combining Multiple Speedup Techniques -
Alberto Segre, C. Elkan, Alexander Russell (2005)
A critical look at experimental evaluations of EBLMachine Learning, 6
-
Perry Trunick (2003)
AT THE RIGHT MOVESLogistics Today
-
(1982)
emo 667, MIT Artificial Intelligence Laboratory,Cambridge -
Alberto Segre (1987)
Explanation-Based Learning of Generalized Robot Assembly Plans -
David McAllester (1980)
An Outlook on Truth Maintenance. -
C. Green (1969)
Application of Theorem Proving to Problem Solving -
(1993)
Adaptive Inference, " i n Fo undations of KnowledgeA cquisition -
J. Turney, Alberto Segre (1989)
A Framework for Learning in Planning Domains with Uncertainty -
O. Astrachan, M. Stickel (1992)
Caching and Lemmaizing in Model Elimination Theorem Provers -
R. Korf (1985)
Depth-First Iterative-Deepening: An Optimal Admissible Tree SearchArtif. Intell., 27
- Publisher
- Springer Journals
- Copyright
- Copyright
- Subject
- Computer Science; Mathematical Logic and Formal Languages; Artificial Intelligence; Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- DOI
- 10.1007/BF00881901
- Publisher site
- See Article on Publisher Site
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.
Journal
Journal of Automated Reasoning – Springer Journals
Published: Dec 10, 2004