Automated Commonsense Reasoning about Human Memory

Metacognition in Computation

Volume

Papers from the 2005 AAAI Spring Symposium

Contents

Metacognitive reasoning in computational systems will be enabled by the development of formal theories that have broad coverage over mental states and processes as well as inferential competency. In this paper we evaluate the inferential competency of an existing formal theory of commonsense human memory by attempting to use it to validate the appropriateness of a commonsense memory strategy. We formulate a particular memory strategy (to create an associated obstacle) as a theorem in first-order predicate calculus. We then attempt to validate this strategy by showing that it is entailed by the axioms of the theory we evaluated. These axioms were encoded into the syntax of an automated reasoning system, which was used to automatically generate inferences and search for formal proofs.