Computational psychology has the aim to explain human cognition by computational models of cognitive processes. The cognitive architecture ACT-R is popular to develop such models. Although ACT-R has a well-defined psychological theory and has been used to explain many cognitive processes, there are two problems that make it hard to reason formally about its cognitive models: First, ACT-R lacks a formalization of its underlying production rule system and secondly, there are many different implementations and extensions of ACT-R with technical artifacts complicating formal reasoning even more. This paper describes a formal operational semantics - the very abstract semantics - that abstracts from as many technical details as possible keeping it open to extensions and different implementations of the ACT-R theory. In a second step, this semantics is refined to define some of its abstract features that are found in many implementations of ACT-R - the abstract semantics. It concentrates on the procedural core of ACT-R and is suitable for analysis of the transition system since it still abstracts from details like timing, the sub-symbolic layer or conflict resolution. Furthermore, a translation of ACT-R models to the programming language Constraint Handling Rules (CHR) is defined. This makes the abstract semantics an executable specification of ACT-R. CHR has been used successfully to embed other rule-based formalisms like graph transformation systems or functional programming. There are many results and tools that support formal reasoning about and analysis of CHR programs. The translation of ACT-R models to CHR is proven sound and complete w.r.t. the abstract operational semantics of ACT-R. This paves the way to analysis of ACT-R models through CHR. Therefore, to the best of our knowledge, our abstract semantics is the first formulation of ACT-R suitable for both analysis and execution.
Download