Model-Checking Memory Requirements of Resource-Bounded Reasoners

Proceedings of the AAAI Conference on Artificial Intelligence, 21

Volume

Technical Papers

Knowledge Representation and Logic

Memory bounds may limit the ability of a reasoner to make inferences and therefore affect the reasoner's usefulness. In this paper, we propose a framework to automatically verify the reasoning capabilities of propositional memory-bounded reasoners which have a sequential 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 trivial to infer even for simple problems, and that memory bounds and length of derivations are closely interrelated.