Memory bounds may limit the ability of a reasoner to make inferences and therefore affect the reasoner’s use- fulness. In this paper, we propose a framework to au- tomatically verify the reasoning capabilities of proposi- tional memory-bounded reasoners which have a sequen- tial architecture. Our framework explicitly accounts for the use of memory both to store facts and to support backtracking in the course of deductions. We describe an implementation of our framework in which proof existence is recast as a strong planning problem, and present results of experiments using the MBP planner which indicate that memory bounds may not be triv- ial to infer even for simple problems, and that mem- ory bounds and length of derivations are closely inter- related.
Model-checking memory requirements of resource-bounded reasoners
Albore, Alexandre;Bertoli, Piergiorgio;Ghidini, Chiara;Serafini, Luciano
2006-01-01
Abstract
Memory bounds may limit the ability of a reasoner to make inferences and therefore affect the reasoner’s use- fulness. In this paper, we propose a framework to au- tomatically verify the reasoning capabilities of proposi- tional memory-bounded reasoners which have a sequen- tial architecture. Our framework explicitly accounts for the use of memory both to store facts and to support backtracking in the course of deductions. We describe an implementation of our framework in which proof existence is recast as a strong planning problem, and present results of experiments using the MBP planner which indicate that memory bounds may not be triv- ial to infer even for simple problems, and that mem- ory bounds and length of derivations are closely inter- related.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
